---

Step * of Lemma RankEx4-ext

RankEx4() ≡ lbl:Atom × if lbl =a "Foo" then ℤ + RankEx4() else Void fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
RankEx4()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Foo"  then  \mBbbZ{}  +  RankEx4()  else  Void  fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index