Nuprl Lemma : product_well_fnd
∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
(WellFnd{i}(A;a1,a2.Ra[a1;a2])
⇒ WellFnd{i}(B;b1,b2.Rb[b1;b2])
⇒ WellFnd{i}(A × B;p1,p2.let a1,b1 = p1
in let a2,b2 = p2
in Ra[a1;a2] ∨ ((a1 = a2 ∈ A) ∧ Rb[b1;b2])))
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],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s1;s2],
and: P ∧ Q,
subtype_rel: A ⊆r B,
or: P ∨ Q,
so_apply: x[s],
all: ∀x:A. B[x],
so_lambda: λ2x y.t[x; y]
Lemmas referenced :
all_wf,
or_wf,
equal_wf,
wellfounded_wf
Rules used in proof :
hyp_replacement,
applyLambdaEquality,
unionElimination,
dependent_functionElimination,
spreadEquality,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
productEquality,
cumulativity,
hypothesisEquality,
sqequalRule,
lambdaEquality,
functionEquality,
because_Cache,
productElimination,
applyEquality,
functionExtensionality,
hypothesis,
independent_pairEquality,
universeEquality
Latex:
\mforall{}[A,B:Type]. \mforall{}[Ra:A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}]. \mforall{}[Rb:B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}].
(WellFnd\{i\}(A;a1,a2.Ra[a1;a2])
{}\mRightarrow{} WellFnd\{i\}(B;b1,b2.Rb[b1;b2])
{}\mRightarrow{} WellFnd\{i\}(A \mtimes{} B;p1,p2.let a1,b1 = p1
in let a2,b2 = p2
in Ra[a1;a2] \mvee{} ((a1 = a2) \mwedge{} Rb[b1;b2])))
Date html generated:
2019_06_20-PM-01_04_20
Last ObjectModification:
2019_06_20-PM-01_01_50
Theory : well_fnd
Home
Index