---

Step * of Lemma combine-reduce

∀[F,f,g,x,y:Top]. ∀[L:Top List].
  (F reduce(f;x;L) reduce(g;y;L) ~ (λz.let x,y = z in F x y) reduce(λu,z. let x,y = z in <f u x, g u y>;<x, y>;L))
BY
{ xxx(RepeatFor 5 ((D 0 THENA Auto))
      THEN (Assert ∀L:Top List. (reduce(λu,z. let x,y = z in <f u x, g u y>;<x, y>;L) ~ <reduce(f;x;L), reduce(g;y;L)>) \000CBY
                  (InductionOnList THEN Reduce 0 THEN Try (Trivial) THEN RWO "-1" 0 THEN Reduce 0 THEN Trivial))
      THEN ParallelLast
      THEN RWO "-1" 0
      THEN Reduce 0
      THEN Trivial)xxx }

---

Latex:

---

Latex:
\mforall{}[F,f,g,x,y:Top].  \mforall{}[L:Top  List].
    (F  reduce(f;x;L)  reduce(g;y;L)  \msim{}  (\mlambda{}z.let  x,y  =  z 
                                                                              in  F  x  y) 
                                                                      reduce(\mlambda{}u,z.  let  x,y  =  z  in  <f  u  x,  g  u  y><x,  y>L))


By

---

Latex:
xxx(RepeatFor  5  ((D  0  THENA  Auto))
        THEN  (Assert  \mforall{}L:Top  List.  (reduce(\mlambda{}u,z.  let  x,y  =  z  in  <f  u  x,  g  u  y><x,  y>L)  \msim{}  <reduce(f;x;L)\000C,  reduce(g;y;L)>)  BY
                                (InductionOnList
                                  THEN  Reduce  0
                                  THEN  Try  (Trivial)
                                  THEN  RWO  "-1"  0
                                  THEN  Reduce  0
                                  THEN  Trivial))
        THEN  ParallelLast
        THEN  RWO  "-1"  0
        THEN  Reduce  0
        THEN  Trivial)xxx

---

Home Index