fact: Fixpoint rCompSeval' n (u : nat*rComp) : (nat *rComp)*bool:= match n with S n => match u with | (l, rCompApp s t) => match rCompSeval' n (0,s),rCompSeval' n (0,t) with (i, s',true),(j, t',true) => match rCompBeta s' t' with Some u => rCompSeval' n ((S l)+(i+j),u) | None => ((l+(i+j),s' t'),false) end | ((i,s'),_),((j,t'),_) => ((l+(i+j),s' t'),false) end | (l, rCompClos (rApp s t) A ) => rCompSeval' n (l, rCompApp (rCompClos s A) (rCompClos t A)) | (l , rCompClos (rVar x) A )=> (l,nth x A (rCompVar x),true) | (l, rCompClos (rConst x) A )=> (u,true) | (l, rCompVar x ) => (u,true) | (l, rCompClos (rLam _) A) => (u,true) | (l, rCompClos (rRho _) A) => (u,true) end | 0 => (u,true) end.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd