(**************************************************************************)
include "arithmetics/nat.ma".
-include "basics/list.ma".
+include "basics/lists/list.ma".
interpretation "iff" 'iff a b = (iff a b).
interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}.
interpretation "cat" 'pc a b = (c ? a b).
(* to get rid of \middot
interpretation "pepsilon" 'epsilon = (pe ?).
interpretation "pempty" 'empty = (pz ?).
-notation > "| e |" non associative with precedence 65 for @{forget ? $e}.
+notation > "| e |" non associative with precedence 66 for @{forget ? $e}.
let rec forget (S: Alpha) (l : pitem S) on l: re S ≝
match l with
[ pz ⇒ ∅
qed.
definition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1||b2〉.
match e with
[ pair i b ⇒ 〈\fst (f S i), \snd (f S i) || b〉].
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc (lift eclose) $a $b}.
+notation > "a ⊙ b" left associative with precedence 65 for @{'lc (lift eclose) $a $b}.
definition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λe:pre S.
match e with
notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation > "•" non associative with precedence 65 for @{eclose ?}.
let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝
match i with
[ pz ⇒ 〈 ∅, false 〉
| pc E1 E2 ⇒ •E1 ⊙ 〈E2,false〉
| pk E ⇒ 〈(\fst(•E))^*,true〉].
-notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+notation < "• x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+notation > "• x" non associative with precedence 65 for @{'eclose $x}.
definition reclose ≝ lift eclose.
interpretation "reclose" 'eclose x = (reclose ? x).
definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
+notation "A ≐ B" non associative with precedence 45 for @{'eq_f1 $A $B}.
interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
(*
-lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) =1 ϵ b1 ∪ ϵ b2.
+lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) ≐ ϵ b1 ∪ ϵ b2.
##[##2: napply S]
#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
nqed.
#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*)
(* theorem 16: 2 *)
-lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}.
#S * #i1 #b1 * #i2 #b2 >lo_def normalize in ⊢ (?%?);
#w cases b1 cases b2 normalize % #w r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
STOP
notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
match E with
[ pz ⇒ 〈 ∅, false 〉
| po e1 e2 ⇒ \move x e1 ⊕ \move x e2
| pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
| pk e ⇒ (\move x e)^⊛ ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
interpretation "move" 'move x E = (move ? x E).
ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
nqed.
-notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}.
nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
match w with
[ nil ⇒ E