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/xoa/or_5.ma".
16 include "ground/xoa/ex_3_1.ma".
17 include "ground/xoa/ex_4_2.ma".
18 include "ground/xoa/ex_4_3.ma".
19 include "ground/xoa/ex_5_3.ma".
20 include "delayed_updating/syntax/term_constructors.ma".
21 include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
23 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
25 inductive bdd: predicate term โ
26 | bdd_oref: โn. bdd #n
27 | bdd_iref: โt,n. bdd t โ bdd ๐n.t
28 | bdd_abst: โt. bdd t โ bdd ๐.t
29 | bdd_appl: โu,t. bdd u โ bdd t โ bdd @u.t
33 "well-formed by-depth delayed (term)"
34 'InPredicateDPhi t = (bdd t).
36 (* Basic destructions *******************************************************)
38 lemma bdd_inv_in_com_gen:
39 โt,p. t ฯต ๐๐ โ p ฯตโฌฆ t โ
40 โจโจ โโn. #n = t & ๐ฑโจnโฉ;๐ = p
41 | โโu,q,n. u ฯต ๐๐ & q ฯตโฌฆ u & ๐n.u = t & ๐ฑโจnโฉ;q = p
42 | โโu,q. u ฯต ๐๐ & q ฯตโฌฆ u & ๐.u = t & ๐;q = p
43 | โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯตโฌฆ u & @v.u = t & ๐;q = p
44 | โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯตโฌฆ v & @v.u = t & ๐ฆ;q = p
47 [ #n * /3 width=3 by or5_intro0, ex2_intro/
48 | #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
49 | #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
50 | #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
54 lemma bdd_inv_in_com_d:
55 โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉ;q ฯตโฌฆ t โ
56 โจโจ โงโง #n = t & ๐ = q
57 | โโu. u ฯต ๐๐ & q ฯตโฌฆ u & ๐n.u = t
60 elim (bdd_inv_in_com_gen โฆ Ht Hq) -Ht -Hq *
61 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
62 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
63 | #u0 #q0 #_ #_ #_ #H0 destruct
64 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
65 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
69 lemma bdd_inv_in_ini_d:
70 โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉ;q ฯตโต t โ
71 โจโจ โงโง #n = t & ๐ = q
72 | โโu. u ฯต ๐๐ & q ฯตโต u & ๐n.u = t
75 elim (bdd_inv_in_com_d โฆ Ht Hq) -Ht -Hq *
77 elim (eq_inv_list_empty_append โฆ H2) -H2 #H2 #_ destruct
78 /3 width=1 by or_introl, conj/
79 | #u #Hu #Hq #H1 destruct
80 /4 width=4 by ex3_intro, ex_intro, or_intror/
85 โl,n,p,t. t ฯต ๐๐ โ p,๐ฑโจnโฉ ฯตโต t โ p,l ฯตโต t โ ๐ฑโจnโฉ = l.
87 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
88 elim (bdd_inv_in_ini_d โฆ Ht Hn) -Ht -Hn *
90 elim (term_in_ini_inv_lcons_oref โฆ Hl) -Hl //
91 | #u #_ #_ #H1 destruct
92 elim (term_in_ini_inv_lcons_iref โฆ Hl) -Hl //
94 | * [ #m ] #p #IH #t #Ht
95 <list_cons_shift <list_cons_shift #Hn #Hl
96 [ elim (bdd_inv_in_ini_d โฆ Ht Hn) -Ht -Hn *
98 elim (eq_inv_list_empty_rcons ??? H)
99 | #u #Hu #Hp #H destruct
100 elim (term_in_ini_inv_lcons_iref โฆ Hl) -Hl #_ #Hl