Twelf 1.5R3, Aug 30, 2005 (%trustme) %% OK %% [Opening file /home/www/twelf/hcode/7060c1743be206623aab396ecd32723d] tp : type. nat : tp. arr : tp -> tp -> tp. exp : type. z : exp. s : exp -> exp. ifz : exp -> exp -> (exp -> exp) -> exp. fun : tp -> tp -> (exp -> exp -> exp) -> exp. app : exp -> exp -> exp. of : exp -> tp -> type. %mode +{E:exp} -{T:tp} (of E T). of/z : of z nat. of/s : {E:exp} of E nat -> of (s E) nat. of/ifz : {E2:exp -> exp} {T:tp} {E1:exp} {E:exp} ({x:exp} of x nat -> of (E2 x) T) -> of E1 T -> of E nat -> of (ifz E E1 ([x:exp] E2 x)) T. of/fun : {T1:tp} {T2:tp} {E:exp -> exp -> exp} ({f:exp} of f (arr T1 T2) -> ({x:exp} of x T1 -> of (E f x) T2)) -> of (fun T1 T2 ([f:exp] [x:exp] E f x)) (arr T1 T2). of/app : {E2:exp} {T2:tp} {E1:exp} {T:tp} of E2 T2 -> of E1 (arr T2 T) -> of (app E1 E2) T. value : exp -> type. %mode +{E:exp} (value E). value/z : value z. value/s : {E:exp} value E -> value (s E). value/fun : {T1:tp} {T2:tp} {E1:exp -> exp -> exp} value (fun T1 T2 ([e:exp] [e1:exp] E1 e e1)). step : exp -> exp -> type. %mode +{E1:exp} -{E2:exp} (step E1 E2). step/s : {E:exp} {E':exp} step E E' -> step (s E) (s E'). step/ifz/arg : {E:exp} {E':exp} {E1:exp} {E2:exp -> exp} step E E' -> step (ifz E E1 ([x:exp] E2 x)) (ifz E' E1 ([x:exp] E2 x)). step/ifz/z : {E1:exp} {E2:exp -> exp} step (ifz z E1 ([x:exp] E2 x)) E1. step/ifz/s : {E:exp} {E1:exp} {E2:exp -> exp} value E -> step (ifz (s E) E1 ([x:exp] E2 x)) (E2 E). step/app/fun : {E1:exp} {E1':exp} {E2:exp} step E1 E1' -> step (app E1 E2) (app E1' E2). step/app/arg : {E2:exp} {E2':exp} {E1:exp} step E2 E2' -> value E1 -> step (app E1 E2) (app E1 E2'). step/app/beta-v : {E2:exp} {T1:tp} {T2:tp} {E:exp -> exp -> exp} value E2 -> step (app (fun T1 T2 ([f:exp] [x:exp] E f x)) E2) (E (fun T1 T2 ([f:exp] [x:exp] E f x)) E2). pres : {E:exp} {E':exp} {T:tp} step E E' -> of E T -> of E' T -> type. %mode +{E:exp} +{E':exp} +{T:tp} +{Dstep:step E E'} +{Dof:of E T} -{Dof1:of E' T} (pres Dstep Dof Dof1). - : {E1:exp} {E2:exp} {Dstep:step E1 E2} {Dof:of E1 nat} {Dof':of E2 nat} pres Dstep Dof Dof' -> pres (step/s Dstep) (of/s Dof) (of/s Dof'). - : {E1:exp} {E2:exp} {Dstep:step E1 E2} {Dof:of E1 nat} {Dof':of E2 nat} {E3:exp} {E4:exp -> exp} {T1:tp} {Dof2:{e:exp} of e nat -> of (E4 e) T1} {Dof1:of E3 T1} pres Dstep Dof Dof' -> pres (step/ifz/arg Dstep) (of/ifz ([x:exp] [dx:of x nat] Dof2 x dx) Dof1 Dof) (of/ifz ([x:exp] [dx:of x nat] Dof2 x dx) Dof1 Dof'). - : {E1:exp} {E2:exp -> exp} {T1:tp} {Dof1:{x:exp} of x nat -> of (E2 x) T1} {Dof2:of E1 T1} {Dof3:of z nat} pres step/ifz/z (of/ifz ([x:exp] [dof:of x nat] Dof1 x dof) Dof2 Dof3) Dof2. - : {E:exp} {E1:exp} {E2:exp -> exp} {T1:tp} {Dval1:value E} {Dof2:{e:exp} of e nat -> of (E2 e) T1} {Dof1:of E1 T1} {Dof:of E nat} pres (step/ifz/s Dval1) (of/ifz ([x:exp] [dx:of x nat] Dof2 x dx) Dof1 (of/s Dof)) (Dof2 E Dof). - : {E1:exp} {E2:exp} {T1:tp} {T2:tp} {Dstep1:step E1 E2} {Dof1:of E1 (arr T1 T2)} {Dof1':of E2 (arr T1 T2)} {E3:exp} {Dof2:of E3 T1} pres Dstep1 Dof1 Dof1' -> pres (step/app/fun Dstep1) (of/app Dof2 Dof1) (of/app Dof2 Dof1'). - : {E1:exp} {E2:exp} {T1:tp} {Dstep2:step E1 E2} {Dof2:of E1 T1} {Dof2':of E2 T1} {E3:exp} {T2:tp} {Dval1:value E3} {Dof1:of E3 (arr T1 T2)} pres Dstep2 Dof2 Dof2' -> pres (step/app/arg Dstep2 Dval1) (of/app Dof2 Dof1) (of/app Dof2' Dof1). - : {T1:tp} {T2:tp} {E1:exp -> exp -> exp} {E2:exp} {Dval1:value E2} {Dof2:of E2 T1} {Dof1:{e:exp} of e (arr T1 T2) -> ({e1:exp} of e1 T1 -> of (E1 e e1) T2)} pres (step/app/beta-v Dval1) (of/app Dof2 (of/fun ([f:exp] [df:of f (arr T1 T2)] [x:exp] [dx:of x T1] Dof1 f df x dx))) (Dof1 (fun T1 T2 ([f:exp] [x:exp] E1 f x)) (of/fun ([f:exp] [df:of f (arr T1 T2)] [x:exp] [dx:of x T1] Dof1 f df x dx)) E2 Dof2). %worlds () (pres Dstep Dof Dof'). %total Dstep (pres Dstep _ _). val-or-step : exp -> type. vos/val : {E:exp} value E -> val-or-step E. vos/step : {E:exp} {E1:exp} step E E1 -> val-or-step E. prog/s : {E:exp} val-or-step E -> val-or-step (s E) -> type. %mode +{E:exp} +{Dvos1:val-or-step E} -{Dvos2:val-or-step (s E)} (prog/s Dvos1 Dvos2). - : {E1:exp} {E2:exp} {Dstep:step E1 E2} prog/s (vos/step Dstep) (vos/step (step/s Dstep)). - : {E1:exp} {Dval:value E1} prog/s (vos/val Dval) (vos/val (value/s Dval)). %worlds () (prog/s _ _). %total {} (prog/s _ _). prog/ifz : {E:exp} {E':exp} of E nat -> val-or-step E -> ({E1:exp} {E2:exp -> exp} step (ifz E E1 ([x:exp] E2 x)) E' -> type). %mode +{E:exp} -{E':exp} +{Dof:of E nat} +{Dvos:val-or-step E} +{E1:exp} +{E2:exp -> exp} -{Dstep:step (ifz E E1 ([x:exp] E2 x)) E'} (prog/ifz Dof Dvos E1 E2 Dstep). - : {E1:exp} {E2:exp} {E3:exp} {E4:exp -> exp} {Dof1:of E1 nat} {Dstep:step E1 E2} prog/ifz Dof1 (vos/step Dstep) E3 ([e:exp] E4 e) (step/ifz/arg Dstep). - : {E1:exp} {Dof1:of z nat} {E2:exp -> exp} prog/ifz Dof1 (vos/val value/z) E1 ([e:exp] E2 e) step/ifz/z. - : {E1:exp} {E2:exp -> exp} {Dof1:of (s E1) nat} {Dval:value E1} {E3:exp} prog/ifz Dof1 (vos/val (value/s Dval)) E3 ([e:exp] E2 e) (step/ifz/s Dval). %worlds () (prog/ifz _ _ _ _ _). %total {} (prog/ifz _ _ _ _ _). prog/app : {E1:exp} {T2:tp} {T:tp} {E2:exp} {E':exp} of E1 (arr T2 T) -> val-or-step E1 -> val-or-step E2 -> step (app E1 E2) E' -> type. %mode +{E1:exp} +{T2:tp} +{T:tp} +{E2:exp} -{E':exp} +{Dof:of E1 (arr T2 T)} +{Dvos1:val-or-step E1} +{Dvos2:val-or-step E2} -{Dstep:step (app E1 E2) E'} (prog/app Dof Dvos1 Dvos2 Dstep). - : {E1:exp} {T1:tp} {T2:tp} {E2:exp} {E3:exp} {Dof1:of E1 (arr T1 T2)} {Dstep1:step E1 E3} {Dvos1:val-or-step E2} prog/app Dof1 (vos/step Dstep1) Dvos1 (step/app/fun Dstep1). - : {E1:exp} {T1:tp} {T2:tp} {E2:exp} {E3:exp} {Dof1:of E1 (arr T1 T2)} {Dval1:value E1} {Dstep2:step E2 E3} prog/app Dof1 (vos/val Dval1) (vos/step Dstep2) (step/app/arg Dstep2 Dval1). - : {T1:tp} {T2:tp} {E1:exp -> exp -> exp} {T3:tp} {T4:tp} {E2:exp} {Dof1:of (fun T1 T2 ([f:exp] [x:exp] E1 f x)) (arr T3 T4)} {Dval1:value (fun T1 T2 ([f:exp] [x:exp] E1 f x))} {Dval2:value E2} prog/app Dof1 (vos/val Dval1) (vos/val Dval2) (step/app/beta-v Dval2). %worlds () (prog/app _ _ _ _). %total {} (prog/app _ _ _ _). prog : {E:exp} {T:tp} of E T -> val-or-step E -> type. %mode +{E:exp} +{T:tp} +{Dof:of E T} -{Dvos:val-or-step E} (prog Dof Dvos). - : prog of/z (vos/val value/z). - : {E1:exp} {Dvos:val-or-step E1} {Dvos':val-or-step (s E1)} {Dof:of E1 nat} prog/s Dvos Dvos' -> prog Dof Dvos -> prog (of/s Dof) Dvos'. - : {E1:exp} {E2:exp} {Dof:of E1 nat} {Dvos:val-or-step E1} {E3:exp} {E4:exp -> exp} {Dstep:step (ifz E1 E3 ([x:exp] E4 x)) E2} {T1:tp} {Dof2:{e:exp} of e nat -> of (E4 e) T1} {Dof1:of E3 T1} prog/ifz Dof Dvos E3 ([e:exp] E4 e) Dstep -> prog Dof Dvos -> prog (of/ifz ([x:exp] [dx:of x nat] Dof2 x dx) Dof1 Dof) (vos/step Dstep). - : {T1:tp} {T2:tp} {E1:exp -> exp -> exp} {Dof1:{f:exp} of f (arr T1 T2) -> ({x:exp} of x T1 -> of (E1 f x) T2)} prog (of/fun ([f:exp] [dof:of f (arr T1 T2)] [x:exp] [dof1:of x T1] Dof1 f dof x dof1)) (vos/val value/fun). - : {E1:exp} {T1:tp} {T2:tp} {E2:exp} {E3:exp} {Dof1:of E1 (arr T1 T2)} {Dvos1:val-or-step E1} {Dvos2:val-or-step E2} {Dstep:step (app E1 E2) E3} {Dof2:of E2 T1} prog/app Dof1 Dvos1 Dvos2 Dstep -> prog Dof2 Dvos2 -> prog Dof1 Dvos1 -> prog (of/app Dof2 Dof1) (vos/step Dstep). %worlds () (prog _ _). %total Dof (prog Dof _). plus : exp = fun nat (arr nat nat) ([plus:exp] [x:exp] ifz x (fun nat nat ([e:exp] [y:exp] y)) ([predx:exp] fun nat nat ([e:exp] [y:exp] s (app (app plus predx) y)))). %solve of (fun nat (arr nat nat) ([plus1:exp] [x:exp] ifz x (fun nat nat ([e:exp] [y:exp] y)) ([predx:exp] fun nat nat ([e:exp] [y:exp] s (app (app plus1 predx) y))))) T. OK D : of (fun nat (arr nat nat) ([plus1:exp] [x:exp] ifz x (fun nat nat ([e:exp] [y:exp] y)) ([predx:exp] fun nat nat ([e:exp] [y:exp] s (app (app plus1 predx) y))))) (arr nat (arr nat nat)) = of/fun ([f:exp] [dof:of f (arr nat (arr nat nat))] [x:exp] [dof1:of x nat] of/ifz ([x2:exp] [dof2:of x2 nat] of/fun ([f2:exp] [dof3:of f2 (arr nat nat)] [x3:exp] [dof4:of x3 nat] of/s (of/app dof4 (of/app dof2 dof)))) (of/fun ([f1:exp] [dof2:of f1 (arr nat nat)] [x1:exp] [dof3:of x1 nat] dof3)) dof1). mult : exp = fun nat (arr nat nat) ([mult:exp] [x:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x1:exp] ifz x1 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx) y2))))) x) (app (app mult x) predy)))). %solve of (fun nat (arr nat nat) ([mult1:exp] [x:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x1:exp] ifz x1 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx) y2))))) x) (app (app mult1 x) predy))))) T. OK Dmult : of (fun nat (arr nat nat) ([mult1:exp] [x:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x1:exp] ifz x1 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx) y2))))) x) (app (app mult1 x) predy))))) (arr nat (arr nat nat)) = of/fun ([f:exp] [dof:of f (arr nat (arr nat nat))] [x:exp] [dof1:of x nat] of/fun ([f1:exp] [dof2:of f1 (arr nat nat)] [x2:exp] [dof3:of x2 nat] of/ifz ([x3:exp] [dof4:of x3 nat] of/app (of/app dof4 (of/app dof1 dof)) (of/app dof1 (of/fun ([f2:exp] [dof5:of f2 (arr nat (arr nat nat))] [x4:exp] [dof6:of x4 nat] of/ifz ([x6:exp] [dof7:of x6 nat] of/fun ([f4:exp] [dof8:of f4 (arr nat nat)] [x7:exp] [dof9:of x7 nat] of/s (of/app dof9 (of/app dof7 dof5)))) (of/fun ([f3:exp] [dof7:of f3 (arr nat nat)] [x5:exp] [dof8:of x5 nat] dof8)) dof6)))) of/z dof3)). fact : exp = fun nat nat ([fact:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact predx))). %solve of (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) T. OK Dfact : of (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ( [e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (arr nat nat) = of/fun ([f:exp] [dof:of f (arr nat nat)] [x:exp] [dof1:of x nat] of/ifz ([x3:exp] [dof2:of x3 nat] of/app (of/app dof2 dof) (of/app dof1 (of/fun ([f1:exp] [dof3:of f1 (arr nat (arr nat nat))] [x4:exp] [dof4:of x4 nat] of/fun ([f2:exp] [dof5:of f2 (arr nat nat)] [x5:exp] [dof6:of x5 nat] of/ifz ([x6:exp] [dof7:of x6 nat] of/app (of/app dof7 (of/app dof4 dof3)) (of/app dof4 (of/fun ([f3:exp] [dof8:of f3 (arr nat (arr nat nat))] [x7:exp] [dof9:of x7 nat] of/ifz ([x9:exp] [dof10:of x9 nat] of/fun ([f5:exp] [dof11:of f5 (arr nat nat)] [x10:exp] [dof12:of x10 nat] of/s (of/app dof12 (of/app dof10 dof8)))) (of/fun ([f4:exp] [dof10:of f4 (arr nat nat)] [x8:exp] [dof11:of x8 nat] dof11)) dof9)))) of/z dof6))))) (of/s of/z) dof1). stepv : exp -> exp -> type. stepv/v : {E:exp} value E -> stepv E E. stepv/s : {E':exp} {E'':exp} {E:exp} stepv E' E'' -> step E E' -> stepv E E''. %solve stepv (app (app (fun nat (arr nat nat) ([plus1:exp] [x:exp] ifz x (fun nat nat ([e:exp] [y:exp] y)) ([predx:exp] fun nat nat ([e:exp] [y:exp] s (app (app plus1 predx) y))))) (s (s z))) (s (s z))) E. OK D : stepv (app (app (fun nat (arr nat nat) ([plus1:exp] [x:exp] ifz x (fun nat nat ([e:exp] [y:exp] y)) ([predx:exp] fun nat nat ([e:exp] [y:exp] s (app (app plus1 predx) y))))) (s (s z))) (s (s z))) (s (s (s (s z)))) = stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/v (value/s (value/s (value/s (value/s value/z))))) (step/s (step/s (step/app/beta-v (value/s (value/s value/z)))))) (step/s (step/s (step/app/fun step/ifz/z)))) (step/s (step/s (step/app/fun (step/app/beta-v value/z))))) (step/s (step/app/beta-v (value/s (value/s value/z))))) (step/s (step/app/fun (step/ifz/s value/z)))) (step/s (step/app/fun (step/app/beta-v (value/s value/z))))) (step/app/beta-v (value/s (value/s value/z)))) (step/app/fun (step/ifz/s (value/s value/z)))) (step/app/fun (step/app/beta-v (value/s (value/s value/z)))). %solve stepv (app (app (fun nat (arr nat nat) ([mult1:exp] [x:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x1:exp] ifz x1 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx) y2))))) x) (app (app mult1 x) predy))))) (s (s (s z)))) (s (s z))) E. OK D : stepv (app (app (fun nat (arr nat nat) ([mult1:exp] [x:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app ( app (fun nat (arr nat nat) ([plus1:exp] [x1:exp] ifz x1 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx) y2))))) x) (app (app mult1 x) predy))))) (s (s (s z)))) (s (s z))) (s (s (s (s (s (s z)))))) = stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/v (value/s (value/s (value/s (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))))) (step/s (step/s (step/s (step/app/fun step/ifz/z))))) (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z)))))) (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/app/fun (step/ifz/s value/z))))) (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z)))))) (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/s (step/app/fun (step/ifz/s (value/s value/z))))) (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z)))))) (step/app/beta-v (value/s (value/s (value/s value/z))))) (step/app/arg (step/s (step/s (step/s (step/app/beta-v value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun step/ifz/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z))))) value/fun)) (step/app/arg (step/s (step/s (step/app/beta-v value/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/ifz/s value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z))))) value/fun)) (step/app/arg (step/s (step/app/beta-v value/z)) value/fun)) (step/app/arg (step/s (step/app/fun (step/ifz/s (value/s value/z)))) value/fun)) (step/app/arg (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/app/beta-v value/z) value/fun)) (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun) value/fun)) (step/app/arg (step/app/fun (step/ifz/s (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/ifz/s value/z) value/fun)) (step/app/arg (step/app/beta-v (value/s value/z)) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/fun (step/ifz/s (value/s (value/s value/z))))) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/ifz/s (value/s value/z))) (step/app/beta-v (value/s (value/s value/z)))) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))). %solve stepv (app (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (s (s (s z)))) E. OK D : stepv (app (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (s (s (s z)))) (s (s (s (s (s (s z)))))) = stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/v (value/s (value/s (value/s (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))))) (step/s (step/s (step/s (step/app/fun step/ifz/z))))) (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z)))))) (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/app/fun (step/ifz/s value/z))))) (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z)))))) (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/s (step/app/fun (step/ifz/s (value/s value/z))))) (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z)))))) (step/app/beta-v (value/s (value/s (value/s value/z))))) (step/app/arg (step/s (step/s (step/s (step/app/beta-v value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun step/ifz/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z))))) value/fun)) (step/app/arg (step/s (step/s (step/app/beta-v value/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/ifz/s value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z))))) value/fun)) (step/app/arg (step/s (step/app/beta-v value/z)) value/fun)) (step/app/arg (step/s (step/app/fun (step/ifz/s (value/s value/z)))) value/fun)) (step/app/arg (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/app/beta-v value/z) value/fun)) (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun) value/fun)) (step/app/arg (step/app/fun (step/ifz/s (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/ifz/s value/z) value/fun)) (step/app/arg (step/app/beta-v (value/s value/z)) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/fun (step/ifz/s (value/s (value/s value/z))))) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/ifz/s (value/s value/z))) (step/app/beta-v (value/s (value/s value/z)))) (step/app/arg (step/s (step/s (step/app/beta-v value/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun step/ifz/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/app/beta-v value/z)))) value/fun)) (step/app/arg (step/s (step/app/beta-v value/z)) value/fun)) (step/app/arg (step/s (step/app/fun (step/ifz/s value/z))) value/fun)) (step/app/arg (step/s (step/app/fun (step/app/beta-v (value/s value/z)))) value/fun)) (step/app/arg (step/app/beta-v value/z) value/fun)) (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun) value/fun)) (step/app/arg (step/app/fun (step/ifz/s (value/s value/z))) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/ifz/s value/z) value/fun)) (step/app/arg (step/app/beta-v (value/s value/z)) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/beta-v value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/fun step/ifz/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/fun (step/app/beta-v value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/ifz/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/ifz/s value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v (value/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/ifz/s value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v (value/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/ifz/s (value/s value/z)) value/fun)) (step/app/arg (step/app/beta-v (value/s (value/s value/z))) value/fun)) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/ifz/s (value/s (value/s value/z)))) (step/app/beta-v (value/s (value/s (value/s value/z)))). [Closing file /home/www/twelf/hcode/7060c1743be206623aab396ecd32723d] %% OK %%