---

Step * of Lemma super-fact-unroll

∀[n:ℕ+]. ((n)!! ~ (n)! * (n - 1)!!)
BY
{ xxx(Auto
      THEN RW (AddrC [2] UnfoldTopAbC) 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN Reduce 0
      THEN Fold `super-fact` 0
      THEN AutoSplit)xxx }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  ((n)!!  \msim{}  (n)!  *  (n  -  1)!!)


By

---

Latex:
xxx(Auto
        THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  Fold  `super-fact`  0
        THEN  AutoSplit)xxx

---

Home Index