---

Step * 1 of Lemma fact0_redex_lemma

(0)! ~ 1
BY
{ (RW (AddrC [1] (UnfoldC `fact` ANDTHENC ReduceC)) 0⋅ THENM Complete (Auto)) }

---

Latex:

---

Latex:
(0)!  \msim{}  1


By

---

Latex:
(RW  (AddrC  [1]  (UnfoldC  `fact`  ANDTHENC  ReduceC))  0\mcdot{}  THENM  Complete  (Auto))

---

Home Index