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