Nuprl Lemma : vdf-eq-subtype
∀[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) ⊆r (∀[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: T List,
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
le: A ≤ B,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
add: n + m,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
and: P ∧ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
implies: P ⇒ Q,
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,
lambdaEquality_alt,
because_Cache,
independent_functionElimination,
applyEquality,
sqequalRule,
universeIsType,
productEquality,
addEquality,
setElimination,
rename,
natural_numberEquality,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
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) \msubseteq{}r (\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_48
Last ObjectModification:
2020_03_05-PM-04_41_33
Theory : co-recursion-2
Home
Index