---

Step * of Lemma set-sig-add-prop

∀[Item:Type]
  ∀s:set-sig{i:l}(Item). ∀set:set-sig-set(s). ∀x,y:Item.
    (↑(set-sig-member(s) x (set-sig-add(s) y set)) ⇐⇒ (x = y ∈ Item) ∨ (↑(set-sig-member(s) x set)))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌈s ∈ set-sig{i:l}(Item)⌉⋅ THENA Auto)
   THEN (D 2 THENA Auto)
   THEN DVarSets
   THEN (Unhide THENA Auto)
   THEN Try (Complete (((BoolCase ⌈set-sig-member(s) x set⌉⋅ THENA Auto) THEN D 0 THEN Auto THEN D (-1) THEN Auto)))
   THEN All(Folds ``set-sig-member set-sig-add set-sig-set``)
   THEN RWO "-5" 0
   THEN Auto) }

---

Latex:


\mforall{}[Item:Type]
    \mforall{}s:set-sig\{i:l\}(Item).  \mforall{}set:set-sig-set(s).  \mforall{}x,y:Item.
        (\muparrow{}(set-sig-member(s)  x  (set-sig-add(s)  y  set))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}(set-sig-member(s)  x  set)))


By

((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}s  \mmember{}  set-sig\{i:l\}(Item)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  2  THENA  Auto)
  THEN  DVarSets
  THEN  (Unhide  THENA  Auto)
  THEN  Try  (Complete  (((BoolCase  \mkleeneopen{}set-sig-member(s)  x  set\mkleeneclose{}\mcdot{}  THENA  Auto)
                                            THEN  D  0
                                            THEN  Auto
                                            THEN  D  (-1)
                                            THEN  Auto)))
  THEN  All(Folds  ``set-sig-member  set-sig-add  set-sig-set``)
  THEN  RWO  "-5"  0
  THEN  Auto)

---

Home Index