(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/class_c_2.ma".
+include "delayed_updating/notation/functions/class_c_3.ma".
include "ground/arith/nat_plus_pred.ma".
include "ground/lib/subset.ma".
include "ground/lib/bool_and.ma".
(* CLOSED CONDITION FOR PATH ************************************************)
-inductive pcc (o): relation2 nat path β
+inductive pcc (o) (e): relation2 nat path β
| pcc_empty:
- pcc o (π) (π)
+ pcc o e e (π)
| pcc_d_dx (p) (n) (k):
(β = o β n = ββn) β
- pcc o (n+ninj k) p β pcc o n (pβπ±k)
+ pcc o e (n+ninj k) p β pcc o e n (pβπ±k)
| pcc_m_dx (p) (n):
- pcc o n p β pcc o n (pβπΊ)
+ pcc o e n p β pcc o e n (pβπΊ)
| pcc_L_dx (p) (n):
- pcc o n p β pcc o (βn) (pβπ)
+ pcc o e n p β pcc o e (βn) (pβπ)
| pcc_A_dx (p) (n):
- pcc o n p β pcc o n (pβπ)
+ pcc o e n p β pcc o e n (pβπ)
| pcc_S_dx (p) (n):
- pcc o n p β pcc o n (pβπ¦)
+ pcc o e n p β pcc o e n (pβπ¦)
.
interpretation
"closed condition (path)"
- 'ClassC o n = (pcc o n).
+ 'ClassC o n e = (pcc o e n).
(* Advanced constructions ***************************************************)
-lemma pcc_false_d_dx (p) (n) (k:pnat):
- p Ο΅ πβ¨β»,n+kβ© β pβπ±k Ο΅ πβ¨β»,nβ©.
-#p #n #k #H0
+lemma pcc_false_d_dx (e) (p) (n) (k:pnat):
+ p Ο΅ πβ¨β»,n+k,eβ© β pβπ±k Ο΅ πβ¨β»,n,eβ©.
+#e #p #n #k #H0
@pcc_d_dx [| // ]
#H0 destruct
qed.
-lemma pcc_true_d_dx (p) (n:pnat) (k:pnat):
- p Ο΅ πβ¨β,n+kβ© β pβπ±k Ο΅ πβ¨β,nβ©.
+lemma pcc_true_d_dx (e) (p) (n:pnat) (k:pnat):
+ p Ο΅ πβ¨β,n+k,eβ© β pβπ±k Ο΅ πβ¨β,n,eβ©.
/2 width=1 by pcc_d_dx/
qed.
+lemma pcc_plus_bi_dx (o) (e) (p) (n):
+ p Ο΅ πβ¨o,n,eβ© β
+ βm. p Ο΅ πβ¨o,n+m,e+mβ©.
+#o #e #p #n #H0 elim H0 -p -n //
+#p #n [ #k #Ho ] #_ #IH #m
+[|*: /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/ ]
+@pcc_d_dx // -IH #H0
+>Ho -Ho // <nplus_succ_sn //
+qed.
+
(* Basic inversions ********************************************************)
-lemma pcc_inv_empty (o) (n):
- (π) Ο΅ πβ¨o,nβ© β π = n.
-#o #n @(insert_eq_1 β¦ (π))
+lemma pcc_inv_empty (o) (e) (n):
+ (π) Ο΅ πβ¨o,n,eβ© β e = n.
+#o #e #n @(insert_eq_1 β¦ (π))
#x * -n //
#p #n [ #k #_ ] #_ #H0 destruct
qed-.
alias symbol "UpArrow" (instance 3) = "successor (non-negative integers)".
alias symbol "and" (instance 1) = "logical and".
-lemma pcc_inv_d_dx (o) (p) (n) (k):
- pβπ±k Ο΅ πβ¨o, nβ© β
+lemma pcc_inv_d_dx (o) (e) (p) (n) (k):
+ pβπ±k Ο΅ πβ¨o,n,eβ© β
β§β§ (β = o β n = ββn)
- & p Ο΅ πβ¨o, n+kβ©.
-#o #p #n #h @(insert_eq_1 β¦ (pβπ±h))
+ & p Ο΅ πβ¨o,n+k,eβ©.
+#o #e #p #n #h @(insert_eq_1 β¦ (pβπ±h))
#x * -x -n
[|*: #x #n [ #k #Ho ] #Hx ] #H0 destruct
/3 width=1 by conj/
qed-.
-lemma pcc_inv_m_dx (o) (p) (n):
- pβπΊ Ο΅ πβ¨o,nβ© β p Ο΅ πβ¨o,nβ©.
-#o #p #n @(insert_eq_1 β¦ (pβπΊ))
+lemma pcc_inv_m_dx (o) (e) (p) (n):
+ pβπΊ Ο΅ πβ¨o,n,eβ© β p Ο΅ πβ¨o,n,eβ©.
+#o #e #p #n @(insert_eq_1 β¦ (pβπΊ))
#x * -x -n
[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
qed-.
-lemma pcc_inv_L_dx (o) (p) (n):
- pβπ Ο΅ πβ¨o,nβ© β
- β§β§ p Ο΅ πβ¨o,βnβ© & n = ββn.
-#o #p #n @(insert_eq_1 β¦ (pβπ))
+lemma pcc_inv_L_dx (o) (e) (p) (n):
+ pβπ Ο΅ πβ¨o,n,eβ© β
+ β§β§ p Ο΅ πβ¨o,βn,eβ© & n = ββn.
+#o #e #p #n @(insert_eq_1 β¦ (pβπ))
#x * -x -n
[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct
<npred_succ /2 width=1 by conj/
qed-.
-lemma pcc_inv_A_dx (o) (p) (n):
- pβπ Ο΅ πβ¨o,nβ© β p Ο΅ πβ¨o,nβ©.
-#o #p #n @(insert_eq_1 β¦ (pβπ))
+lemma pcc_inv_A_dx (o) (e) (p) (n):
+ pβπ Ο΅ πβ¨o,n,eβ© β p Ο΅ πβ¨o,n,eβ©.
+#o #e #p #n @(insert_eq_1 β¦ (pβπ))
#x * -x -n
[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
qed-.
-lemma pcc_inv_S_dx (o) (p) (n):
- pβπ¦ Ο΅ πβ¨o,nβ© β p Ο΅ πβ¨o,nβ©.
-#o #p #n @(insert_eq_1 β¦ (pβπ¦))
+lemma pcc_inv_S_dx (o) (e) (p) (n):
+ pβπ¦ Ο΅ πβ¨o,n,eβ© β p Ο΅ πβ¨o,n,eβ©.
+#o #e #p #n @(insert_eq_1 β¦ (pβπ¦))
#x * -x -n
[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
qed-.
(* Advanced destructions ****************************************************)
-lemma pcc_des_d_dx (o) (p) (n) (k):
- pβπ±k Ο΅ πβ¨o,nβ© β p Ο΅ πβ¨o,n+kβ©.
-#o #p #n #k #H0
+lemma pcc_des_d_dx (o) (e) (p) (n) (k):
+ pβπ±k Ο΅ πβ¨o,n,eβ© β p Ο΅ πβ¨o,n+k,eβ©.
+#o #e #p #n #k #H0
elim (pcc_inv_d_dx β¦ H0) -H0 #H1 #H2 //
qed-.
-lemma pcc_des_gen (o) (p) (n):
- p Ο΅ πβ¨o,nβ© β p Ο΅ πβ¨β»,nβ©.
-#o #p #n #H0 elim H0 -p -n //
+lemma pcc_des_gen (o) (e) (p) (n):
+ p Ο΅ πβ¨o,n,eβ© β p Ο΅ πβ¨β»,n,eβ©.
+#o #e #p #n #H0 elim H0 -p -n //
#p #n [ #k #Ho ] #_ #IH
/2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/
qed-.
(* Advanced inversions ******************************************************)
-lemma pcc_inv_empty_succ (o) (n):
- (π) Ο΅ πβ¨o,βnβ© β β₯.
+lemma pcc_inv_empty_succ_zero (o) (n):
+ (π) Ο΅ πβ¨o,βn,πβ© β β₯.
#o #n #H0
lapply (pcc_inv_empty β¦ H0) -H0 #H0
/2 width=7 by eq_inv_zero_nsucc/
qed-.
-lemma pcc_true_inv_d_dx_zero (p) (k):
- pβπ±k Ο΅ πβ¨β,πβ© β β₯.
-#p #k #H0
+lemma pcc_true_inv_d_dx_zero_sn (e) (p) (k):
+ pβπ±k Ο΅ πβ¨β,π, eβ© β β₯.
+#e #p #k #H0
elim (pcc_inv_d_dx β¦ H0) -H0 #H0 #_
elim (eq_inv_zero_nsucc β¦ (H0 ?)) -H0 //
qed-.
-lemma pcc_inv_L_dx_zero (o) (p):
- pβπ Ο΅ πβ¨o,πβ© β β₯.
-#o #p #H0
+lemma pcc_inv_L_dx_zero_sn (o) (e) (p):
+ pβπ Ο΅ πβ¨o,π,eβ© β β₯.
+#o #e #p #H0
elim (pcc_inv_L_dx β¦ H0) -H0 #_ #H0
/2 width=7 by eq_inv_zero_nsucc/
qed-.
-lemma pcc_inv_L_dx_succ (o) (p) (n):
- pβπ Ο΅ πβ¨o,βnβ© β p Ο΅ πβ¨o,nβ©.
-#o #p #n #H0
+lemma pcc_inv_L_dx_succ (o) (e) (p) (n):
+ pβπ Ο΅ πβ¨o,βn,eβ© β p Ο΅ πβ¨o,n,eβ©.
+#o #e #p #n #H0
elim (pcc_inv_L_dx β¦ H0) -H0 //
qed-.
(* Constructions with land **************************************************)
-lemma pcc_land_dx (o1) (o2) (p) (n):
- p Ο΅ πβ¨o1,nβ© β p Ο΅ πβ¨o1β§o2,nβ©.
+lemma pcc_land_dx (o1) (o2) (e) (p) (n):
+ p Ο΅ πβ¨o1,n,eβ© β p Ο΅ πβ¨o1β§o2,n,eβ©.
#o1 * /2 width=2 by pcc_des_gen/
qed.
-lemma pcc_land_sn (o1) (o2) (p) (n):
- p Ο΅ πβ¨o2,nβ© β p Ο΅ πβ¨o1β§o2,nβ©.
+lemma pcc_land_sn (o1) (o2) (e) (p) (n):
+ p Ο΅ πβ¨o2,n,eβ© β p Ο΅ πβ¨o1β§o2,n,eβ©.
* /2 width=2 by pcc_des_gen/
qed.
(* Main constructions with path_append **************************************)
-theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
- p Ο΅ πβ¨o1,mβ© β q Ο΅ πβ¨o2,nβ© β pβq Ο΅ πβ¨o1β§o2,m+nβ©.
-#o1 #o2 #p #q #m #n #Hm #Hn elim Hn -q -n
-/2 width=1 by pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_land_dx/
+theorem pcc_append_bi (o1) (o2) (e1) (e2) (p) (q) (m) (n):
+ p Ο΅ πβ¨o1,m,e1β© β q Ο΅ πβ¨o2,n,e2β© β pβq Ο΅ πβ¨o1β§o2,m+n,e1+e2β©.
+#o1 #o2 #e1 #e2 #p #q #m #n #Hm #Hn elim Hn -q -n
+/3 width=1 by pcc_land_dx, pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_plus_bi_dx/
#q #n [ #k #Ho2 ] #_ #IH
[ @pcc_d_dx // #H0
elim (andb_inv_true_sn β¦ H0) -H0 #_ #H0 >Ho2 //
(* Inversions with path_append **********************************************)
-lemma pcc_false_inv_append_bi (x) (m) (n):
- x Ο΅ πβ¨β»,m+nβ© β
- ββp,q. p Ο΅ πβ¨β»,mβ© & q Ο΅ πβ¨β»,nβ© & pβq = x.
+lemma pcc_false_zero_dx_inv_append_bi (x) (m) (n):
+ x Ο΅ πβ¨β»,m+n,πβ© β
+ ββp,q. p Ο΅ πβ¨β»,m,πβ© & q Ο΅ πβ¨β»,n,πβ© & pβq = x.
#x #m #n #Hx
@(insert_eq_1 β¦ (m+n) β¦ Hx) -Hx #y #Hy
generalize in match n; -n
(* Constructions with path_lcons ********************************************)
-lemma pcc_m_sn (o) (q) (n):
- q Ο΅ πβ¨o,nβ© β (πΊβq) Ο΅ πβ¨o,nβ©.
-#o #q #n #Hq
-lapply (pcc_append_bi (β) β¦ (πβπΊ) β¦ Hq) -Hq
+lemma pcc_m_sn (o) (e) (q) (n):
+ q Ο΅ πβ¨o,n,eβ© β (πΊβq) Ο΅ πβ¨o,n,eβ©.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Γ’\93\89) Γ’\80Β¦ (Γ°\9d\9f\8e) e Γ’\80Β¦ (Γ°\9d\90\9eΓ’\97\96Γ°\9d\97ΒΊ) Γ’\80Β¦ Hq) -Hq
/2 width=3 by pcc_m_dx/
qed.
-lemma pcc_L_sn (o) (q) (n):
- q Ο΅ πβ¨o,nβ© β (πβq) Ο΅ πβ¨o,βnβ©.
-#o #q #n #Hq
-lapply (pcc_append_bi (β) β¦ (πβπ) β¦ Hq) -Hq
+lemma pcc_L_sn (o) (e) (q) (n):
+ q Ο΅ πβ¨o,n,eβ© β (πβq) Ο΅ πβ¨o,βn,eβ©.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Γ’\93\89) Γ’\80Β¦ (Γ°\9d\9f\8e) e Γ’\80Β¦ (Γ°\9d\90\9eΓ’\97\96Γ°\9d\97\9f) Γ’\80Β¦ Hq) -Hq
/2 width=3 by pcc_L_dx/
qed.
-lemma pcc_A_sn (o) (q) (n):
- q Ο΅ πβ¨o,nβ© β (πβq) Ο΅ πβ¨o,nβ©.
-#o #q #n #Hq
-lapply (pcc_append_bi (β) β¦ (πβπ) β¦ Hq) -Hq
+lemma pcc_A_sn (o) (e) (q) (n):
+ q Ο΅ πβ¨o,n,eβ© β (πβq) Ο΅ πβ¨o,n,eβ©.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Γ’\93\89) Γ’\80Β¦ (Γ°\9d\9f\8e) e Γ’\80Β¦ (Γ°\9d\90\9eΓ’\97\96Γ°\9d\97\94) Γ’\80Β¦ Hq) -Hq
/2 width=3 by pcc_A_dx/
qed.
-lemma pcc_S_sn (o) (q) (n):
- q Ο΅ πβ¨o,nβ© β (π¦βq) Ο΅ πβ¨o,nβ©.
-#o #q #n #Hq
-lapply (pcc_append_bi (β) β¦ (πβπ¦) β¦ Hq) -Hq
+lemma pcc_S_sn (o) (e) (q) (n):
+ q Ο΅ πβ¨o,n,eβ© β (π¦βq) Ο΅ πβ¨o,n,eβ©.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Γ’\93\89) Γ’\80Β¦ (Γ°\9d\9f\8e) e Γ’\80Β¦ (Γ°\9d\90\9eΓ’\97\96Γ°\9d\97Β¦) Γ’\80Β¦ Hq) -Hq
/2 width=3 by pcc_S_dx/
qed.
(* Main inversions **********************************************************)
-theorem pcc_mono (o1) (o2) (q) (n1):
- q Ο΅ πβ¨o1,n1β© β βn2. q Ο΅ πβ¨o2,n2β© β n1 = n2.
-#o1 #o2 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
+theorem pcc_mono (o1) (o2) (e) (q) (n1):
+ q Ο΅ πβ¨o1,n1,eβ© β βn2. q Ο΅ πβ¨o2,n2,eβ© β n1 = n2.
+#o1 #o2 #e #q1 #n1 #Hn1 elim Hn1 -q1 -n1
[|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2
[ <(pcc_inv_empty β¦ Hn2) -n2 //
| lapply (pcc_des_d_dx β¦ Hn2) -Hn2 #Hn2
]
qed-.
-theorem pcc_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
- q1 Ο΅ πβ¨o1,nβ© β βq2. q2 Ο΅ πβ¨o2,nβ© β
+theorem pcc_zero_dx_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
+ q1 Ο΅ πβ¨o1,n,πβ© β βq2. q2 Ο΅ πβ¨o2,n,πβ© β
p1βπβq1 = p2βπβq2 β q1 = q2.
#o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
[|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * //
[1,3,5,7,9,11: #l2 #q2 ] #Hq2
<list_append_lcons_sn <list_append_lcons_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
-[ elim (pcc_inv_L_dx_zero β¦ Hq2)
+[ elim (pcc_inv_L_dx_zero_sn β¦ Hq2)
| lapply (pcc_des_d_dx β¦ Hq2) -Hq2 #Hq2
<(IH β¦ Hq2) //
| lapply (pcc_inv_m_dx β¦ Hq2) -Hq2 #Hq2
<(IH β¦ Hq2) //
| lapply (pcc_inv_S_dx β¦ Hq2) -Hq2 #Hq2
<(IH β¦ Hq2) //
-| elim (pcc_inv_empty_succ β¦ Hq2)
+| elim (pcc_inv_empty_succ_zero β¦ Hq2)
]
qed-.
-theorem pcc_inv_L_sn (o) (q) (n) (m):
- (πβq) Ο΅ πβ¨o,nβ© β q Ο΅ πβ¨o,mβ© β
+theorem pcc_inv_L_sn (o) (e) (q) (n) (m):
+ (πβq) Ο΅ πβ¨o,n,eβ© β q Ο΅ πβ¨o,m,eβ© β
β§β§ βn = m & n = ββn.
-#o #q #n #m #H1q #H2q
+#o #e #q #n #m #H1q #H2q
lapply (pcc_L_sn β¦ H2q) -H2q #H2q
<(pcc_mono β¦ H2q β¦ H1q) -q -n
/2 width=1 by conj/