---

Step * 3 of Lemma sbhomout_wf


1. u : ℕ2
2. v : ℕ2 List
3. ∀x:ℕ. ∀[a,b,c,d:ℕ].  (((a + b + c + d) ≤ x) ⇒ 0 < a + b ⇒ 0 < c + d ⇒ (sbhomout(a;b;c;d;v) ∈ ℕ2 List))
4. x : ℤ
5. 0 < x
6. ∀[a,b,c,d:ℕ].  (((a + b + c + d) ≤ (x - 1)) ⇒ 0 < a + b ⇒ 0 < c + d ⇒ (sbhomout(a;b;c;d;[u / v]) ∈ ℕ2 List))
7. a : ℕ
8. b : ℕ
9. c : ℕ
10. d : ℕ
11. ¬↑mtge1(c;d;a;b)
12. ¬↑mtge1(a;b;c;d)
13. (a + b + c + d) ≤ x
14. 0 < a + b
15. 0 < c + d
16. ff ∈ 𝔹
17. ff ∈ 𝔹
18. u = 0 ∈ ℤ
⊢ sbhomout(a + b;b;c + d;d;v) ∈ ℕ2 List
BY
{ ((InstHyp [⌜a + (b * 2) + c + (d * 2)⌝] 3⋅ THENA Auto) THEN BHyp -1  THEN Auto') }

---

Latex:

---

Latex:

1.  u  :  \mBbbN{}2
2.  v  :  \mBbbN{}2  List
3.  \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)  \mmember{}  \mBbbN{}2  List))
4.  x  :  \mBbbZ{}
5.  0  <  x
6.  \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])  \mmember{}  \mBbbN{}2  List))
7.  a  :  \mBbbN{}
8.  b  :  \mBbbN{}
9.  c  :  \mBbbN{}
10.  d  :  \mBbbN{}
11.  \mneg{}\muparrow{}mtge1(c;d;a;b)
12.  \mneg{}\muparrow{}mtge1(a;b;c;d)
13.  (a  +  b  +  c  +  d)  \mleq{}  x
14.  0  <  a  +  b
15.  0  <  c  +  d
16.  ff  \mmember{}  \mBbbB{}
17.  ff  \mmember{}  \mBbbB{}
18.  u  =  0
\mvdash{}  sbhomout(a  +  b;b;c  +  d;d;v)  \mmember{}  \mBbbN{}2  List


By

---

Latex:
((InstHyp  [\mkleeneopen{}a  +  (b  *  2)  +  c  +  (d  *  2)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto')

---

Home Index