[Item:Type]
∀s:set-sig{i:l}(Item). ∀set:set-sig-set(s). ∀x,y:Item.
(↑(set-sig-member(s) (set-sig-add(s) set)) ⇐⇒ (x y ∈ Item) ∨ (↑(set-sig-member(s) set)))

Proof

Definitions occuring in Statement :  set-sig-add: set-sig-add(s) set-sig-member: set-sig-member(s) set-sig-set: set-sig-set(s) set-sig: set-sig{i:l}(Item) assert: b uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q apply: a universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T set-sig: set-sig{i:l}(Item) record+: record+ record-select: r.x subtype_rel: A ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt implies:  Q guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] prop: iff: ⇐⇒ Q rev_implies:  Q and: P ∧ Q or: P ∨ Q squash: T bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) uimplies: supposing a assert: b sq_stable: SqStable(P) true: True bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb false: False set-sig-member: set-sig-member(s) set-sig-set: set-sig-set(s) set-sig-add: set-sig-add(s)

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)))

Date html generated: 2016_05_17-PM-01_44_31
Last ObjectModification: 2016_01_17-AM-11_37_40

Theory : datatype-signatures

Home Index