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