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/rintersection_3.ma".
16 include "ground_2/relocation/rtmap_sle.ma".
18 coinductive sand: relation3 rtmap rtmap rtmap ≝
19 | sand_pp: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g
20 | sand_np: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g
21 | sand_pn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → sand g1 g2 g
22 | sand_nn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → sand g1 g2 g
25 interpretation "intersection (rtmap)"
26 'RIntersection f1 f2 f = (sand f1 f2 f).
28 (* Basic properties *********************************************************)
30 let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?.
31 #f cases (pn_split f) * #g #H
32 [ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H //
35 let corec sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f ≝ ?.
36 #f1 #f2 #f * -f1 -f2 -f
37 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
38 [ @sand_pp | @sand_pn | @sand_np | @sand_nn ]
39 [4,11,18,25: @sand_sym // |1,2,3,8,9,10,15,16,17,22,23,24: skip |*: // ]