step-eval-context : % If {E} {E'} {Step : step E E'} {EC : eval-context} {Fill : fill EC EH} % then step (EH E) (EH E') -> type. %mode step-eval-context +E +E' +StepIn +EC +Fill -StepOut. - : step-eval-context E E' Step (ec/hole) (fill/hole) Step. - : step-eval-context E E' Step (ec/app1 EC1 E2) (fill/app1 Fill1) (step/app1 Step1) <- step-eval-context E E' Step EC1 Fill1 Step1. - : step-eval-context E E' Step (ec/app2 E1 IsVal1 EC2) (fill/app2 Fill2) (step/app2 IsVal1 Step2) <- step-eval-context E E' Step EC2 Fill2 Step2. - : step-eval-context E E' Step (ec/merge1 EC1 E2) (fill/merge1 Fill1) (step/merge1 Step1) <- step-eval-context E E' Step EC1 Fill1 Step1. - : step-eval-context E E' Step (ec/merge2 E1 EC2) (fill/merge2 Fill2) (step/merge2 Step2) <- step-eval-context E E' Step EC2 Fill2 Step2. %worlds () (step-eval-context _ _ _ _ _ _). %total EC (step-eval-context _ _ _ EC _ _). step*eval-context : % If {E} {E'} {Step* : step* E E'} {EC : eval-context} {Fill : fill EC EH} % then step* (EH E) (EH E') -> type. %mode step*eval-context +E +E' +StepIn +EC +Fill -StepOut. - : step*eval-context E E (step*/zero) EC Fill (step*/zero). - : step*eval-context E E' (step*/left StepIn StepIn*) EC Fill (step*/left StepOut StepOut*) <- step-eval-context E _ StepIn EC Fill StepOut <- step*eval-context _ E' StepIn* EC Fill StepOut*. %worlds () (step*eval-context _ _ _ _ _ _). %total StepIn (step*eval-context _ _ StepIn _ _ _).