---

{ [as1:Top List]. [as2,P:Top].  (P*(as1 @ as2) ~ P*(as1)*(as2)) }

{ Proof }

---

Definitions occuring in Statement :  iterate-dataflow: P*(inputs),  append: as @ bs,  uall: [x:A]. B[x],  top: Top,  list: type List,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  top: Top,  append: as @ bs,  member: t  T
Lemmas :  top_wf

---

\mforall{}[as1:Top  List].  \mforall{}[as2,P:Top].    (P*(as1  @  as2)  \msim{}  P*(as1)*(as2))


Date html generated: 2011_08_10-AM-08_14_18
Last ObjectModification: 2011_06_18-AM-08_29_53

Home Index