---

Step * 4 1 of Lemma remove-nat-missing-prop


1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
⊢ (x ≤ m)
  ∧ (¬((∃l:ℕ List
         (l @ [x] ≤ s1 ∧ (∀y1∈l.int-minus-comparison-inc(λx.x) y y1 < 0) ∧ int-minus-comparison-inc(λx.x) y x < 0))
    ∨ (∃l,l':ℕ List
        ∃a:ℕ
         (((l @ [a / l']) = s1 ∈ (ℕ List))
         ∧ (∀y1∈l.int-minus-comparison-inc(λx.x) y y1 < 0)
         ∧ ((0 < int-minus-comparison-inc(λx.x) y a ∧ (x ∈ [y; [a / l']]))
           ∨ (((int-minus-comparison-inc(λx.x) y a) = 0 ∈ ℤ) ∧ (x ∈ [y / l'])))))
    ∨ ((x = y ∈ ℕ) ∧ (∀y1∈s1.int-minus-comparison-inc(λx.x) y y1 < 0))))
⇐⇒ (¬(x = y ∈ ℕ)) ∧ (x ≤ m) ∧ (¬(x ∈ s1))
BY
{ (RepUR ``int-minus-comparison-inc`` 0 THEN Auto) }

1
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
7. x ≤ m@i
8. ¬((∃l:ℕ List. (l @ [x] ≤ s1 ∧ (∀y1∈l.y1 - y < 0) ∧ x - y < 0))
∨ (∃l,l':ℕ List
    ∃a:ℕ
     (((l @ [a / l']) = s1 ∈ (ℕ List))
     ∧ (∀y1∈l.y1 - y < 0)
     ∧ ((0 < a - y ∧ (x ∈ [y; [a / l']])) ∨ (((a - y) = 0 ∈ ℤ) ∧ (x ∈ [y / l'])))))
∨ ((x = y ∈ ℕ) ∧ (∀y1∈s1.y1 - y < 0)))@i
⊢ ¬(x = y ∈ ℕ)

2
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
7. x ≤ m@i
8. ¬((∃l:ℕ List. (l @ [x] ≤ s1 ∧ (∀y1∈l.y1 - y < 0) ∧ x - y < 0))
∨ (∃l,l':ℕ List
    ∃a:ℕ
     (((l @ [a / l']) = s1 ∈ (ℕ List))
     ∧ (∀y1∈l.y1 - y < 0)
     ∧ ((0 < a - y ∧ (x ∈ [y; [a / l']])) ∨ (((a - y) = 0 ∈ ℤ) ∧ (x ∈ [y / l'])))))
∨ ((x = y ∈ ℕ) ∧ (∀y1∈s1.y1 - y < 0)))@i
⊢ ¬(x ∈ s1)

3
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
7. ¬(x = y ∈ ℕ)@i
8. x ≤ m@i
9. ¬(x ∈ s1)@i
⊢ ¬((∃l:ℕ List. (l @ [x] ≤ s1 ∧ (∀y1∈l.y1 - y < 0) ∧ x - y < 0))
∨ (∃l,l':ℕ List
    ∃a:ℕ
     (((l @ [a / l']) = s1 ∈ (ℕ List))
     ∧ (∀y1∈l.y1 - y < 0)
     ∧ ((0 < a - y ∧ (x ∈ [y; [a / l']])) ∨ (((a - y) = 0 ∈ ℤ) ∧ (x ∈ [y / l'])))))
∨ ((x = y ∈ ℕ) ∧ (∀y1∈s1.y1 - y < 0)))

---

Latex:



1.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\}  @i
2.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\}  @i
3.  x  :  \mBbbN{}@i
4.  y  :  \mBbbN{}@i
5.  \mneg{}m  <  y
6.  y  \mneq{}  m
\mvdash{}  (x  \mleq{}  m)
    \mwedge{}  (\mneg{}((\mexists{}l:\mBbbN{}  List
                  (l  @  [x]  \mleq{}  s1
                  \mwedge{}  (\mforall{}y1\mmember{}l.int-minus-comparison-inc(\mlambda{}x.x)  y  y1  <  0)
                  \mwedge{}  int-minus-comparison-inc(\mlambda{}x.x)  y  x  <  0))
        \mvee{}  (\mexists{}l,l':\mBbbN{}  List
                \mexists{}a:\mBbbN{}
                  (((l  @  [a  /  l'])  =  s1)
                  \mwedge{}  (\mforall{}y1\mmember{}l.int-minus-comparison-inc(\mlambda{}x.x)  y  y1  <  0)
                  \mwedge{}  ((0  <  int-minus-comparison-inc(\mlambda{}x.x)  y  a  \mwedge{}  (x  \mmember{}  [y;  [a  /  l']]))
                      \mvee{}  (((int-minus-comparison-inc(\mlambda{}x.x)  y  a)  =  0)  \mwedge{}  (x  \mmember{}  [y  /  l'])))))
        \mvee{}  ((x  =  y)  \mwedge{}  (\mforall{}y1\mmember{}s1.int-minus-comparison-inc(\mlambda{}x.x)  y  y1  <  0))))
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (x  \mleq{}  m)  \mwedge{}  (\mneg{}(x  \mmember{}  s1))


By

(RepUR  ``int-minus-comparison-inc``  0  THEN  Auto)

---

Home Index