Nuprl Lemma : W-elimination-facts
∀A:Type. ∀B:A ⟶ Type. ∀w:W(A;a.B[a]).
((cw-step(A;a.B[a]) ∈ Type)
∧ (W-rel(A;a.B[a];w) ∈ n:ℕ ⟶ (ℕn ⟶ cw-step(A;a.B[a])) ⟶ cw-step(A;a.B[a]) ⟶ ℙ)
∧ (W(A;a.B[a]) ∈ Type)
∧ (W(A;a.B[a]) ⊆r (pco-W ⋅))
∧ (∀n:ℕ. ∀s:ℕn ⟶ cw-step(A;a.B[a]). (Barred(<n, s>) ∨ (¬Barred(<n, s>))))
∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (alpha ∈ Path)))
∧ (∀[pp:n:ℕ × (ℕn ⟶ cw-step(A;a.B[a]))]. (Barred(pp) ∈ ℙ))
∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (↓∃n:ℕ. Barred(<n, alpha>))))
∧ (∀a:A. ∀x1:B[a] ⟶ W(A;a.B[a]). ∀n:ℕ+. ∀s:ℕn ⟶ cw-step(A;a.B[a]). ∀a1:A. ∀w1:b:B[a1] ⟶ (pco-W ⋅). ∀x:B[a1]. ∀a2:A.
∀z1:b:B[a2] ⟶ (pco-W ⋅).
((∀k:ℕn. (W-rel(A;a.B[a];<a, x1>) k s (s k)))
⇒ ((s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A;a.B[a]))
⇒ ((w1 x) = <a2, z1> ∈ (pco-W ⋅))
⇒ (z1 ∈ B[a2] ⟶ W(A;a.B[a])))))
Proof
Definitions occuring in Statement :
W-rel: W-rel(A;a.B[a];w),
W: W(A;a.B[a]),
cw-step: cw-step(A;a.B[a]),
pcw-pp-barred: Barred(pp),
pcw-path: Path,
param-co-W: pco-W,
int_seg: {i..j-},
nat_plus: ℕ+,
nat: ℕ,
it: ⋅,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
unit: Unit,
member: t ∈ T,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
inl: inl x,
subtract: n - m,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
W: W(A;a.B[a]),
param-W: pW,
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
implies: P ⇒ Q,
prop: ℙ,
pcw-path: Path,
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
exists: ∃x:A. B[x],
pcw-partial: pcw-partial(path;n),
W-rel: W-rel(A;a.B[a];w),
param-W-rel: param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w),
cw-step: cw-step(A;a.B[a]),
squash: ↓T
Lemmas referenced :
cw-step_wf,
W-rel_wf,
W_wf,
param-co-W_wf,
top_wf,
all_wf,
pcw-path_wf,
unit_wf2,
it_wf,
pcw-step-agree_wf,
false_wf,
le_wf,
squash_wf,
exists_wf,
nat_wf,
pcw-pp-barred_wf,
pcw-partial_wf,
pcw-pp-barred-W-decidable,
int_seg_wf,
W-path-lemma,
pcw-pp-barred-W,
subtype_rel_self,
pcw-step_wf,
W-path-lemma2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality,
applyEquality,
hypothesis,
independent_pairFormation,
because_Cache,
setElimination,
rename,
setEquality,
cumulativity,
functionExtensionality,
isect_memberEquality,
voidElimination,
voidEquality,
functionEquality,
dependent_set_memberEquality,
natural_numberEquality,
dependent_functionElimination,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry,
imageElimination,
imageMemberEquality,
baseClosed,
universeEquality
Latex:
\mforall{}A:Type. \mforall{}B:A {}\mrightarrow{} Type. \mforall{}w:W(A;a.B[a]).
((cw-step(A;a.B[a]) \mmember{} Type)
\mwedge{} (W-rel(A;a.B[a];w) \mmember{} n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} cw-step(A;a.B[a])) {}\mrightarrow{} cw-step(A;a.B[a]) {}\mrightarrow{} \mBbbP{})
\mwedge{} (W(A;a.B[a]) \mmember{} Type)
\mwedge{} (W(A;a.B[a]) \msubseteq{}r (pco-W \mcdot{}))
\mwedge{} (\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} cw-step(A;a.B[a]). (Barred(<n, s>) \mvee{} (\mneg{}Barred(<n, s>))))
\mwedge{} (\mforall{}alpha:\mBbbN{} {}\mrightarrow{} cw-step(A;a.B[a])
((\mforall{}n:\mBbbN{}. (W-rel(A;a.B[a];w) n alpha (alpha n))) {}\mRightarrow{} (alpha \mmember{} Path)))
\mwedge{} (\mforall{}[pp:n:\mBbbN{} \mtimes{} (\mBbbN{}n {}\mrightarrow{} cw-step(A;a.B[a]))]. (Barred(pp) \mmember{} \mBbbP{}))
\mwedge{} (\mforall{}alpha:\mBbbN{} {}\mrightarrow{} cw-step(A;a.B[a])
((\mforall{}n:\mBbbN{}. (W-rel(A;a.B[a];w) n alpha (alpha n))) {}\mRightarrow{} (\mdownarrow{}\mexists{}n:\mBbbN{}. Barred(<n, alpha>))))
\mwedge{} (\mforall{}a:A. \mforall{}x1:B[a] {}\mrightarrow{} W(A;a.B[a]). \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} cw-step(A;a.B[a]). \mforall{}a1:A. \mforall{}w1:b:B[a1] {}\mrightarrow{} (pco-W
\mcdot{}).
\mforall{}x:B[a1]. \mforall{}a2:A. \mforall{}z1:b:B[a2] {}\mrightarrow{} (pco-W \mcdot{}).
((\mforall{}k:\mBbbN{}n. (W-rel(A;a.B[a];<a, x1>) k s (s k)))
{}\mRightarrow{} ((s (n - 1)) = <\mcdot{}, <a1, w1>, inl x>)
{}\mRightarrow{} ((w1 x) = <a2, z1>)
{}\mRightarrow{} (z1 \mmember{} B[a2] {}\mrightarrow{} W(A;a.B[a])))))
Date html generated:
2019_06_20-PM-00_36_32
Last ObjectModification:
2018_08_08-AM-08_40_15
Theory : co-recursion
Home
Index