Step * 1 of Lemma bag_combine_empty_lemma


1. Top@i
⊢ ⋃x∈{}.f[x] {}
BY
Try (RW (AddrC [1] (UnfoldC `bag-combine` ANDTHENC ReduceC)) 0)⋅ }

1
1. Top@i
⊢ {} {}


Latex:


Latex:

1.  f  :  Top@i
\mvdash{}  \mcup{}x\mmember{}\{\}.f[x]  \msim{}  \{\}


By


Latex:
Try  (RW  (AddrC  [1]  (UnfoldC  `bag-combine`  ANDTHENC  ReduceC))  0)\mcdot{}




Home Index