---

Step * of Lemma mk-set-nat-missing_wf

mk-set-nat-missing() ∈ set-sig{i:l}(ℕ)
BY
{ (RepUR ``mk-set-nat-missing let`` 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN AllReduce
   THEN Try (Complete ((BLemma `empty-nat-missing-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `isEmpty-nat-missing-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `singleton-nat-missing-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `add-nat-missing-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `union-nat-missing-prop` THEN Auto)))
   THEN Try (Complete ((RWO "remove-nat-missing-prop" (-1) THEN Auto)))
   THEN Try (Complete ((RWO "remove-nat-missing-prop" 0 THEN Auto)))) }

---

Latex:


mk-set-nat-missing()  \mmember{}  set-sig\{i:l\}(\mBbbN{})


By

(RepUR  ``mk-set-nat-missing  let``  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  AllReduce
  THEN  Try  (Complete  ((BLemma  `empty-nat-missing-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `isEmpty-nat-missing-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `singleton-nat-missing-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `add-nat-missing-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `union-nat-missing-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((RWO  "remove-nat-missing-prop"  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((RWO  "remove-nat-missing-prop"  0  THEN  Auto))))

---

Home Index