---

Step * 4 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
⊢ ↑member-nat-missing(x;<m, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;y;s1)>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-\000Cnat-missing(x;<m, s1>))
BY
{ (RWO "assert-member-nat-missing" 0
   THEN AllReduce
   THEN Try (Complete (Auto))
   THEN Try (((RW ListC 0 THENA Auto) THEN Reduce 0))
   THEN Try (Complete ((DVarSets
                        THEN Auto
                        THEN MemTypeCD
                        THEN Auto
                        THEN Try (Complete ((BLemma `l-ordered-insert-combine`
                                             THEN Auto
                                             THEN All(RepUR ``int-minus-comparison-inc``)
                                             THEN Auto')))
                        THEN (All(RWO "l_all_iff") THEN Auto)
                        THEN (FLemma `member-insert-combine` [-1] THENA Auto)
                        THEN DProdsAndUnions
                        THEN Try (Complete (Auto'))
                        THEN Try (Complete ((BackThruSomeHyp⋅ THEN Auto)))
                        THEN Reduce (-1)
                        THEN (RWO "l_exists_iff" (-1) THENA Auto)
                        THEN ExRepD
                        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
⊢ (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))

---

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{}  \muparrow{}member-nat-missing(x;<m,  insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;y;s1)>)
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}member-nat-missing(x;<m,  s1>))


By

(RWO  "assert-member-nat-missing"  0
  THEN  AllReduce
  THEN  Try  (Complete  (Auto))
  THEN  Try  (((RW  ListC  0  THENA  Auto)  THEN  Reduce  0))
  THEN  Try  (Complete  ((DVarSets
                                            THEN  Auto
                                            THEN  MemTypeCD
                                            THEN  Auto
                                            THEN  Try  (Complete  ((BLemma  `l-ordered-insert-combine`
                                                                                      THEN  Auto
                                                                                      THEN  All(RepUR  ``int-minus-comparison-inc``)
                                                                                      THEN  Auto')))
                                            THEN  (All(RWO  "l\_all\_iff")  THEN  Auto)
                                            THEN  (FLemma  `member-insert-combine`  [-1]  THENA  Auto)
                                            THEN  DProdsAndUnions
                                            THEN  Try  (Complete  (Auto'))
                                            THEN  Try  (Complete  ((BackThruSomeHyp\mcdot{}  THEN  Auto)))
                                            THEN  Reduce  (-1)
                                            THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
                                            THEN  ExRepD
                                            THEN  Auto'))))

---

Home Index