---

Step * 1 1 1 1 of Lemma sbhomout-correct


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
15. ((c ≤ a) ∧ d < b) ∨ (c < a ∧ (d ≤ b))
16. v2 : ℕ+
17. v3 : ℕ+
18. sbdecode([u / v]) = <v2, v3> ∈ (ℕ+ × ℕ+)
⊢ [1 / sbcode(((a - c) * v2) + ((b - d) * v3);(c * v2) + (d * v3))]
= sbcode((a * v2) + (b * v3);(c * v2) + (d * v3))
∈ (ℕ2 List)
BY
{ xxx(RW (AddrC [3] RecUnfoldTopAbC) 0 THEN AutoSplit)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
15. ((c ≤ a) ∧ d < b) ∨ (c < a ∧ (d ≤ b))
16. v2 : ℕ+
17. v3 : ℕ+
18. sbdecode([u / v]) = <v2, v3> ∈ (ℕ+ × ℕ+)
19. (a * v2) + (b * v3) < (c * v2) + (d * v3)
⊢ [1 / sbcode(((a - c) * v2) + ((b - d) * v3);(c * v2) + (d * v3))]
= [0 / sbcode((a * v2) + (b * v3);((c * v2) + (d * v3)) - (a * v2) + (b * v3))]
∈ (ℕ2 List)

2
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
15. ((c ≤ a) ∧ d < b) ∨ (c < a ∧ (d ≤ b))
16. v2 : ℕ+
17. v3 : ℕ+
18. ¬(a * v2) + (b * v3) < (c * v2) + (d * v3)
19. sbdecode([u / v]) = <v2, v3> ∈ (ℕ+ × ℕ+)
⊢ [1 / sbcode(((a - c) * v2) + ((b - d) * v3);(c * v2) + (d * v3))]
= if ((c * v2) + (d * v3)) < ((a * v2) + (b * v3))
     then [1 / sbcode(((a * v2) + (b * v3)) - (c * v2) + (d * v3);(c * v2) + (d * v3))]
     else []
∈ (ℕ2 List)

---

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.  v  :  \mBbbN{}2  List
4.  \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))))
5.  x  :  \mBbbZ{}
6.  0  <  x
7.  \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))))
8.  a  :  \mBbbN{}
9.  b  :  \mBbbN{}
10.  c  :  \mBbbN{}
11.  d  :  \mBbbN{}
12.  (a  +  b  +  c  +  d)  \mleq{}  x
13.  0  <  a  +  b
14.  0  <  c  +  d
15.  ((c  \mleq{}  a)  \mwedge{}  d  <  b)  \mvee{}  (c  <  a  \mwedge{}  (d  \mleq{}  b))
16.  v2  :  \mBbbN{}\msupplus{}
17.  v3  :  \mBbbN{}\msupplus{}
18.  sbdecode([u  /  v])  =  <v2,  v3>
\mvdash{}  [1  /  sbcode(((a  -  c)  *  v2)  +  ((b  -  d)  *  v3);(c  *  v2)  +  (d  *  v3))]
=  sbcode((a  *  v2)  +  (b  *  v3);(c  *  v2)  +  (d  *  v3))


By

---

Latex:
xxx(RW  (AddrC  [3]  RecUnfoldTopAbC)  0  THEN  AutoSplit)xxx

---

Home Index