---

Step * of Lemma test-mutual-corec-ext

test-mutual-corec() ≡ λi.if (i =z 0)
                         then Unit + (test-mutual-corec() 0 × ((test-mutual-corec() 1) List))
                         else Unit + (test-mutual-corec() 1 × ((test-mutual-corec() 0) List))
                         fi 
BY
{ ProveMutualCorecExt }

---

Latex:

---

Latex:
test-mutual-corec()  \mequiv{}  \mlambda{}i.if  (i  =\msubz{}  0)
                                                  then  Unit  +  (test-mutual-corec()  0  \mtimes{}  ((test-mutual-corec()  1)  List))
                                                  else  Unit  +  (test-mutual-corec()  1  \mtimes{}  ((test-mutual-corec()  0)  List))
                                                  fi 


By

---

Latex:
ProveMutualCorecExt

---

Home Index