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 "delayed_updating/syntax/path.ma".
16 include "delayed_updating/notation/functions/class_i_0.ma".
17 include "ground/lib/subset.ma".
18 include "ground/generated/insert_eq_1.ma".
20 (* INNER CONDITION FOR PATH *************************************************)
22 inductive pic: predicate path ā
23 | pic_empty: (š) Ļµ pic
24 | pic_m_dx (p): pāšŗ Ļµ pic
25 | pic_L_dx (p): pāš Ļµ pic
26 | pic_A_dx (p): pāš Ļµ pic
27 | pic_S_dx (p): pāš¦ Ļµ pic
31 "inner condition (path)"
34 (* Basic inversions ********************************************************)
36 lemma pic_inv_d_dx (p) (k):
37 pāš±k Ļµ š ā ā„.
38 #p #k @(insert_eq_1 ā¦ (pāš±k))
39 #q * -q [|*: #q ] #H0 destruct
42 lemma pic_inv_d2_dx (p) (k) (d):
43 pāš±āØk,dā© Ļµ š ā ā„.
44 #p #k #d @(insert_eq_1 ā¦ (pāš±āØk,dā©))
45 #q * -q [|*: #q ] #H0 destruct
48 (* Constructions with path_lcons ********************************************)
51 p Ļµ š ā šŗāp Ļµ š.
56 p Ļµ š ā šāp Ļµ š.
61 p Ļµ š ā šāp Ļµ š.
66 p Ļµ š ā š¦āp Ļµ š.