### 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