---

Step * 1 of Lemma sbhomout-correct


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))))
BY
{ xxx((Assert ⌜∀L:ℕ2 List. ∀x:ℕ.
                 ∀[a,b,c,d:ℕ].
                   (((a + b + c + d) ≤ x)
                   ⇒ 0 < a + b
                   ⇒ 0 < c + d
                   ⇒ (sbhomout(a;b;c;d;L)
                      = let m,n = sbdecode(L) 
                        in sbcode((a * m) + (b * n);(c * m) + (d * n))
                      ∈ (ℕ2 List)))⌝
       ⋅
      THENM (xxxAutoxxx THEN InstHyp [⌜L⌝;⌜a + b + c + d⌝] 2⋅ THEN Auto)
      )
      THEN InductionOnList
      THEN InductionOnNat
      THEN Auto'
      THEN RecUnfold `sbhomout` 0
      THEN Reduce 0
      THEN Auto)xxx }

1
1. ∀a,b:ℕ. ∀m,n:ℕ+.  (0 < a + b ⇒ 0 < (a * m) + (b * n))
2. u : ℕ2
3. v : ℕ2 List
4. ∀x:ℕ
     ∀[a,b,c,d:ℕ].
       (((a + b + c + d) ≤ x)
       ⇒ 0 < a + b
       ⇒ 0 < c + d
       ⇒ (sbhomout(a;b;c;d;v) = let m,n = sbdecode(v) in sbcode((a * m) + (b * n);(c * m) + (d * n)) ∈ (ℕ2 List)))
5. x : ℤ
6. 0 < x
7. ∀[a,b,c,d:ℕ].
     (((a + b + c + d) ≤ (x - 1))
     ⇒ 0 < a + b
     ⇒ 0 < c + d
     ⇒ (sbhomout(a;b;c;d;[u / v])
        = let m,n = sbdecode([u / v]) 
          in sbcode((a * m) + (b * n);(c * m) + (d * n))
        ∈ (ℕ2 List)))
8. a : ℕ
9. b : ℕ
10. c : ℕ
11. d : ℕ
12. (a + b + c + d) ≤ x
13. 0 < a + b
14. 0 < c + d
⊢ if mtge1(a;b;c;d) then eval a' = a - c in eval b' = b - d in   [1 / sbhomout(a';b';c;d;[u / v])]
if mtge1(c;d;a;b) then eval c' = c - a in eval d' = d - b in   [0 / sbhomout(a;b;c';d';[u / v])]
else if u=0
     then eval a' = a + b in
          eval c' = c + d in
            sbhomout(a';b;c';d;v)
     else eval b' = a + b in
          eval d' = c + d in
            sbhomout(a;b';c;d';v)
fi 
= let m,n = sbdecode([u / v]) 
  in sbcode((a * m) + (b * n);(c * m) + (d * n))
∈ (ℕ2 List)

---

Latex:

---

Latex:

1.  \mforall{}a,b:\mBbbN{}.  \mforall{}m,n:\mBbbN{}\msupplus{}.    (0  <  a  +  b  {}\mRightarrow{}  0  <  (a  *  m)  +  (b  *  n))
\mvdash{}  \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  \mkleeneopen{}\mforall{}L:\mBbbN{}2  List.  \mforall{}x:\mBbbN{}.
                              \mforall{}[a,b,c,d:\mBbbN{}].
                                  (((a  +  b  +  c  +  d)  \mleq{}  x)
                                  {}\mRightarrow{}  0  <  a  +  b
                                  {}\mRightarrow{}  0  <  c  +  d
                                  {}\mRightarrow{}  (sbhomout(a;b;c;d;L)
                                        =  let  m,n  =  sbdecode(L) 
                                            in  sbcode((a  *  m)  +  (b  *  n);(c  *  m)  +  (d  *  n))))\mkleeneclose{}
          \mcdot{}
        THENM  (xxxAutoxxx  THEN  InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a  +  b  +  c  +  d\mkleeneclose{}]  2\mcdot{}  THEN  Auto)
        )
        THEN  InductionOnList
        THEN  InductionOnNat
        THEN  Auto'
        THEN  RecUnfold  `sbhomout`  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index