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


1. {m:ℤ(-1) ≤ m} @i
2. s1 {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. : ℕ@i
4. : ℕ@i
5. x ≤ m
6. ¬(x ∈ remove-combine(λx.(x y);s1))
7. ¬m < y
8. ¬(m y ∈ ℤ)
⊢ (x y ∈ ℕ) ∨ ((x ≤ m) ∧ (x ∈ s1)))
BY
((Decide ⌈y ∈ ℕ⌉⋅ THEN Auto)
   THEN ParallelOp -5
   THEN BLemma `remove-combine-implies-member2`
   THEN Reduce 0
   THEN Auto) }


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.  x  \mleq{}  m
6.  \mneg{}(x  \mmember{}  remove-combine(\mlambda{}x.(x  -  y);s1))
7.  \mneg{}m  <  y
8.  \mneg{}(m  =  y)
\mvdash{}  (x  =  y)  \mvee{}  ((x  \mleq{}  m)  \mwedge{}  (\mneg{}(x  \mmember{}  s1)))


By

((Decide  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  ParallelOp  -5
  THEN  BLemma  `remove-combine-implies-member2`
  THEN  Reduce  0
  THEN  Auto)




Home Index