---

Step * of Lemma sbhomout-correct

∀[a,b,c,d:ℕ].
  (0 < a + b
  ⇒ 0 < c + d
  ⇒ (∀[L:ℕ2 List]
        (sbhomout(a;b;c;d;L) = let m,n = sbdecode(L) in sbcode((a * m) + (b * n);(c * m) + (d * n)) ∈ (ℕ2 List))))
BY
{ xxx(Assert ∀a,b:ℕ. ∀m,n:ℕ+.  (0 < a + b ⇒ 0 < (a * m) + (b * n)) BY
            (Auto
             THEN (Assert (0 ≤ (b * n)) ∧ (0 ≤ (a * m)) BY
                         Auto)
             THEN (Decide ⌜0 < a⌝⋅ THENA Auto)
             THEN Try ((Mul ⌜m⌝ (-1)⋅ THEN Auto'))
             THEN (Assert 0 < b BY
                         Auto')
             THEN Mul ⌜n⌝ (-1)⋅
             THEN Auto'))xxx }

1
1. ∀a,b:ℕ. ∀m,n:ℕ+.  (0 < a + b ⇒ 0 < (a * m) + (b * n))
⊢ ∀[a,b,c,d:ℕ].
    (0 < a + b
    ⇒ 0 < c + d
    ⇒ (∀[L:ℕ2 List]
          (sbhomout(a;b;c;d;L) = let m,n = sbdecode(L) in sbcode((a * m) + (b * n);(c * m) + (d * n)) ∈ (ℕ2 List))))

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbN{}].
    (0  <  a  +  b
    {}\mRightarrow{}  0  <  c  +  d
    {}\mRightarrow{}  (\mforall{}[L:\mBbbN{}2  List]
                (sbhomout(a;b;c;d;L)
                =  let  m,n  =  sbdecode(L) 
                    in  sbcode((a  *  m)  +  (b  *  n);(c  *  m)  +  (d  *  n)))))


By

---

Latex:
xxx(Assert  \mforall{}a,b:\mBbbN{}.  \mforall{}m,n:\mBbbN{}\msupplus{}.    (0  <  a  +  b  {}\mRightarrow{}  0  <  (a  *  m)  +  (b  *  n))  BY
                    (Auto
                      THEN  (Assert  (0  \mleq{}  (b  *  n))  \mwedge{}  (0  \mleq{}  (a  *  m))  BY
                                              Auto)
                      THEN  (Decide  \mkleeneopen{}0  <  a\mkleeneclose{}\mcdot{}  THENA  Auto)
                      THEN  Try  ((Mul  \mkleeneopen{}m\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto'))
                      THEN  (Assert  0  <  b  BY
                                              Auto')
                      THEN  Mul  \mkleeneopen{}n\mkleeneclose{}  (-1)\mcdot{}
                      THEN  Auto'))xxx

---

Home Index