-
-nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
- #m; #t; #s; #err; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
- #m; #t; #s; #susp; #n;
- ncases n;
- ##[ ##2: #n1 ##]
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma breakpoint :
- ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
- #m; #t; #n1;
- nelim n1;
- ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
- ##| ##2: #n3; #H; #n2; #s; ncases s;
- ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
- ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
- ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
- nchange with ((execute m t (tick m t x) (n3+n2)) =
- (execute m t (execute m t (tick m t x) n3) n2));
- nrewrite > (H n2 (tick m t x));
- napply refl_eq
- ##]
- ##]
-nqed.