Nuprl Lemma : wellfounded-lex
∀[A:Type]. ∀[<A:A ⟶ A ⟶ ℙ].
(WellFnd{i}(A;a,b.<A[a;b])
⇒ (∀[B:Type]. ∀[<B:B ⟶ B ⟶ ℙ].
(WellFnd{i}(B;a,b.<B[a;b])
⇒ WellFnd{i}(A × B;p,q.<A[fst(p);fst(q)] ∨ (((fst(p)) = (fst(q)) ∈ A) ∧ <B[snd(p);snd(q)])))))
Proof
Definitions occuring in Statement :
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
guard: {T},
all: ∀x:A. B[x],
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s1;s2],
pi1: fst(t),
and: P ∧ Q,
pi2: snd(t),
subtype_rel: A ⊆r B,
or: P ∨ Q,
so_apply: x[s],
so_lambda: λ2x y.t[x; y]
Lemmas referenced :
all_wf,
or_wf,
equal_wf,
wellfounded_wf,
pi2_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
rename,
cut,
dependent_functionElimination,
hypothesisEquality,
hypothesis,
productEquality,
cumulativity,
introduction,
extract_by_obid,
isectElimination,
sqequalRule,
lambdaEquality,
functionEquality,
because_Cache,
applyEquality,
functionExtensionality,
universeEquality,
independent_pairEquality,
independent_functionElimination,
unionElimination,
equalityTransitivity,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality
Latex:
\mforall{}[A:Type]. \mforall{}[<A:A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}].
(WellFnd\{i\}(A;a,b.<A[a;b])
{}\mRightarrow{} (\mforall{}[B:Type]. \mforall{}[<B:B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}].
(WellFnd\{i\}(B;a,b.<B[a;b])
{}\mRightarrow{} WellFnd\{i\}(A \mtimes{} B;p,q.<A[fst(p);fst(q)] \mvee{} (((fst(p)) = (fst(q))) \mwedge{} <B[snd(p);snd(q)])))))
Date html generated:
2018_05_21-PM-07_20_14
Last ObjectModification:
2017_07_26-PM-05_05_00
Theory : general
Home
Index