---

Step * 1 of Lemma add-nat-missing-prop


1. s : nat-missing-type()@i
2. x : ℕ@i
3. y : ℕ@i
4. ↑member-nat-missing(x;add-nat-missing(y;s))@i
⊢ (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s))
BY
{ (All(RepUR ``member-nat-missing nat-missing-type add-nat-missing``)
   THEN DProdsAndUnions
   THEN AllReduce
   THEN (SplitOnHypITE (-1) THENA Auto)
   THEN Reduce (-2)
   THEN Try ((SplitOnHypITE (-2) THENA Auto))
   THEN Reduce (-3)
   THEN Repeat (AllPushDown)
   THEN Auto
   THEN (All(RWO "assert-in-missing-nat-iff") THENA Auto)) }

1
.....wf..... 
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. x ≤ y
6. ¬↑in-missing(x;s1 @ [m + 1, y))
7. m < y
8. (x ∈ s1 @ [m + 1, y))@i
⊢ s1 @ [m + 1, y) ∈ {l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} 

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. x ≤ y
6. ¬(x ∈ s1 @ [m + 1, y))
7. m < y
⊢ (x = y ∈ ℕ) ∨ ((x ≤ m) ∧ (¬(x ∈ s1)))

3
.....wf..... 
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. x ≤ m
6. ¬↑in-missing(x;remove-combine(λx.(x - y);s1))
7. ¬m < y
8. ¬(m = y ∈ ℤ)
9. (x ∈ remove-combine(λx.(x - y);s1))@i
⊢ remove-combine(λx.(x - y);s1) ∈ {l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} 

4
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. x ≤ m
6. ¬(x ∈ remove-combine(λx.(x - y);s1))
7. ¬m < y
8. ¬(m = y ∈ ℤ)
⊢ (x = y ∈ ℕ) ∨ ((x ≤ m) ∧ (¬(x ∈ s1)))

---

Latex:



1.  s  :  nat-missing-type()@i
2.  x  :  \mBbbN{}@i
3.  y  :  \mBbbN{}@i
4.  \muparrow{}member-nat-missing(x;add-nat-missing(y;s))@i
\mvdash{}  (x  =  y)  \mvee{}  (\muparrow{}member-nat-missing(x;s))


By

(All(RepUR  ``member-nat-missing  nat-missing-type  add-nat-missing``)
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  (SplitOnHypITE  (-1)  THENA  Auto)
  THEN  Reduce  (-2)
  THEN  Try  ((SplitOnHypITE  (-2)  THENA  Auto))
  THEN  Reduce  (-3)
  THEN  Repeat  (AllPushDown)
  THEN  Auto
  THEN  (All(RWO  "assert-in-missing-nat-iff")  THENA  Auto))

---

Home Index