CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g'). Solving... R' = [f':ctriv] [g':ctriv] klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))), CR = [f:dtriv] [f':ctriv] [cf:cpsT f f'] [g:dtriv] [g':ctriv] [cg:cpsT g g'] cps_droot [k:ccont] cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dapp (cps_dapp (cps_dtriv cf) ([t0:ctriv] cps_dtriv CT)) ([t0:ctriv] cps_dapp (cps_dtriv cg) ([t01:ctriv] cps_dtriv CT))). ; no more solutions ------------------------------------------------------------------------------- CVR : {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalR (klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v))))). Solving... CVR = [f':ctriv] [cvf:cvalT f'] [g':ctriv] [cvg:cvalT g'] cval_klam (cval_cret cval_k (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT1:cvalT v] cval_capp (cval_vlam [v1:ctriv] [CVT11:cvalT v1] cval_capp (cval_vlam [v11:ctriv] [CVT111:cvalT v11] cval_cret cval_k CVT111) CVT1 CVT11) cvg CVT) cvf CVT))). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalR (R' f' g')] {f:dtriv}{f':ctriv}{cvf:cvalT f'}{cf:cpsT f f'}{c1:cps_cvT cf cvf} {g:dtriv}{g':ctriv}{cvg:cvalT g'}{cg:cpsT g g'}{c2:cps_cvT cg cvg} cps_cvR (CR f f' cf g g' cg)(CVR f' cvf g' cvg). Solving... R' = [f':ctriv] [g':ctriv] klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))). ; no more solutions ------------------------------------------------------------------------------- VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} {g':ctriv}{vvg:{Xi:stack}vvalT Xi g' Xi} vvalR (klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v))))). Solving... VVR = [f':ctriv] [vvf:{Xi:stack} vvalT Xi f' Xi] [g':ctriv] [vvg:{Xi:stack} vvalT Xi g' Xi] vval_klam [k:ccont] [VVC:vvalC dot k] vval_cret VVC (vval_clam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_capp (vval_cont [v:ctriv] [VVT1:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_capp (vval_cont [v1:ctriv] [VVT11:{Xi':stack} vvalT (Xi' , v1) v1 Xi'] vval_capp (vval_cont [v11:ctriv] [VVT111:{Xi':stack} vvalT (Xi' , v11) v11 Xi'] vval_cret VVC1 (VVT111 dot)) (VVT1 dot) (VVT11 (dot , v))) (vvg (dot , v)) (VVT (dot , v))) (vvf dot) (VVT dot)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g')] sigma[VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} {g':ctriv}{vvg:{Xi:stack}vvalT Xi g' Xi} vvalR (R' f' g')] {f:dtriv}{f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi}{cf:cpsT f f'} {c1:cps_vvT cf vvf} {g:dtriv}{g':ctriv}{vvg:{Xi:stack}vvalT Xi g' Xi}{cg:cpsT g g'} {c2:cps_vvT cg vvg} cps_vvR (CR f f' cf g g' cg)(VVR f' vvf g' vvg). Solving... R' = [f':ctriv] [g':ctriv] klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))). ; no more solutions ------------------------------------------------------------------------------- CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f'). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v), CR = [f:dtriv] [f':ctriv] [cf:cpsT f f'] cps_droot [k:ccont] cps_dapp (cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dtriv CT)) ([t0:ctriv] cps_dtriv cf). ; no more solutions ------------------------------------------------------------------------------- CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v)). Solving... CVR = [f':ctriv] [cvf:cvalT f'] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT:cvalT v] cval_cret cval_k CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_cret cval_k CVT)) cvf). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v))] {f:dtriv}{f':ctriv}{cvf:cvalT f'}{cf:cpsT f f'}{c1:cps_cvT cf cvf} cps_cvR (CR f f' cf)(CVR f' cvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v)). Solving... VVR = [f':ctriv] [vvf:{Xi:stack} vvalT Xi f' Xi] vval_klam [k:ccont] [VVC:vvalC dot k] vval_capp (vval_cont [v:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_cret VVC (VVT dot)) (vval_clam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_cret VVC1 (VVT dot)) (vvf dot). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] sigma[VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v))] {f:dtriv}{f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi}{cf:cpsT f f'} {c1:cps_vvT cf vvf} cps_vvR (CR f f' cf)(VVR f' vvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] {f':ctriv}bareR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] {f':ctriv}cstackR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] {f':ctriv}{df:{xi:stack}dstackT xi f' f' xi} dstackR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f))) (R' f')] {f':ctriv}{df:{xi:stack}two_stacksT xi f' f' xi} two_stacksR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f'). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)), CR = [f:dtriv] [f':ctriv] [cf:cpsT f f'] cps_droot [k:ccont] cps_dapp (cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dtriv (cps_dlam [x1:dtriv] [x'1:ctriv] [CT1:cpsT x1 x'1] cps_droot [k11:ccont] cps_dapp (cps_dtriv CT) ([t0:ctriv] cps_dtriv CT1)))) ([t0:ctriv] cps_dapp (cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dtriv CT)) ([t01:ctriv] cps_dtriv cf)). ; no more solutions ------------------------------------------------------------------------------- CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v))). Solving... CVR = [f':ctriv] [cvf:cvalT f'] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT:cvalT v] cval_capp (cval_vlam [v1:ctriv] [CVT1:cvalT v1] cval_cret cval_k CVT1) (cval_xlam [x:ctriv] [CVT1:cvalT x] cval_klam (cval_cret cval_k (cval_xlam [x1:ctriv] [CVT11:cvalT x1] cval_klam (cval_capp (cval_vlam [v1:ctriv] [CVT111:cvalT v1] cval_cret cval_k CVT111) CVT1 CVT11)))) CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_cret cval_k CVT)) cvf). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)))] {f:dtriv}{f':ctriv}{cvf:cvalT f'}{cf:cpsT f f'}{c1:cps_cvT cf cvf} cps_cvR (CR f f' cf)(CVR f' cvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v))). Solving... VVR = [f':ctriv] [vvf:{Xi:stack} vvalT Xi f' Xi] vval_klam [k:ccont] [VVC:vvalC dot k] vval_capp (vval_cont [v:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_capp (vval_cont [v1:ctriv] [VVT1:{Xi':stack} vvalT (Xi' , v1) v1 Xi'] vval_cret VVC (VVT1 dot)) (vval_clam [x:ctriv] [VVT1:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_cret VVC1 (vval_clam [x1:ctriv] [VVT11:{Xi':stack} vvalT Xi' x1 Xi'] vval_klam [k11:ccont] [VVC11:vvalC dot k11] vval_capp (vval_cont [v1:ctriv] [VVT111:{Xi':stack} vvalT (Xi' , v1) v1 Xi'] vval_cret VVC11 (VVT111 dot)) (VVT1 dot) (VVT11 dot))) (VVT dot)) (vval_clam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_cret VVC1 (VVT dot)) (vvf dot). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] sigma[VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)))] {f:dtriv}{f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi}{cf:cpsT f f'} {c1:cps_vvT cf vvf} cps_vvR (CR f f' cf)(VVR f' vvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}bareR (R' f') (A f'). Solving... A = [f':ctriv] xlam [x'11:ctriv] klam [k111:ccont] capp f' x'11 (vlam [v:ctriv] cret k111 v), R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}cstackR (R' f') (A f'). Solving... A = [f':ctriv] xlam [x'1:ctriv] klam [k111:ccont] capp f' x'1 (vlam [v1:ctriv] cret k111 v1), R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}{df:{xi:stack}dstackT xi f' f' xi} dstackR (R' f') (A f'). Solving... A = [f':ctriv] xlam [x'111:ctriv] klam [k111:ccont] capp f' x'111 (vlam [v:ctriv] cret k111 v), R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv] dexp->droot (dapp (dtriv->dexp x) (dtriv->dexp y)))))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}{df:{xi:stack}two_stacksT xi f' f' xi} two_stacksR (R' f') (A f'). Solving... A = [f':ctriv] xlam [x'1:ctriv] klam [k111:ccont] capp f' x'1 (vlam [v1:ctriv] cret k111 v1), R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x' x'1 (vlam [v:ctriv] cret k11 v))) t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f'). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)), CR = [f:dtriv] [f':ctriv] [cf:cpsT f f'] cps_droot [k:ccont] cps_dapp (cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dtriv CT)) ([t0:ctriv] cps_dapp (cps_dtriv (cps_dlam [x:dtriv] [x':ctriv] [CT:cpsT x x'] cps_droot [k1:ccont] cps_dtriv CT)) ([t01:ctriv] cps_dtriv cf)). ; no more solutions ------------------------------------------------------------------------------- CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v))). Solving... CVR = [f':ctriv] [cvf:cvalT f'] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT:cvalT v] cval_capp (cval_vlam [v1:ctriv] [CVT1:cvalT v1] cval_cret cval_k CVT1) (cval_xlam [x:ctriv] [CVT1:cvalT x] cval_klam (cval_cret cval_k CVT1)) CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_cret cval_k CVT)) cvf). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} cvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)))] {f:dtriv}{f':ctriv}{cvf:cvalT f'}{cf:cpsT f f'}{c1:cps_cvT cf cvf} cps_cvR (CR f f' cf)(CVR f' cvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v))). Solving... VVR = [f':ctriv] [vvf:{Xi:stack} vvalT Xi f' Xi] vval_klam [k:ccont] [VVC:vvalC dot k] vval_capp (vval_cont [v:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_capp (vval_cont [v1:ctriv] [VVT1:{Xi':stack} vvalT (Xi' , v1) v1 Xi'] vval_cret VVC (VVT1 dot)) (vval_clam [x:ctriv] [VVT1:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_cret VVC1 (VVT1 dot)) (VVT dot)) (vval_clam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC1:vvalC dot k1] vval_cret VVC1 (VVT dot)) (vvf dot). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] sigma[VVR : {f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi} vvalR (klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)))] {f:dtriv}{f':ctriv}{vvf:{Xi:stack}vvalT Xi f' Xi}{cf:cpsT f f'} {c1:cps_vvT cf vvf} cps_vvR (CR f f' cf)(VVR f' vvf). Solving... R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}bareR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}cstackR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}{df:{xi:stack}dstackT xi f' f' xi} dstackR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp x))) (dtriv->dexp f)))) (R' f')] {f':ctriv}{df:{xi:stack}two_stacksT xi f' f' xi} two_stacksR (R' f') (A f'). Solving... A = [f':ctriv] f', R' = [f':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') f' (vlam [t1:ctriv] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 x') t1 (vlam [v:ctriv] cret k v)). ; no more solutions ------------------------------------------------------------------------------- THEOREM 8 ------------------------------------------------------------------------------- sigma[ASS : cvalE ([k:ccont]cret (vlam [v:ctriv]cret k v) (xlam [x:ctriv]klam [k:ccont]capp x x k))]th8-1 ASS A. Solving... A = cval_cret cval_k (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)). ; no more solutions ------------------------------------------------------------------------------- PROOF : th8-1 (cval_cret (cval_vlam [v:ctriv] [CVT:cvalT v] cval_cret cval_k CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT))) A. Solving... A = cval_cret cval_k (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)), PROOF = th8-1_proof. ; no more solutions ------------------------------------------------------------------------------- sigma[ASS : cvalE ([k':ccont] capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp v v (vlam [v1:ctriv] cret k v1))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]cret k' v2))] th8-2 ASS A. Solving... A = cval_capp (cval_vlam [v:ctriv] [cvv:cvalT v] cval_capp (cval_vlam [v1:ctriv] [cvv1:cvalT v1] cval_cret (cval_vlam [v11:ctriv] [CVT:cvalT v11] cval_cret cval_k CVT) cvv1) cvv cvv) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)). ; no more solutions ------------------------------------------------------------------------------- PROOF : th8-2 (cval_capp (cval_vlam [v:ctriv] [CVT:cvalT v] cval_cret cval_k CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT1:cvalT v] cval_capp (cval_vlam [v1:ctriv] [CVT11:cvalT v1] cval_cret cval_k CVT11) CVT1 CVT1) CVT CVT)) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT))) A. Solving... A = cval_capp (cval_vlam [v:ctriv] [cvv:cvalT v] cval_capp (cval_vlam [v1:ctriv] [cvv1:cvalT v1] cval_cret (cval_vlam [v11:ctriv] [CVT:cvalT v11] cval_cret cval_k CVT) cvv1) cvv cvv) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)), ------------------------------------------------------------------------------- A : cvalCS ([k:ccont](cdot ; vlam [v:ctriv]cret k v)). Solving... A = cvalS_vlam ([v:ctriv] [cvv:cvalT v] cval_cret cval_k cvv) cvalS_init. ; no more solutions ------------------------------------------------------------------------------- A : {x:ctriv}{y:ctriv} cstack_substE ([k:ccont]capp x x (vlam [v:ctriv]capp x x (vlam [v1:ctriv] cret k v1))) ([k:ccont] (cdot ; (vlam [v:ctriv]cret k (xlam[x1:ctriv]klam[k1:ccont]capp x x k1)) ; vlam [v:ctriv] capp y y k)) (E x y). Solving... E = [x:ctriv] [y:ctriv] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] cret (vlam [v11:ctriv] capp y y (vlam [v111:ctriv] cret k_init (xlam [x1:ctriv] klam [k1:ccont] capp x x k1))) v1)), A = [x:ctriv] [y:ctriv] csubst_capp (csubst_vlam [v:ctriv] csubst_capp (csubst_vlam [v1:ctriv] csubst_cret (csubst_k_vlam [v11:ctriv] csubst_capp (csubst_k_vlam [v111:ctriv] csubst_cret csubst_k_init)))). ; no more solutions ------------------------------------------------------------------------------- A : {x:ctriv}{y:ctriv} {k1:ccont}{k2:ccont}{cvx:cvalT x}{cvy:cvalT y} cvalCS ([k:ccont] (cdot ; (vlam [v:ctriv]cret k (xlam[x1:ctriv]klam[k:ccont]capp x x k)) ; vlam [v:ctriv] capp y y k)). Solving... A = [x:ctriv] [y:ctriv] [k1:ccont] [k2:ccont] [cvx:cvalT x] [cvy:cvalT y] cvalS_vlam ([v:ctriv] [cvv:cvalT v] cval_capp cval_k cvy cvy) (cvalS_vlam ([v:ctriv] [cvv:cvalT v] cval_cret cval_k (cval_xlam [x1:ctriv] [CVT:cvalT x1] cval_klam (cval_capp cval_k cvx cvx))) cvalS_init). ; no more solutions ------------------------------------------------------------------------------- sigma[CVS:{x:ctriv}{y:ctriv} {cvx:cvalT x}{cvy:cvalT y} cvalCS ([k:ccont] (cdot ; (vlam [v:ctriv]cret k (xlam[x1:ctriv]klam[k:ccont]capp x x k)) ; vlam [v:ctriv] capp y y k))] sigma[CVE:{f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalE ([k:ccont]cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))))] sigma[CSE:{x:ctriv}{y:ctriv}{v:ctriv} cstack_substE ([k:ccont]capp y y k) ([k:ccont] (cdot ; (vlam [v:ctriv]cret k (xlam[x1:ctriv]klam[k:ccont]capp x x k)))) (E1 v x y)] {x:ctriv}{y:ctriv} {cvx:cvalT x}{cvy:cvalT y} {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} lemma14-1a (CVS x y cvx cvy) (CVE f' cvf g' cvg) (CSE x y) (S2 g' f' x y). Solving... S2 = [g':ctriv] [f':ctriv] [x:ctriv] [y:ctriv] csubst_cret (csubst_k_vlam [v:ctriv] csubst_capp (csubst_k_vlam [v1:ctriv] csubst_cret csubst_k_init)), E1 = [v:ctriv] [x:ctriv] [y:ctriv] capp y y (vlam [v1:ctriv] cret k_init (xlam [x1:ctriv] klam [k1:ccont] capp x x k1)). ; no more solutions ------------------------------------------------------------------------------- sigma[CVS:{x:ctriv}{y:ctriv} {cvx:cvalT x}{cvy:cvalT y} cvalCS ([k:ccont] (cdot ; (vlam [v:ctriv]cret k (xlam[x1:ctriv]klam[k:ccont]capp x x k)) ; vlam [v:ctriv] capp y y k))] sigma[CVE:{f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalE ([k:ccont]cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))))] {x:ctriv}{y:ctriv} {cvx:cvalT x}{cvy:cvalT y} {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} lemma14-1a (CVS x y cvx cvy) (CVE f' cvf g' cvg) ([v:ctriv]csubst_capp (csubst_k_vlam [v1:ctriv] csubst_cret csubst_k_init)) (A g' f' x y). Solving... A = [g':ctriv] [f':ctriv] [x:ctriv] [y:ctriv] csubst_cret (csubst_k_vlam [v:ctriv] csubst_capp (csubst_k_vlam [v1:ctriv] csubst_cret csubst_k_init)). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalR (R' f' g')] sigma[CM:{f':ctriv}{g':ctriv}cstackR (R' f' g') (C f' g')] sigma[BM:{f':ctriv}{g':ctriv}bareR (R' f' g') (B f' g')] {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} th15-1 (CVR f' cvf g' cvg) (CM f' g') (BM f' g'). Solving... B = [f':ctriv] [g':ctriv] xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v))), C = [f':ctriv] [g':ctriv] xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v))), R' = [f':ctriv] [g':ctriv] klam [k:ccont] cret k (xlam [x':ctriv] klam [k1:ccont] capp f' x' (vlam [t01:ctriv] capp g' x' (vlam [t1:ctriv] capp t01 t1 (vlam [v:ctriv] cret k1 v)))). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] dexp->droot (dtriv->dexp (dlam [y:dtriv]dexp->droot (dapp (dtriv->dexp y) (dtriv->dexp x)))))) (dtriv->dexp g))) (R' g')] sigma[CVR : {g':ctriv}{cvg:cvalT g'} cvalR (R' g')] sigma[CM:{g':ctriv}cstackR (R' g') (C g')] sigma[BM:{g':ctriv}bareR (R' g') (B g')] {g':ctriv}{cvg:cvalT g'} th15-1 (CVR g' cvg) (CM g') (BM g'). Solving... B = [g':ctriv] xlam [x'1:ctriv] klam [k11:ccont] capp x'1 g' (vlam [v:ctriv] cret k11 v), C = [g':ctriv] xlam [x'1:ctriv] klam [k11:ccont] capp x'1 g' (vlam [v:ctriv] cret k11 v), R' = [g':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] cret k1 (xlam [x'1:ctriv] klam [k11:ccont] capp x'1 x' (vlam [v:ctriv] cret k11 v))) g' (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- sigma[CR : {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dapp (dtriv->dexp (dlam ([x:dtriv]dexp->droot (dapp (dtriv->dexp x)(dtriv->dexp g))))) (dtriv->dexp (dlam ([x:dtriv]dexp->droot (dtriv->dexp x)))))) (R' g')] sigma[CVR : {g':ctriv}{cvg:cvalT g'} cvalR (R' g')] sigma[CM:{g':ctriv}cstackR (R' g') (C g')] sigma[BM:{g':ctriv}bareR (R' g') (B g')] {g':ctriv}{cvg:cvalT g'} th15-1 (CVR g' cvg) (CM g') (BM g'). Solving... B = [g':ctriv] g', C = [g':ctriv] g', R' = [g':ctriv] klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] capp x' g' (vlam [v:ctriv] cret k1 v)) (xlam [x':ctriv] klam [k1:ccont] cret k1 x') (vlam [v:ctriv] cret k v). ; no more solutions ------------------------------------------------------------------------------- LEMMA 9, THEOREM 10 ------------------------------------------------------------------------------- sigma[ASS : {k:ccont}{vvk:vvalC dot k}vvalE dot (cret (vlam [v:ctriv]cret k v) (xlam [x:ctriv]klam [k:ccont]capp x x k))] {k:ccont}{vvk:vvalC dot k}th10-1 (ASS k vvk) (A k vvk). Solving... A = [k:ccont] [vvk:vvalC dot k] vval_cret vvk (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)). ; no more solutions ------------------------------------------------------------------------------- PROOF : {k:ccont}{vvk:vvalC dot k} th10-1 (vval_cret (vval_vlam [v:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_cret vvk (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (A k vvk). Solving... A = [k:ccont] [vvk:vvalC dot k] vval_cret vvk (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)), PROOF = [k:ccont] [vvk:vvalC dot k] th10-1_c lemma9-1b_cret_t. ; no more solutions ------------------------------------------------------------------------------- sigma[ASS : {v':ctriv}{vvv':{xi:stack}vvalT (xi , v') v' xi}{k:ccont}{vvk:vvalC dot k}vvalE (dot , v') ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v' v2 k))] sigma[ASS1 : {v':ctriv}{cvv':cvalT v'} cvalE ([k:ccont] capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v' v2 k))] {v':ctriv}{vvv':{xi:stack}vvalT (xi , v') v' xi} {cvv':cvalT v'} th10-2 (ASS v' vvv') (ASS1 v' cvv')([xi:stack]vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))(A v' vvv'). Solving... A = [v':ctriv] [vvv':{xi:stack} vvalT (xi , v') v' xi] [k:ccont] [vvk:vvalC dot k] vval_capp (vval_vlam [v:ctriv] [vvv:{xi:stack} vvalT (xi , v) v xi] vval_capp (vval_vlam [v1:ctriv] [vvv1:{xi:stack} vvalT (xi , v1) v1 xi] vval_capp (vval_vlam [v11:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v11) v11 Xi'] vval_capp vvk (vvv' dot) (VVT (dot , v'))) (vvv (dot , v')) (vvv1 (dot , v' , v))) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)). ; no more solutions ------------------------------------------------------------------------------- PROOF : {v':ctriv}{vvv':{xi:stack}vvalT (xi , v') v' xi} {cvv':cvalT v'} th10-2 ([k:ccont] [vvk:vvalC dot k] vval_capp (vval_vlam [v:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_capp vvk (vvv' dot) (VVT (dot , v'))) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp (vval_vlam [v:ctriv] [VVT1:{Xi':stack} vvalT (Xi' , v) v Xi'] vval_capp (vval_vlam [v1:ctriv] [VVT11:{Xi':stack} vvalT (Xi' , v1) v1 Xi'] vval_capp VVC (VVT1 dot) (VVT11 (dot , v))) (VVT (dot , v)) (VVT (dot , v))) (VVT dot) (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)))( cval_capp (cval_vlam [v:ctriv] [CVT:cvalT v] cval_capp cval_k cvv' CVT) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp (cval_vlam [v:ctriv] [CVT1:cvalT v] cval_capp (cval_vlam [v1:ctriv] [CVT11:cvalT v1] cval_capp cval_k CVT1 CVT11) CVT CVT) CVT CVT)) (cval_xlam [x:ctriv] [CVT:cvalT x] cval_klam (cval_capp cval_k CVT CVT)))([xi:stack]vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)) (A v' vvv'). Solving... A = [v':ctriv] [vvv':{xi:stack} vvalT (xi , v') v' xi] [k:ccont] [vvk:vvalC dot k] vval_capp (vval_vlam [v:ctriv] [vvv:{xi:stack} vvalT (xi , v) v xi] vval_capp (vval_vlam [v1:ctriv] [vvv1:{xi:stack} vvalT (xi , v1) v1 xi] vval_capp (vval_vlam [v11:ctriv] [VVT:{Xi':stack} vvalT (Xi' , v11) v11 Xi'] vval_capp vvk (vvv' dot) (VVT (dot , v'))) (vvv (dot , v')) (vvv1 (dot , v' , v))) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)) (vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot)), PROOF = [v':ctriv] [vvv':{xi:stack} vvalT (xi , v') v' xi] [cvv':cvalT v'] th10-2_proof [k:ccont] [vvk:vvalC dot k] lemma9-3a_capp_c (app_t (xlam [x:ctriv] klam [k1:ccont] capp x x k1) ([xi:stack] vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (app_t (xlam [x:ctriv] klam [k1:ccont] capp x x k1) ([xi:stack] vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (lemma9-3b_vlam [v:ctriv] [vvv:{xi:stack} vvalT (xi , v) v xi] [cvv:cvalT v] lemma9-3a_capp_c (app_t (xlam [x:ctriv] klam [k1:ccont] capp x x k1) ([xi:stack] vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (app_t (xlam [x:ctriv] klam [k1:ccont] capp x x k1) ([xi:stack] vval_xlam [x:ctriv] [VVT:{Xi':stack} vvalT Xi' x Xi'] vval_klam [k1:ccont] [VVC:vvalC dot k1] vval_capp VVC (VVT dot) (VVT dot))) (lemma9-3b_vlam [v1:ctriv] [vvv1:{xi:stack} vvalT (xi , v1) v1 xi] [cvv1:cvalT v1] lemma9-3a_capp_k (app_v v1 ([xi:stack] vvv1 xi)) (app_v v ([xi:stack] vvv xi)))). ; no more solutions ------------------------------------------------------------------------------- LEMMA 17 ------------------------------------------------------------------------------- sigma[ASS : {v':ctriv}{vvv':{xi:stack}vvalT (xi , v') v' xi}{k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k}{dsv':{xi:stack}{t:ctriv}dstack_substT v' (xi , t) t xi}{lTk: lemma17-1C vvk dsk} vvalE (dot , v') ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v' v2 k))] {v':ctriv}{vvv':{xi:stack}vvalT (xi , v') v' xi}{k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k}{dsv':{xi:stack}{t:ctriv}dstack_substT v' (xi , t) t xi}{lTk: lemma17-1C vvk dsk} lemma17-1E (ASS v' vvv' k vvk dsk dsv' lTk) (DSE v' vvv' k vvk dsk dsv' lTk). DSE = [v':ctriv] [vvv':{xi:stack} vvalT (xi , v') v' xi] [k:ccont] [vvk:vvalC dot k] [dsk:dstack_substC k dot k] [dsv':{xi:stack} {t:ctriv} dstack_substT v' (xi , t) t xi] [lTv':{xi:stack} lemma17-1T (vvv' xi) (dsv' xi v')] [lTk:lemma17-1C vvk dsk] dstack_subst_capp (dstack_subst_vlam [v:ctriv] [dsv:{xi:stack} {t:ctriv} dstack_substT v (xi , t) t xi] dstack_subst_capp dsk (dsv' dot v') (dsv (dot , v') v)) dstack_subst_xlam dstack_subst_xlam. ; no more solutions ------------------------------------------------------------------------------- sigma[ASS : {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} {lTk: lemma17-1C vvk dsk} vvalE dot ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x v (vlam [v1:ctriv] cret k v1))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]cret k v2))] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} {lTk: lemma17-1C vvk dsk} lemma17-1E (ASS k vvk dsk lTk) (A k vvk dsk lTk). A = [k:ccont] [vvk:vvalC dot k] [dsk:dstack_substC k dot k] [lTk:lemma17-1C vvk dsk] dstack_subst_capp (dstack_subst_vlam [v:ctriv] [dsv:{xi:stack} {t:ctriv} dstack_substT v (xi , t) t xi] dstack_subst_cret dsk (dsv dot v)) dstack_subst_xlam dstack_subst_xlam. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v:ctriv}app ((dot , v) & dot) (XXi1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v) ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k))] sigma[APP1 : {v:ctriv}app ((dot , v) & dot) (Xi1 v)] sigma[VVMS : {v:ctriv}vvalMS (XXi1 v) (Xi1 (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 v) (E1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k)))) (E1 (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} lemma17-2 V APP (VVE k vvk) APP1 VVMS (DSE k dsk) (DSE' k dsk). Solving... E1 = [v:ctriv] [k:ccont] capp (xlam [x:ctriv] klam [k1:ccont] capp x x (vlam [v1:ctriv] capp x x (vlam [v11:ctriv] capp v1 v11 k1))) (xlam [x:ctriv] klam [k1:ccont] capp x x k1) (vlam [v1:ctriv] capp v v1 k), Xi1 = [v:ctriv] dot , v, XXi1 = [v:ctriv] dot , v. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v1:ctriv}{v:ctriv}app ((dot , v) & (dot , v1)) (XXi1 v1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v1 v) (capp v v1 k)] sigma[APP1 : {v:ctriv}app ((dot , v) & (dot , (xlam [x:ctriv] klam [k:ccont] capp x x k))) (Xi1 v)] sigma[VVMS : {v1:ctriv}{v:ctriv}vvalMS (XXi1 v1 v) (Xi1 (xlam [x:ctriv] klam [k:ccont] cret k x))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (capp v v1 k) (Xi1 v) (E v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (capp v v1 k) (Xi1 (xlam [x:ctriv]klam [k:ccont] cret k x)) (E (xlam [x:ctriv]klam [k:ccont] cret k x) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} lemma17-2 V (APP v1) (VVE k vvk v1 vvv1) APP1 (VVMS v1) (DSE k dsk v1 dsv1) (DSE' k dsk v1 dsv1). Solving... E = [v:ctriv] [k:ccont] capp v (xlam [x:ctriv] klam [k1:ccont] capp x x k1) k, Xi1 = [v:ctriv] dot , v , (xlam [x:ctriv] klam [k:ccont] capp x x k), XXi1 = [v1:ctriv] [v:ctriv] dot , v , v1. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v:ctriv}app ((dot , v) & dot) (XXi1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v) ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k))] sigma[APP1 : {v:ctriv}app ((dot , v) & dot) (Xi1 v)] sigma[VVMS : {v:ctriv}vvalMS (XXi1 v) (Xi1 (xlam [x:ctriv] klam [k:ccont]cret k x))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 v) (E1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 (xlam [x:ctriv] klam [k:ccont] cret k x)) (E1 (xlam [x:ctriv] klam [k:ccont] cret k x) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} lemma17-2 V APP (VVE k vvk) APP1 CORR (DSE k dsk) (DSE' k dsk). Solving... E1 = [v:ctriv] [k:ccont] capp (xlam [x:ctriv] klam [k1:ccont] capp x x k1) (xlam [x:ctriv] klam [k1:ccont] capp x x k1) (vlam [v1:ctriv] capp v v1 k), Xi1 = [v:ctriv] dot , v, XXi1 = [v:ctriv] dot , v. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v:ctriv}app ((dot , v) & dot) (XXi1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v) ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k))] sigma[APP1 : {v:ctriv}app ((dot , v) & dot) (Xi1 v)] sigma[VVMS : {v:ctriv}vvalMS (XXi1 v) (Xi1 (xlam [x:ctriv] klam [k:ccont]cret k x))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 v) (E1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x k) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 (xlam [x:ctriv] klam [k:ccont] cret k x)) (E1 (xlam [x:ctriv] klam [k:ccont] cret k x) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} lemma17-2 V APP (VVE k vvk) APP1 VVMS (DSE k dsk) (DSE' k dsk). Solving... E1 = [v:ctriv] [k:ccont] capp (xlam [x:ctriv] klam [k1:ccont] capp x x k1) (xlam [x:ctriv] klam [k1:ccont] capp x x k1) (vlam [v1:ctriv] capp v v1 k), Xi1 = [v:ctriv] dot , v, XXi1 = [v:ctriv] dot , v. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v:ctriv}app ((dot , v) & dot) (XXi1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v) (cret (vlam [v1:ctriv] capp v v1 k)(xlam [x:ctriv] klam [k:ccont] capp x x k)) ] sigma[APP1 : {v:ctriv}app ((dot , v) & dot) (Xi1 v)] sigma[VVMS : {v:ctriv}vvalMS (XXi1 v) (Xi1 (xlam [x:ctriv] klam [k:ccont] cret k x))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k)(xlam [x:ctriv] klam [k:ccont] capp x x k)) (Xi1 v) (E v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k)(xlam [x:ctriv] klam [k:ccont] capp x x k)) (Xi1 (xlam [x:ctriv]klam [k:ccont] cret k x)) (E (xlam [x:ctriv]klam [k:ccont] cret k x) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} lemma17-2 V APP (VVE k vvk) APP1 VVMS (DSE k dsk) (DSE' k dsk). Solving... E = [v:ctriv] [k:ccont] cret (vlam [v1:ctriv] capp v v1 k) (xlam [x:ctriv] klam [k1:ccont] capp x x k1), Xi1 = [v:ctriv] dot , v, XXi1 = [v:ctriv] dot , v. ; no more solutions ------------------------------------------------------------------------------- sigma[APP : {v1:ctriv}{v:ctriv}app ((dot , v) & (dot , v1)) (XXi1 v1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v1 v) (cret (vlam [v1:ctriv] capp v v1 k) v1) ] sigma[APP1 : {v1:ctriv}{v:ctriv}app ((dot , v) & (dot , v1)) (Xi1 v1 v)] sigma[VVMS : {v1:ctriv}{v:ctriv}vvalMS (XXi1 v1 v) (Xi1 v1 (xlam [x:ctriv] klam [k:ccont] cret k x))] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k) v1) (Xi1 v1 v) (E v1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k) v1) (Xi1 v1 (xlam [x:ctriv]klam [k:ccont] cret k x)) (E v1 (xlam [x:ctriv]klam [k:ccont] cret k x) k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} lemma17-2 V (APP v1) (VVE k vvk v1 vvv1) (APP1 v1) (VVMS v1) (DSE k dsk v1 dsv1) (DSE' k dsk v1 dsv1). ------------------------------------------------------------------------------- sigma[APP : {v1:ctriv}{v:ctriv}app ((dot , v) & (dot , v1)) (XXi1 v1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v1 v) (cret (vlam [v1:ctriv] capp v v1 k) v1) ] sigma[APP1 : {v1:ctriv}{v:ctriv}app ((dot , v) & (dot , v1)) (Xi1 v1 v)] sigma[VVMS : {v1:ctriv}{v:ctriv}vvalMS (XXi1 v1 v) (Xi1 v1 v)] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k) v1) (Xi1 v1 v) (E v1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v1:ctriv}{dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE (cret (vlam [v1:ctriv] capp v v1 k) v1) (Xi1 v1 v) (E v1 v k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} {v1:ctriv}{vvv1:{xi:stack}vvalT (xi , v1) v1 xi} {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi} lemma17-2 V (APP v1) (VVE k vvk v1 vvv1) (APP1 v1) (VVMS v1) (DSE k dsk v1 dsv1) (DSE' k dsk v1 dsv1). ------------------------------------------------------------------------------- theorem 18 ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g')] sigma[VVR : {f':ctriv}{vvf:{xi:stack}vvalT xi f' xi} {g':ctriv}{vvg:{xi:stack}vvalT xi g' xi} vvalR (R' f' g')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalR (R' f' g')] sigma[DR : {f':ctriv}{g':ctriv} {df':{xi:stack}dstackT xi f' f' xi} {dg':{xi:stack}dstackT xi g' g' xi} dstackR (R' f' g') (A f' df' g' dg')] {f:dtriv}{f':ctriv}{vvf:{xi:stack}vvalT xi f' xi}{cf:cpsT f f'}{cvf:cvalT f'} {g:dtriv}{g':ctriv}{vvg:{xi:stack}vvalT xi g' xi}{cg:cpsT g g'}{cvg:cvalT g'} {df':{xi:stack}dstackT xi f' f' xi}{dg':{xi:stack}dstackT xi g' g' xi} th18-1 (VVR f' vvf g' vvg) (CVR f' cvf g' cvg) (DR f' g' df' dg') (BR f' g'). ------------------------------------------------------------------------------- sigma[CR : {f:dtriv}{f':ctriv}{cf:cpsT f f'} {g:dtriv}{g':ctriv}{cg:cpsT g g'} cpsR (dexp->droot (dtriv->dexp (dlam [x:dtriv] dexp->droot (dapp (dapp (dtriv->dexp f) (dtriv->dexp x)) (dapp (dtriv->dexp g) (dtriv->dexp x)))))) (R' f' g')] sigma[VVR : {f':ctriv}{vvf:{xi:stack}vvalT xi f' xi} {g':ctriv}{vvg:{xi:stack}vvalT xi g' xi} vvalR (R' f' g')] sigma[CVR : {f':ctriv}{cvf:cvalT f'} {g':ctriv}{cvg:cvalT g'} cvalR (R' f' g')] sigma[DR : {f':ctriv}{g':ctriv} {df':{xi:stack}dstackT xi f' f' xi} {dg':{xi:stack}dstackT xi g' g' xi} dstackR (R' f' g') (A f' df' g' dg')] {f:dtriv}{f':ctriv}{vvf:{xi:stack}vvalT xi f' xi}{cf:cpsT f f'}{cvf:cvalT f'} {g:dtriv}{g':ctriv}{vvg:{xi:stack}vvalT xi g' xi}{cg:cpsT g g'}{cvg:cvalT g'} {df':{xi:stack}dstackT xi f' f' xi}{dg':{xi:stack}dstackT xi g' g' xi} th18-1 (VVR f' vvf g' vvg) (CVR f' cvf g' cvg) (DR f' g' df' dg') (BR f' g'). ------------------------------------------------------------------------------- sigma[CR : cpsR (dexp->droot (dapp (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] (dexp->droot (dtriv->dexp x)))) (dtriv->dexp f))))) (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dtriv->dexp f)))))) R'] sigma[VVR : vvalR R'] sigma[CVR : cvalR R'] sigma[DR : dstackR R' A] th18-1 VVR CVR DR BR. BR = bare_klam (bare_capp (bare_capp (bare_cret (bare_cret bare_init)))), A = xlam [x':ctriv] klam [k1:ccont] cret k1 x', R' = klam [k:ccont] capp (xlam [x':ctriv] klam [k1:ccont] capp (xlam [x'1:ctriv] klam [k11:ccont] cret k11 x'1) x' (vlam [v:ctriv] cret k1 v)) (xlam [x':ctriv] klam [k1:ccont] cret k1 x') (vlam [v:ctriv] cret k v) (vlam [v:ctriv] cret k v). ------------------------------------------------------------------------------- sigma[CR : cpsR (dexp->droot (dapp (dapp (dtriv->dexp(dlam [x:dtriv](dexp->droot (dtriv->dexp x)))) (dtriv->dexp (dlam [x:dtriv](dexp->droot (dtriv->dexp x))))) (dapp (dtriv->dexp(dlam [x:dtriv](dexp->droot (dtriv->dexp x)))) (dtriv->dexp (dlam [x:dtriv](dexp->droot (dtriv->dexp x))))))) R'] sigma[VVR : vvalR R'] sigma[CVR : cvalR R'] sigma[DR : dstackR R' A] th18-1 VVR CVR DR BR. ------------------------------------------------------------------------------- sigma[CR : cpsR (dexp->droot (dapp (dapp (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] (dexp->droot (dtriv->dexp x)))) (dtriv->dexp f))))) (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dtriv->dexp f))))) (dapp (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dapp (dtriv->dexp (dlam [x:dtriv] (dexp->droot (dtriv->dexp x)))) (dtriv->dexp f))))) (dtriv->dexp (dlam [f:dtriv] (dexp->droot (dtriv->dexp f))))))) R'] sigma[VVR : vvalR R'] sigma[CVR : cvalR R'] sigma[BR : bareR R' A] th18-1 VVR CVR DR BR. ------------------------------------------------------------------------------- sigma[APP : {v:ctriv}app ((dot , v) & dot) (XXi1 v)] sigma[VVE : {k:ccont}{vvk:vvalC dot k} {v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi} vvalE (XXi1 v) ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k))] sigma[APP1 : {v:ctriv}app ((dot , v) & dot) (Xi1 v)] sigma[VVALMS : {v:ctriv}vvalMS (XXi1 v) (Xi1 v)] sigma[DSE : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 v) (E1 v k)] sigma[DSE' : {k:ccont}{dsk:dstack_substC k dot k} {v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi} dstack_substE ( capp (xlam [x:ctriv] klam [k:ccont] capp x x (vlam [v:ctriv] capp x x (vlam [v1:ctriv] capp v v1 k))) (xlam [x:ctriv]klam [k:ccont]capp x x k) (vlam [v2:ctriv]capp v v2 k)) (Xi1 v) (E1 v k)] {k:ccont}{vvk:vvalC dot k}{dsk:dstack_substC k dot k} lemma17-2 ([v:ctriv]v) APP (VVE k vvk) APP1 VVALMS (DSE k dsk) (DSE' k dsk).