- [ pz ⇒ 〈 false, pz ? 〉
- | pe ⇒ 〈 false, pe ? 〉
- | ps y ⇒ 〈false, ps ? y 〉
- | pp y ⇒ 〈 eqb … x y, ps ? y 〉
- | pc E1 E2 ⇒
- let E1' ≝ move ? x E1 in
- let E2' ≝ move ? x E2 in
- let E1'' ≝ snd … E1' in
- let E2'' ≝ snd ?? E2' in
- match fst … E1' with
- [ true =>
- let E2''' ≝ eclose S E2'' in
- 〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
- | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
- | po E1 E2 ⇒
- let E1' ≝ move ? x E1 in
- let E2' ≝ move ? x E2 in
- 〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
- | pk E ⇒
- let E' ≝ move S x E in
- let E'' ≝ snd bool (pre S) E' in
- match fst … E' with
- [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
- | false ⇒ 〈 false, pk ? E'' 〉 ]].
+ [ pz ⇒ 〈 ∅, false 〉
+ | pe ⇒ 〈 ϵ, true 〉
+ | ps x ⇒ 〈 `.x, false 〉
+ | pp x ⇒ 〈 `.x, false 〉
+ | po E1 E2 ⇒ •E1 ⊕ •E2
+ | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
+ | pk E ⇒ 〈E,true〉^⊛].
+notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+interpretation "eclose" 'eclose x = (eclose ? x).
+notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+
+ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
+interpretation "reclose" 'eclose x = (reclose ? x).
+
+nlemma lemma19_2 :
+ ∀S:Alpha.∀e1,e2:pre S.∀w. w .∈ e1 ⊕ e2 → w .∈ e1 ∨ w .∈ e2.
+#S e1 e2 w H; nnormalize in H; ncases H;
+##[ *; #defw; ncases e1; #p b; ncases b; nnormalize;
+ ##[ #_; @1; @1; /2/ by conj;
+ ##| #H1; @2; @1; /2/ by conj; ##]
+##| #H1; ninversion H1; #; ndestruct; /4/ by or_introl, or_intror; ##]
+nqed.
+
+notation > "\move term 90 x term 90 E"
+non associative with precedence 60 for @{move ? $x $E}.
+nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 ∅, false 〉
+ | pe ⇒ 〈 ϵ, false 〉
+ | ps y ⇒ 〈 `y, false 〉
+ | pp y ⇒ 〈 `y, x == y 〉
+ | 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}.
+interpretation "move" 'move x E = (move ? x E).
+
+ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
+interpretation "rmove" 'move x E = (rmove ? x E).
+
+nlemma XXz : ∀S:Alpha.∀w:word S. w .∈ ∅ → False.
+#S w abs; ninversion abs; #; ndestruct;
+nqed.
+
+
+nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
+#S w abs; ninversion abs; #; ndestruct;
+nqed.
+
+nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False.
+#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
+nqed.
+
+
+naxiom in_move_cat:
+ ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
+ (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
+#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
+ncases e1 in H; ncases e2;
+##[##1: *; ##[*; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##|##2: *; ##[*; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##| #r; *; ##[ *; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
+##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
+ #H; ninversion H; nnormalize; #; ndestruct;
+ ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
+##| #r1 r2; *; ##[ *; #defw]
+ ...
+nqed.