Nuprl Lemma : Wmul-add-properties
∀[A:Type]. ∀[B:A ⟶ Type].
∀zero,succ:A ⟶ 𝔹.
((∀a:A. ((↑(succ a)) ⇒ B[a] ≡ Unit))
⇒ (∀a:A. (¬↑(zero a) ⇐⇒ B[a]))
⇒ (∀a1,a2:A. ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A)))
⇒ (∀x,y,z:W(A;a.B[a]).
(((x + (y + z)) = ((x + y) + z) ∈ W(A;a.B[a]))
∧ ((x * (y + z)) = ((x * y) + (x * z)) ∈ W(A;a.B[a]))
∧ ((x * (y * z)) = ((x * y) * z) ∈ W(A;a.B[a]))
∧ (isZero(z) ⇒ isZero(y) ⇒ (z = y ∈ W(A;a.B[a])))
∧ (isZero(z)
⇒ ((((x + z) = x ∈ W(A;a.B[a])) ∧ ((z + x) = x ∈ W(A;a.B[a]))) ∧ ((x * z) = z ∈ W(A;a.B[a])) ∧ (z ≤ x)))
∧ ((x ≤ y) ⇒ (((x + z) ≤ (y + z)) ∧ ((z + x) ≤ (z + y))))
∧ ((x < y) ⇒ ((z + x) < (z + y)))
∧ ((x ≤ y) ⇒ ((x * z) ≤ (y * z))))))
Proof
Definitions occuring in Statement :
Wmul: (w1 * w2),
Wadd: (w1 + w2),
Wzero: isZero(w),
Wcmp: Wcmp(A;a.B[a];leq),
W: W(A;a.B[a]),
assert: ↑b,
bfalse: ff,
btrue: tt,
bool: 𝔹,
ext-eq: A ≡ B,
uall: ∀[x:A]. B[x],
infix_ap: x f y,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
not: ¬A,
false: False,
so_apply: x[s],
prop: ℙ,
rev_implies: P ⇐ Q,
decidable: Dec(P),
or: P ∨ Q,
subtype_rel: A ⊆r B,
cand: A c∧ B,
squash: ↓T,
so_lambda: λ2x.t[x],
true: True,
uimplies: b supposing a,
guard: {T},
ext-eq: A ≡ B,
infix_ap: x f y
Lemmas referenced :
assert_wf,
decidable__assert,
not_wf,
assert_witness,
equal_wf,
squash_wf,
true_wf,
W_wf,
Wadd-assoc,
Wadd_wf,
iff_weakening_equal,
Wmul-Wadd,
Wmul_wf,
Wmul-assoc,
Wzero-unique,
Wzero_wf,
Wadd-Wzero,
Wmul-Wzero,
Wzero-leq,
Wleq-Wadd,
Wleq-Wadd2,
Wcmp_wf,
btrue_wf,
Wless-Wadd,
bfalse_wf,
Wleq-Wmul,
all_wf,
iff_wf,
ext-eq_wf,
unit_wf2,
bool_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
independent_pairFormation,
thin,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
hypothesis,
sqequalHypSubstitution,
independent_functionElimination,
voidElimination,
extract_by_obid,
isectElimination,
dependent_functionElimination,
unionElimination,
productElimination,
because_Cache,
sqequalRule,
independent_pairEquality,
lambdaEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
imageMemberEquality,
baseClosed,
universeEquality,
independent_isectElimination,
axiomEquality,
functionEquality
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type].
\mforall{}zero,succ:A {}\mrightarrow{} \mBbbB{}.
((\mforall{}a:A. ((\muparrow{}(succ a)) {}\mRightarrow{} B[a] \mequiv{} Unit))
{}\mRightarrow{} (\mforall{}a:A. (\mneg{}\muparrow{}(zero a) \mLeftarrow{}{}\mRightarrow{} B[a]))
{}\mRightarrow{} (\mforall{}a1,a2:A. ((\muparrow{}(zero a1)) {}\mRightarrow{} (\muparrow{}(zero a2)) {}\mRightarrow{} (a1 = a2)))
{}\mRightarrow{} (\mforall{}x,y,z:W(A;a.B[a]).
(((x + (y + z)) = ((x + y) + z))
\mwedge{} ((x * (y + z)) = ((x * y) + (x * z)))
\mwedge{} ((x * (y * z)) = ((x * y) * z))
\mwedge{} (isZero(z) {}\mRightarrow{} isZero(y) {}\mRightarrow{} (z = y))
\mwedge{} (isZero(z) {}\mRightarrow{} ((((x + z) = x) \mwedge{} ((z + x) = x)) \mwedge{} ((x * z) = z) \mwedge{} (z \mleq{} x)))
\mwedge{} ((x \mleq{} y) {}\mRightarrow{} (((x + z) \mleq{} (y + z)) \mwedge{} ((z + x) \mleq{} (z + y))))
\mwedge{} ((x < y) {}\mRightarrow{} ((z + x) < (z + y)))
\mwedge{} ((x \mleq{} y) {}\mRightarrow{} ((x * z) \mleq{} (y * z))))))
Date html generated:
2017_04_14-AM-07_45_09
Last ObjectModification:
2017_02_27-PM-03_16_18
Theory : co-recursion
Home
Index