---

Step * of Lemma bind-class-assoc

∀[Info,T,S,U:Type]. ∀[X:EClass(T)]. ∀[Y:T ─→ EClass(S)]. ∀[Z:S ─→ EClass(U)].
  (X >x> Y[x] >y> Z[y] = X >x> Y[x] >y> Z[y] ∈ EClass(U))
BY
{ (Auto
   THEN RepUR ``bind-class eclass`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN (Assert ⌈≤loc(e) ∈ bag({e':E| e' ≤loc e } )⌉⋅ BY
               (SubsumeC ⌈{e':E| e' ≤loc e }  List⌉⋅
                THEN Try ((BLemma `list-subtype-bag` THEN Auto))
                THEN (BLemma `list_set_type` THEN Auto)
                THEN BLemma `l_all_iff`
                THEN Auto
                THEN (BLemma `member-es-le-before` THEN Auto)⋅))⋅
   THEN All (Unfold `eclass`)) }

1
1. Info : Type
2. T : Type
3. S : Type
4. U : Type
5. X : es:EO+(Info) ─→ e:E ─→ bag(T)
6. Y : T ─→ es:EO+(Info) ─→ e:E ─→ bag(S)
7. Z : S ─→ es:EO+(Info) ─→ e:E ─→ bag(U)
8. es : EO+(Info)@i'
9. e : E@i
10. ≤loc(e) ∈ bag({e':E| e' ≤loc e } )
⊢ ∪e'∈≤loc(e).∪y∈∪e'@0∈≤loc(e').∪x∈X es e'@0.Y[x] es.e'@0 e'.Z[y] es.e' e
= ∪e'∈≤loc(e).∪x∈X es e'.∪e'@0∈≤loc(e).∪y∈Y[x] es.e' e'@0.Z[y] es.e'.e'@0 e
∈ bag(U)

---

Latex:


\mforall{}[Info,T,S,U:Type].  \mforall{}[X:EClass(T)].  \mforall{}[Y:T  {}\mrightarrow{}  EClass(S)].  \mforall{}[Z:S  {}\mrightarrow{}  EClass(U)].
    (X  >x>  Y[x]  >y>  Z[y]  =  X  >x>  Y[x]  >y>  Z[y])


By

(Auto
  THEN  RepUR  ``bind-class  eclass``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}\mleq{}loc(e)  \mmember{}  bag(\{e':E|  e'  \mleq{}loc  e  \}  )\mkleeneclose{}\mcdot{}  BY
                          (SubsumeC  \mkleeneopen{}\{e':E|  e'  \mleq{}loc  e  \}    List\mkleeneclose{}\mcdot{}
                            THEN  Try  ((BLemma  `list-subtype-bag`  THEN  Auto))
                            THEN  (BLemma  `list\_set\_type`  THEN  Auto)
                            THEN  BLemma  `l\_all\_iff`
                            THEN  Auto
                            THEN  (BLemma  `member-es-le-before`  THEN  Auto)\mcdot{}))\mcdot{}
  THEN  All  (Unfold  `eclass`))

---

Home Index