(* *)
(**************************************************************************)
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "delayed_updating/syntax/prototerm_equivalence.ma".
+include "delayed_updating/notation/functions/class_d_phi_0.ma".
include "ground/xoa/or_5.ma".
include "ground/xoa/ex_3_1.ma".
include "ground/xoa/ex_4_2.ma".
include "ground/xoa/ex_4_3.ma".
include "ground/xoa/ex_5_3.ma".
-include "delayed_updating/syntax/preterm_equivalence.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-include "delayed_updating/notation/functions/class_d_phi_0.ma".
(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
-inductive bdd: π«β¨pretermβ© β
+inductive bdd: π«β¨prototermβ© β
| bdd_oref: βn. bdd (#n)
| bdd_iref: βt,n. bdd t β bdd (πn.t)
| bdd_abst: βt. bdd t β bdd (π.t)
.
interpretation
- "by-depth delayed (preterm)"
+ "by-depth delayed (prototerm)"
'ClassDPhi = (bdd).
(* Basic inversions *********************************************************)
lemma bdd_inv_in_comp_gen:
βt,p. t Ο΅ ππ β p Ο΅ t β
- β¨β¨ ββn. #n β t & π±β¨nβ©βπ = p
- | ββu,q,n. u Ο΅ ππ & q Ο΅ u & πn.u β t & π±β¨nβ©βq = p
+ β¨β¨ ββn. #n β t & π±nβπ = p
+ | ββu,q,n. u Ο΅ ππ & q Ο΅ u & πn.u β t & π±nβq = p
| ββu,q. u Ο΅ ππ & q Ο΅ u & π.u β t & πβq = p
| ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ u & @v.u β t & πβq = p
| ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ v & @v.u β t & π¦βq = p
qed-.
lemma bdd_inv_in_comp_d:
- βt,q,n. t Ο΅ ππ β π±β¨nβ©βq Ο΅ t β
+ βt,q,n. t Ο΅ ππ β π±nβq Ο΅ t β
β¨β¨ β§β§ #n β t & π = q
| ββu. u Ο΅ ππ & q Ο΅ u & πn.u β t
.
qed-.
lemma bdd_inv_in_root_d:
- βt,q,n. t Ο΅ ππ β π±β¨nβ©βq Ο΅ β΅t β
+ βt,q,n. t Ο΅ ππ β π±nβq Ο΅ β΅t β
β¨β¨ β§β§ #n β t & π = q
| ββu. u Ο΅ ππ & q Ο΅ β΅u & πn.u β t
.
(* Advanced inversions ******************************************************)
lemma bbd_mono_in_root_d:
- βl,n,p,t. t Ο΅ ππ β pβπ±β¨nβ© Ο΅ β΅t β pβl Ο΅ β΅t β π±β¨nβ© = l.
+ βl,n,p,t. t Ο΅ ππ β pβπ±n Ο΅ β΅t β pβl Ο΅ β΅t β π±n = l.
#l #n #p elim p -p
[ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
elim (bdd_inv_in_root_d β¦ Ht Hn) -Ht -Hn *
[ #H0 #_
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_oref β¦ Hl) -Hl //
+ elim (prototerm_in_root_inv_lcons_oref β¦ Hl) -Hl //
| #u #_ #_ #H0
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl //
+ elim (prototerm_in_root_inv_lcons_iref β¦ Hl) -Hl //
]
| * [ #m ] #p #IH #t #Ht
<list_cons_shift <list_cons_shift #Hn #Hl
[ #_ #H0
elim (eq_inv_list_empty_rcons ??? H0)
| #u #Hu #Hp #H0
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl #_ #Hl
+ elim (prototerm_in_root_inv_lcons_iref β¦ Hl) -Hl #_ #Hl
/2 width=4 by/
]
| elim (bdd_inv_in_root_L β¦ Ht Hn) -Ht -Hn
#u #Hu #Hp #H0
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_abst β¦ Hl) -Hl #_ #Hl
+ elim (prototerm_in_root_inv_lcons_abst β¦ Hl) -Hl #_ #Hl
/2 width=4 by/
| elim (bdd_inv_in_root_A β¦ Ht Hn) -Ht -Hn
#v #u #_ #Hu #Hp #H0
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
+ elim (prototerm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
| elim (bdd_inv_in_root_S β¦ Ht Hn) -Ht -Hn
#v #u #Hv #_ #Hp #H0
- lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (prototerm_root_eq_repl β¦ H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
+ elim (prototerm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
]
]