---

Step * of Lemma mk-set_wf

∀[Item:Type]. ∀[set:{s:Type| valueall-type(Item) ⇒ valueall-type(s)} ]. ∀[member:Item ─→ set ─→ 𝔹].
∀[empty:{s:set| ∀x:Item. (¬↑(member x s))} ]. ∀[isEmpty:{f:set ─→ 𝔹| ∀s:set. (↑(f s) ⇐⇒ ∀x:Item. (¬↑(member x s)))} ].
∀[singleton:{f:Item ─→ set| ∀x,y:Item.  (↑(member x (f y)) ⇐⇒ x = y ∈ Item)} ]. ∀[add:{f:Item ─→ set ─→ set| 
                                                                                       ∀s:set. ∀x,y:Item.
                                                                                         (↑(member x (f y s))
                                                                                         ⇐⇒ (x = y ∈ Item)
                                                                                             ∨ (↑(member x s)))} ].
∀[union:{f:set ─→ set ─→ set| ∀s1,s2:set. ∀x:Item.  (↑(member x (f s1 s2)) ⇐⇒ (↑(member x s1)) ∨ (↑(member x s2)))} ].
∀[remove:{f:Item ─→ set ─→ set| ∀s:set. ∀x,y:Item.  (↑(member x (f y s)) ⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(member x s)))} ].
  (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ∈ set-sig{i:l}(Item))
BY
{ (Auto
   THEN RepUR ``mk-set set-sig`` 0
   THEN Repeat ((RecordPlusTypeCD' THEN Reduce 0 THEN Try (Trivial)))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:


\mforall{}[Item:Type].  \mforall{}[set:\{s:Type|  valueall-type(Item)  {}\mRightarrow{}  valueall-type(s)\}  ].  \mforall{}[member:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[empty:\{s:set|  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s))\}  ].  \mforall{}[isEmpty:\{f:set  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                \mforall{}s:set
                                                                                                                    (\muparrow{}(f  s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s)))\}  ].
\mforall{}[singleton:\{f:Item  {}\mrightarrow{}  set|  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y))  \mLeftarrow{}{}\mRightarrow{}  x  =  y)\}  ].
\mforall{}[add:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
              \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}(member  x  s)))\}  ].
\mforall{}[union:\{f:set  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                  \mforall{}s1,s2:set.  \mforall{}x:Item.    (\muparrow{}(member  x  (f  s1  s2))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(member  x  s1))  \mvee{}  (\muparrow{}(member  x  s2)))\}  ].
\mforall{}[remove:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                    \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}(member  x  s)))\}  ].
    (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove)  \mmember{}  set-sig\{i:l\}(Item))


By

(Auto
  THEN  RepUR  ``mk-set  set-sig``  0
  THEN  Repeat  ((RecordPlusTypeCD'  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index