% % Operational semantics of target expressions (M |-> M') % steptm : tm -> tm -> type. %name steptm _Steptm. % pair intro steptm/pair1 : steptm M1 M1' -> steptm (pairtm M1 M2) (pairtm M1' M2). steptm/pair2 : is-valuetm M1 -> steptm M2 M2' -> steptm (pairtm M1 M2) (pairtm M1 M2'). % pair projections steptm/fst : is-valuetm (pairtm M1 M2) -> steptm (fsttm (pairtm M1 M2)) M1. steptm/fst0 : steptm M0 M0' -> steptm (fsttm M0) (fsttm M0'). steptm/snd : is-valuetm (pairtm M1 M2) -> steptm (sndtm (pairtm M1 M2)) M2. steptm/snd0 : steptm M0 M0' -> steptm (sndtm M0) (sndtm M0'). % application steptm/app1 : steptm M1 M1' -> steptm (apptm M1 M2) (apptm M1' M2). steptm/app2 : is-valuetm M1 -> steptm M2 M2' -> steptm (apptm M1 M2 ) (apptm M1 M2'). steptm/beta : is-valuetm Marg -> steptm (apptm (lamtm [x] Mbody x) Marg) (Mbody Marg). % fix steptm/fix : steptm (fixtm ([u] Mbody u)) (Mbody (fixtm ([u] Mbody u))). % sum intro (injection) steptm/inl0 : steptm M0 M0' -> steptm (inltm M0) (inltm M0'). steptm/inr0 : steptm M0 M0' -> steptm (inrtm M0) (inrtm M0'). % sum elim (case) steptm/case0 : steptm M0 M0' -> steptm (casetm M0 N1 N2) (casetm M0' N1 N2). steptm/case1 : is-valuetm M -> steptm (casetm (inltm M) N1 N2) (N1 M). steptm/case2 : is-valuetm M -> steptm (casetm (inrtm M) N1 N2) (N2 M). % % % steptm* : steptm, zero or more times % % steptm* : tm -> tm -> type. %name steptm* _Steptms. steptm*/zero : steptm* M M. steptm*/left : steptm M1 M2 -> steptm* M2 MZ -> steptm* M1 MZ. % % steptm*snoc: adding a step at the end % steptm*snoc : % If steptm* M MY -> steptm MY MZ % then -> steptm* M MZ -> type. %mode steptm*snoc +Steptms +Steptm -Steptms'. steptm*snoc/zero : steptm*snoc steptm*/zero Steptm (steptm*/left Steptm steptm*/zero). steptm*snoc/n : steptm*snoc (steptm*/left Steptm1 Steptms) Steptm (steptm*/left Steptm1 Steptms') <- steptm*snoc Steptms Steptm Steptms'. %worlds () (steptm*snoc _ _ _). %total Steptms (steptm*snoc Steptms _ _).