1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/relations/runion_3.ma".
16 include "ground_2/relocation/trace.ma".
18 (* RELOCATION TRACE *********************************************************)
20 inductive sor: relation3 trace trace trace ≝
21 | sor_empty: sor (◊) (◊) (◊)
22 | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs →
23 ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs).
27 'RUnion L1 L2 L = (sor L2 L1 L).
29 (* Basic properties *********************************************************)
31 lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs.
32 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/