### Nuprl Lemma : assert-pair-blex

`∀[A,B:Type].`
`  ∀eq:EqDecider(A). ∀Ra:A ⟶ A ⟶ 𝔹. ∀Rb:B ⟶ B ⟶ 𝔹. ∀x,y:A × B.`
`    (↑(pair-blex(eq;Ra;Rb) x y) `⇐⇒` pair-lex(A;λa,a'. (↑(Ra a a'));λb,b'. (↑(Rb b b'))) x y)`

Proof

Definitions occuring in Statement :  deq: `EqDecider(T)` pair-blex: `pair-blex(eq;Ra;Rb)` assert: `↑b` bool: `𝔹` pair-lex: `pair-lex(A;Ra;Rb)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` pair-lex: `pair-lex(A;Ra;Rb)` pair-blex: `pair-blex(eq;Ra;Rb)` pi1: `fst(t)` pi2: `snd(t)` eqof: `eqof(d)` member: `t ∈ T` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` or: `P ∨ Q` uiff: `uiff(P;Q)` uimplies: `b supposing a`
Lemmas referenced :  bool_wf deq_wf assert_wf bor_wf band_wf eqof_wf or_wf and_wf equal_wf iff_wf iff_transitivity iff_weakening_uiff assert_of_bor assert_of_band safe-assert-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation productElimination thin sqequalRule productEquality hypothesisEquality functionEquality cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination universeEquality independent_pairFormation because_Cache applyEquality addLevel impliesFunctionality independent_functionElimination dependent_functionElimination orFunctionality independent_isectElimination

Latex:
\mforall{}[A,B:Type].
\mforall{}eq:EqDecider(A).  \mforall{}Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:A  \mtimes{}  B.
(\muparrow{}(pair-blex(eq;Ra;Rb)  x  y)  \mLeftarrow{}{}\mRightarrow{}  pair-lex(A;\mlambda{}a,a'.  (\muparrow{}(Ra  a  a'));\mlambda{}b,b'.  (\muparrow{}(Rb  b  b')))  x  y)

Date html generated: 2016_05_14-AM-06_06_37
Last ObjectModification: 2015_12_26-AM-11_46_55

Theory : equality!deciders

Home Index