### Nuprl Lemma : compose-flips_wf

`∀k:ℕ. ∀flips:(ℕk × ℕk) List.  (compose-flips(flips) ∈ ℕk ⟶ ℕk)`

Proof

Definitions occuring in Statement :  compose-flips: `compose-flips(flips)` list: `T List` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` compose-flips: `compose-flips(flips)` uall: `∀[x:A]. B[x]` nat: `ℕ` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  map_wf int_seg_wf flip_wf list_wf reduce_wf compose_wf equal_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin productEquality natural_numberEquality setElimination rename because_Cache hypothesis functionEquality lambdaEquality spreadEquality productElimination independent_pairEquality hypothesisEquality functionExtensionality applyEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}flips:(\mBbbN{}k  \mtimes{}  \mBbbN{}k)  List.    (compose-flips(flips)  \mmember{}  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k)

Date html generated: 2017_04_17-AM-08_20_19
Last ObjectModification: 2017_02_27-PM-04_42_34

Theory : list_1

Home Index