(* *)
(**************************************************************************)
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "delayed_updating/syntax/prototerm_eq.ma".
+include "delayed_updating/notation/functions/class_d_tau_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❩ ≝
-| bdd_oref: ∀n. bdd (#n)
-| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
+inductive bdd: 𝒫❨prototerm❩ ≝
+| bdd_oref: ∀k. bdd (⧣k)
+| bdd_iref: ∀t,k. bdd t → bdd (𝛕k.t)
| bdd_abst: ∀t. bdd t → bdd (𝛌.t)
-| bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t)
+| bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t)
| bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
.
interpretation
- "by-depth delayed (preterm)"
- 'ClassDPhi = (bdd).
+ "by-depth delayed (prototerm)"
+ 'ClassDTau = (bdd).
+
+(* COMMENT
(* Basic inversions *********************************************************)
lemma bdd_inv_in_comp_gen:
- â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\97 → p ϵ t →
- ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩◗𝐞 = p
- | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & ð\9d\9b\97n.u â\87\94 t & ð\9d\97±â\9d¨nâ\9d©◗q = p
- | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
- | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
- | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
+ â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\95 → p ϵ t →
+ ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
+ | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & ð\9d\9b\95n.u â\87\94 t & ð\9d\97±nâ\97\97ð\9d\97º◗q = p
+ | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
+ | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
+ | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
.
#t #p #H elim H -H
[ #n * /3 width=3 by or5_intro0, ex2_intro/
qed-.
lemma bdd_inv_in_comp_d:
- â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\97 â\86\92 ð\9d\97±â\9d¨nâ\9d©◗q ϵ t →
+ â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\95 â\86\92 ð\9d\97±n◗q ϵ t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
- | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & ð\9d\9b\97n.u ⇔ t
+ | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ ɱ.u & ð\9d\9b\95n.u ⇔ t
.
#t #q #n #Ht #Hq
elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
[ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
-| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
+| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct
+ /4 width=4 by ex3_intro, ex2_intro, or_intror/
| #u0 #q0 #_ #_ #_ #H0 destruct
| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
qed-.
lemma bdd_inv_in_root_d:
- â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\97 â\86\92 ð\9d\97±â\9d¨nâ\9d©◗q ϵ ▵t →
+ â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\95 â\86\92 ð\9d\97±n◗q ϵ ▵t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
- | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ â\96µu & ð\9d\9b\97n.u ⇔ t
+ | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ â\96µÉ±.u & ð\9d\9b\95n.u ⇔ t
.
#t #q #n #Ht * #r #Hq
elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_comp_L:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗟◗q ϵ t →
- â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & 𝛌.u ⇔ t
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗟◗q ϵ t →
+ â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & 𝛌.u ⇔ t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_L:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗟◗q ϵ ▵t →
- â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵u & 𝛌.u ⇔ t.
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗟◗q ϵ ▵t →
+ â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ ▵u & 𝛌.u ⇔ t.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
#u #Hu #Hq #H0 destruct
qed-.
lemma bdd_inv_in_comp_A:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗔◗q ϵ t →
- â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & @v.u ⇔ t
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗔◗q ϵ t →
+ â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & @v.u ⇔ t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_A:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗔◗q ϵ ▵t →
- â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵u & @v.u ⇔ t
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗔◗q ϵ ▵t →
+ â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ ▵u & @v.u ⇔ t
.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
qed-.
lemma bdd_inv_in_comp_S:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗦◗q ϵ t →
- â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ v & @v.u ⇔ t
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗦◗q ϵ t →
+ â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ v & @v.u ⇔ t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_S:
- â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗦◗q ϵ ▵t →
- â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵v & @v.u ⇔ t
+ â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗦◗q ϵ ▵t →
+ â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ ▵v & @v.u ⇔ t
.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
(* Advanced inversions ******************************************************)
lemma bbd_mono_in_root_d:
- â\88\80l,n,p,t. t ϵ ð\9d\90\83ð\9d\9b\97 â\86\92 pâ\97\96ð\9d\97±â\9d¨nâ\9d© ϵ â\96µt â\86\92 pâ\97\96l ϵ â\96µt â\86\92 ð\9d\97±â\9d¨nâ\9d© = l.
+ â\88\80l,n,p,t. t ϵ ð\9d\90\83ð\9d\9b\95 â\86\92 pâ\97\96ð\9d\97±n ϵ â\96µt â\86\92 pâ\97\96l ϵ â\96µt â\86\92 ð\9d\97±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/
]
]
qed-.
+*)