---

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


1. s : nat-missing-type()@i
2. x : ℕ@i
3. y : ℕ@i
4. (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s))@i
⊢ ↑member-nat-missing(x;add-nat-missing(y;s))
BY
{ (All(RepUR ``member-nat-missing nat-missing-type add-nat-missing``)
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Repeat (AutoSplit)
   THEN AllReduce
   THEN Repeat (AllPushDown)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN DVarSets
   THEN (RWO "assert-in-missing-nat-iff" (-1)
         THENA (Auto
                THEN (MemTypeCD THEN Auto)
                THEN Repeat ((RW ListC 0 THEN Auto))
                THEN (All(RWO "l_all_iff") THENA Auto)
                THEN (Try (RW ListC (-1)) THENA Auto)
                THEN Try (OnSomeHyp(\i.InstHyp [⌈x1⌉] i THEN CpltAuto)⋅)
                THEN Try ((BLemma `l-ordered-remove-combine` THEN Auto)))
         )
   THEN Try ((FLemma `remove-combine-implies-member` [-1] THENA Auto))
   THEN (All(RWO "assert-in-missing-nat-iff")⋅ THENA Auto)
   THEN Try ((RW ListC (-1) THENA Auto))
   THEN (All(RWO "l_all_iff") THENA Auto)
   THEN Try (DProdsAndUnions)
   THEN Try (OnSomeHyp(\i.InstHyp [⌈x⌉] i THEN CpltAuto)⋅)
   THEN Try ((RW ListC (-1) THENA Auto))
   THEN Auto
   THEN FLemma `remove-combine-l-ordered-implies-member` [-2]
   THEN AllReduce
   THEN Auto
   THEN (All(Unfold `l-ordered`) THEN Auto)
   THEN OnSomeHyp(\i.InstHyp [⌈x1⌉;⌈y@0⌉] i THEN CpltAuto)⋅) }

---

Latex:



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


By

(All(RepUR  ``member-nat-missing  nat-missing-type  add-nat-missing``)
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Repeat  (AutoSplit)
  THEN  AllReduce
  THEN  Repeat  (AllPushDown)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  DVarSets
  THEN  (RWO  "assert-in-missing-nat-iff"  (-1)
              THENA  (Auto
                            THEN  (MemTypeCD  THEN  Auto)
                            THEN  Repeat  ((RW  ListC  0  THEN  Auto))
                            THEN  (All(RWO  "l\_all\_iff")  THENA  Auto)
                            THEN  (Try  (RW  ListC  (-1))  THENA  Auto)
                            THEN  Try  (OnSomeHyp(\mbackslash{}i.InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  i  THEN  CpltAuto)\mcdot{})
                            THEN  Try  ((BLemma  `l-ordered-remove-combine`  THEN  Auto)))
              )
  THEN  Try  ((FLemma  `remove-combine-implies-member`  [-1]  THENA  Auto))
  THEN  (All(RWO  "assert-in-missing-nat-iff")\mcdot{}  THENA  Auto)
  THEN  Try  ((RW  ListC  (-1)  THENA  Auto))
  THEN  (All(RWO  "l\_all\_iff")  THENA  Auto)
  THEN  Try  (DProdsAndUnions)
  THEN  Try  (OnSomeHyp(\mbackslash{}i.InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  i  THEN  CpltAuto)\mcdot{})
  THEN  Try  ((RW  ListC  (-1)  THENA  Auto))
  THEN  Auto
  THEN  FLemma  `remove-combine-l-ordered-implies-member`  [-2]
  THEN  AllReduce
  THEN  Auto
  THEN  (All(Unfold  `l-ordered`)  THEN  Auto)
  THEN  OnSomeHyp(\mbackslash{}i.InstHyp  [\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y@0\mkleeneclose{}]  i  THEN  CpltAuto)\mcdot{})

---

Home Index