interpretation "labelled sequential computation"
'SeqRedStar M s N = (lsreds s M N).
-notation "hvbox( M break â\87\80* [ term 46 s ] break term 46 N )"
+notation "hvbox( M break â\86¦* [ term 46 s ] break term 46 N )"
non associative with precedence 45
for @{ 'SeqRedStar $M $s $N }.
-lemma lsreds_step_rc: â\88\80p,M1,M2. M1 â\87\80[p] M2 â\86\92 M1 â\87\80*[p::◊] M2.
+lemma lsreds_step_rc: â\88\80p,M1,M2. M1 â\86¦[p] M2 â\86\92 M1 â\86¦*[p::◊] M2.
/2 width=1/
qed.
-lemma lsreds_inv_nil: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → ◊ = s → M1 = M2.
+lemma lsreds_inv_nil: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → ◊ = s → M1 = M2.
/2 width=5 by lstar_inv_nil/
qed-.
-lemma lsreds_inv_cons: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → ∀q,r. q::r = s →
- â\88\83â\88\83M. M1 â\87\80[q] M & M â\87\80*[r] M2.
+lemma lsreds_inv_cons: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → ∀q,r. q::r = s →
+ â\88\83â\88\83M. M1 â\86¦[q] M & M â\86¦*[r] M2.
/2 width=3 by lstar_inv_cons/
qed-.
-lemma lsreds_inv_step_rc: â\88\80p,M1,M2. M1 â\87\80*[p::â\97\8a] M2 â\86\92 M1 â\87\80[p] M2.
+lemma lsreds_inv_step_rc: â\88\80p,M1,M2. M1 â\86¦*[p::â\97\8a] M2 â\86\92 M1 â\86¦[p] M2.
/2 width=1 by lstar_inv_step/
qed-.
-lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → 0 < |s| →
- â\88\83â\88\83p,r,M. p::r = s & M1 â\87\80[p] M & M â\87\80*[r] M2.
+lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → 0 < |s| →
+ â\88\83â\88\83p,r,M. p::r = s & M1 â\86¦[p] M & M â\86¦*[r] M2.
/2 width=1 by lstar_inv_pos/
qed-.
qed-.
(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
+lemma lsreds_fwd_mult: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
#p #s #M1 #M #HM1 #_ #IHM2
lapply (lsred_fwd_mult … HM1) -p #HM1