---

Step * 1 of Lemma member-mapfilter-witness_wf


TERMOF{member-mapfilter-univ:o, 1:l, 1:l} ~ TERMOF{member-mapfilter-univ:o, 1:l, i:l}
BY
{ (RW  (SubC (SymbCompC [] 100)) 0
   THEN RepeatFor 10 ((RW  (SubC (SymbCompC [] 5)) 0 THEN RepeatFor 3 (EqCD) THEN Reduce 0 THEN Try (Trivial)))
   ) }

---

Latex:

---

Latex:

TERMOF\{member-mapfilter-univ:o,  1:l,  1:l\}  \msim{}  TERMOF\{member-mapfilter-univ:o,  1:l,  i:l\}


By

---

Latex:
(RW    (SubC  (SymbCompC  []  100))  0
  THEN  RepeatFor  10  ((RW    (SubC  (SymbCompC  []  5))  0
                                          THEN  RepeatFor  3  (EqCD)
                                          THEN  Reduce  0
                                          THEN  Try  (Trivial)))
  )

---

Home Index