---

Step * of Lemma prank-pvar

∀[a:formula()]. uiff(prank(a) = 0 ∈ ℤ;↑pvar?(a))
BY
{ ((D 0 THENA Auto)
   THEN MoveToConcl (-1)
   THEN (BLemma `formula-induction` THENA Auto)
   THEN Unfold `prank` 0
   THEN Reduce 0
   THEN Try (Fold `prank` 0)
   THEN Auto'
   THEN (RWO "imax_unfold" (-1) THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a:formula()].  uiff(prank(a)  =  0;\muparrow{}pvar?(a))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (BLemma  `formula-induction`  THENA  Auto)
  THEN  Unfold  `prank`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `prank`  0)
  THEN  Auto'
  THEN  (RWO  "imax\_unfold"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto')

---

Home Index