Nuprl Lemma : vdf-eq-implies

[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[n:ℕ]. ∀[f:vdf(A;B;a,b.C[a;b];n)]. ∀[L:(a:A × b:B × C[a;b]) List].
  vdf-eq(A;f;L)  (∀[i:ℕ||L||]. ((fst(L[i])) (f firstn(i;L) (fst(snd(L[i])))) ∈ A)) supposing ||L|| ≤ (n 1)


Proof




Definitions occuring in Statement :  vdf: vdf(A;B;a,b.C[a; b];n) vdf-eq: vdf-eq(A;f;L) firstn: firstn(n;as) select: L[n] length: ||as|| list: List int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] pi1: fst(t) pi2: snd(t) le: A ≤ B implies:  Q apply: a function: x:A ⟶ B[x] product: x:A × B[x] add: m natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] and: P ∧ Q uimplies: supposing a implies:  Q subtype_rel: A ⊆B prop: so_apply: x[s1;s2] nat:
Lemmas referenced :  vdf-wf+ istype-le length_wf list_wf istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination productElimination independent_functionElimination equalityTransitivity equalitySymmetry lambdaFormation_alt rename applyEquality sqequalRule universeIsType productEquality addEquality setElimination natural_numberEquality isect_memberEquality_alt lambdaEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies because_Cache functionIsType instantiate universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[f:vdf(A;B;a,b.C[a;b];n)].
\mforall{}[L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List].
    vdf-eq(A;f;L)  {}\mRightarrow{}  (\mforall{}[i:\mBbbN{}||L||].  ((fst(L[i]))  =  (f  firstn(i;L)  (fst(snd(L[i])))))) 
    supposing  ||L||  \mleq{}  (n  +  1)



Date html generated: 2020_05_19-PM-09_40_51
Last ObjectModification: 2020_03_05-PM-04_49_08

Theory : co-recursion-2


Home Index