---

Step * of Lemma sbhomout_wf

∀[a,b,c,d:ℕ].  (0 < a + b ⇒ 0 < c + d ⇒ (∀[L:ℕ2 List]. (sbhomout(a;b;c;d;L) ∈ ℕ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) ∈ ℕ2 List))⌝
       ⋅
      THENM (xxxAutoxxx THEN InstHyp [⌜L⌝;⌜a + b + c + d⌝] 1⋅ THEN Auto)
      )
      THEN InductionOnList
      THEN InductionOnNat
      THEN Auto'
      THEN RecUnfold `sbhomout` 0
      THEN Reduce 0
      THEN Auto
      THEN Try ((RepUR ``mtge1`` -1 THEN (RW assert_pushdownC (-1) THENA Auto))))xxx }

1
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. (a + b + c + d) ≤ x
12. 0 < a + b
13. 0 < c + d
14. mtge1(a;b;c;d) ∈ 𝔹
15. ((c ≤ a) ∧ d < b) ∨ (c < a ∧ (d ≤ b))
⊢ sbhomout(a - c;b - d;c;d;[u / v]) ∈ ℕ2 List

2
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(a;b;c;d)
12. (a + b + c + d) ≤ x
13. 0 < a + b
14. 0 < c + d
15. ff ∈ 𝔹
16. mtge1(c;d;a;b) ∈ 𝔹
17. ((a ≤ c) ∧ b < d) ∨ (a < c ∧ (b ≤ d))
⊢ sbhomout(a;b;c - a;d - b;[u / v]) ∈ ℕ2 List

3
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

4
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;a + b;c;c + d;v) ∈ ℕ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)  \mmember{}  \mBbbN{}2  List)))


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)  \mmember{}  \mBbbN{}2  List))\mkleeneclose{}
          \mcdot{}
        THENM  (xxxAutoxxx  THEN  InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a  +  b  +  c  +  d\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
        )
        THEN  InductionOnList
        THEN  InductionOnNat
        THEN  Auto'
        THEN  RecUnfold  `sbhomout`  0
        THEN  Reduce  0
        THEN  Auto
        THEN  Try  ((RepUR  ``mtge1``  -1  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))))xxx

---

Home Index