---

Step * of Lemma map-simplify-test

∀[H,f,g:Base]. ∀[L:Atom List].  (map(λx.H[if x ∈b L then f[x] else g[x] fi ];L) ~ map(λx.H[f[x]];L))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN BLemma `map_functionality_wrt_sq` THEN Reduce 0 THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[H,f,g:Base].  \mforall{}[L:Atom  List].    (map(\mlambda{}x.H[if  x  \mmember{}\msubb{}  L  then  f[x]  else  g[x]  fi  ];L)  \msim{}  map(\mlambda{}x.H[f[x]];L))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  BLemma  `map\_functionality\_wrt\_sq`
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))

---

Home Index