---

Step * 1 1 2 2 2 of Lemma sbhomout-correct


1. ∀a,b:ℕ. ∀m,n:ℕ+.  (0 < a + b ⇒ 0 < (a * m) + (b * n))
2. u : ℕ2
3. u ≠ 0
4. v : ℕ2 List
5. ∀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)))
6. x : ℤ
7. 0 < x
8. ∀[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)))
9. a : ℕ
10. b : ℕ
11. c : ℕ
12. d : ℕ
13. ¬↑mtge1(c;d;a;b)
14. ¬↑mtge1(a;b;c;d)
15. (a + b + c + d) ≤ x
16. 0 < a + b
17. 0 < c + d
⊢ sbhomout(a;a + b;c;c + d;v)
= let m,n = let m,n = sbdecode(v) 
            in <m + n, n> 
  in sbcode((a * m) + (b * n);(c * m) + (d * n))
∈ (ℕ2 List)
BY
{ ((InstHyp [⌜(a * 2) + b + (c * 2) + d⌝] 5⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Try (Complete (Auto)))
   THEN (GenConclTerm⌜sbdecode(v)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN EqCD
   THEN Try (MemTypeCD)
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}a,b:\mBbbN{}.  \mforall{}m,n:\mBbbN{}\msupplus{}.    (0  <  a  +  b  {}\mRightarrow{}  0  <  (a  *  m)  +  (b  *  n))
2.  u  :  \mBbbN{}2
3.  u  \mneq{}  0
4.  v  :  \mBbbN{}2  List
5.  \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;v)
                    =  let  m,n  =  sbdecode(v) 
                        in  sbcode((a  *  m)  +  (b  *  n);(c  *  m)  +  (d  *  n))))
6.  x  :  \mBbbZ{}
7.  0  <  x
8.  \mforall{}[a,b,c,d:\mBbbN{}].
          (((a  +  b  +  c  +  d)  \mleq{}  (x  -  1))
          {}\mRightarrow{}  0  <  a  +  b
          {}\mRightarrow{}  0  <  c  +  d
          {}\mRightarrow{}  (sbhomout(a;b;c;d;[u  /  v])
                =  let  m,n  =  sbdecode([u  /  v]) 
                    in  sbcode((a  *  m)  +  (b  *  n);(c  *  m)  +  (d  *  n))))
9.  a  :  \mBbbN{}
10.  b  :  \mBbbN{}
11.  c  :  \mBbbN{}
12.  d  :  \mBbbN{}
13.  \mneg{}\muparrow{}mtge1(c;d;a;b)
14.  \mneg{}\muparrow{}mtge1(a;b;c;d)
15.  (a  +  b  +  c  +  d)  \mleq{}  x
16.  0  <  a  +  b
17.  0  <  c  +  d
\mvdash{}  sbhomout(a;a  +  b;c;c  +  d;v)
=  let  m,n  =  let  m,n  =  sbdecode(v) 
                        in  <m  +  n,  n> 
    in  sbcode((a  *  m)  +  (b  *  n);(c  *  m)  +  (d  *  n))


By

---

Latex:
((InstHyp  [\mkleeneopen{}(a  *  2)  +  b  +  (c  *  2)  +  d\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Try  (Complete  (Auto)))
  THEN  (GenConclTerm\mkleeneopen{}sbdecode(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (MemTypeCD)
  THEN  Auto)

---

Home Index