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