---

Step * of 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))))))
BY
{ (RepeatFor 10 ((D 0 THENA Auto))
   THEN (Assert ∀a:A. (↑(zero a) ⇐⇒ ¬B[a]) BY
               (Auto THEN ((D 0 THENA Auto) ORELSE SupposeNot) THEN FHyp 6 [-1] THEN Auto))
   THEN Auto
   THEN Try (((BLemma `Wadd-assoc`
               ORELSE BLemma `Wmul-Wadd`
               ORELSE BLemma `Wmul-assoc`
               ORELSE BLemma `Wadd-Wzero`
               ORELSE BLemma `Wmul-Wzero`
               ORELSE UsingVars [`zero'] (BLemma `Wzero-unique`)
               ORELSE BLemma `Wleq-Wadd`
               ORELSE BLemma `Wleq-Wadd2`
               ORELSE BLemma `Wless-Wadd`
               ORELSE BLemma `Wleq-Wmul`
               ORELSE BLemma `Wzero-leq`)
              THEN Auto
              ))) }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  10  ((D  0  THENA  Auto))
  THEN  (Assert  \mforall{}a:A.  (\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}B[a])  BY
                          (Auto  THEN  ((D  0  THENA  Auto)  ORELSE  SupposeNot)  THEN  FHyp  6  [-1]  THEN  Auto))
  THEN  Auto
  THEN  Try  (((BLemma  `Wadd-assoc`
                          ORELSE  BLemma  `Wmul-Wadd`
                          ORELSE  BLemma  `Wmul-assoc`
                          ORELSE  BLemma  `Wadd-Wzero`
                          ORELSE  BLemma  `Wmul-Wzero`
                          ORELSE  UsingVars  [`zero']  (BLemma  `Wzero-unique`)
                          ORELSE  BLemma  `Wleq-Wadd`
                          ORELSE  BLemma  `Wleq-Wadd2`
                          ORELSE  BLemma  `Wless-Wadd`
                          ORELSE  BLemma  `Wleq-Wmul`
                          ORELSE  BLemma  `Wzero-leq`)
                        THEN  Auto
                        )))

---

Home Index