include "delayed_updating/syntax/path.ma".
include "delayed_updating/notation/functions/class_c_1.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_pred_succ.ma".
include "ground/lib/subset.ma".
-
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/syntax/path_height.ma".
+include "ground/generated/insert_eq_1.ma".
(* CLOSED CONDITION FOR PATH ************************************************)
-axiom pcc: relation2 nat path.
+inductive pcc: relation2 nat path โ
+| pcc_empty:
+ pcc (๐) (๐)
+| pcc_d_dx (p) (n) (k):
+ pcc (n+ninj k) p โ pcc n (pโ๐ฑk)
+| pcc_m_dx (p) (n):
+ pcc n p โ pcc n (pโ๐บ)
+| pcc_L_dx (p) (n):
+ pcc n p โ pcc (โn) (pโ๐)
+| pcc_A_dx (p) (n):
+ pcc n p โ pcc n (pโ๐)
+| pcc_S_dx (p) (n):
+ pcc n p โ pcc n (pโ๐ฆ)
+.
interpretation
"closed condition (path)"
'ClassC n = (pcc n).
-(* Basic destructions *******************************************************)
+(* Basic inversions ********************************************************)
+
+lemma pcc_inv_empty (n):
+ (๐) ฯต ๐โจnโฉ โ ๐ = n.
+#n @(insert_eq_1 โฆ (๐))
+#x * -n //
+#p #n [ #k ] #_ #H0 destruct
+qed-.
+
+lemma pcc_inv_d_dx (p) (n) (k):
+ pโ๐ฑk ฯต ๐โจnโฉ โ p ฯต ๐โจn+kโฉ.
+#p #n #h @(insert_eq_1 โฆ (pโ๐ฑh))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_m_dx (p) (n):
+ pโ๐บ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐บ))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_L_dx (p) (n):
+ pโ๐ ฯต ๐โจnโฉ โ
+ โงโง p ฯต ๐โจโnโฉ & n = โโn.
+#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 (p) (n):
+ pโ๐ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_S_dx (p) (n):
+ pโ๐ฆ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐ฆ))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma pcc_inv_empty_succ (n):
+ (๐) ฯต ๐โจโnโฉ โ โฅ.
+#n #H0
+lapply (pcc_inv_empty โฆ H0) -H0 #H0
+/2 width=7 by eq_inv_zero_nsucc/
+qed-.
+
+lemma pcc_inv_L_dx_zero (p):
+ pโ๐ ฯต ๐โจ๐โฉ โ โฅ.
+#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 (p) (n):
+ pโ๐ ฯต ๐โจโnโฉ โ p ฯต ๐โจnโฉ.
+#p #n #H0
+elim (pcc_inv_L_dx โฆ H0) -H0 //
+qed-.
+
+(* Main constructions with path_append **************************************)
+
+theorem pcc_append_bi (p) (q) (m) (n):
+ p ฯต ๐โจmโฉ โ q ฯต ๐โจnโฉ โ pโq ฯต ๐โจm+nโฉ.
+#p #q #m #n #Hm #Hm elim Hm -Hm // -Hm
+#p #n [ #k ] #_ #IH [3: <nplus_succ_dx ]
+/2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma pcc_m_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐บโq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐บ) โฆ Hq) -Hq
+/2 width=3 by pcc_m_dx/
+qed.
+
+lemma pcc_L_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจโnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_L_dx/
+qed.
-axiom pcc_empty:
- (๐) ฯต ๐โจ๐โฉ.
+lemma pcc_A_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_A_dx/
+qed.
-axiom pcc_d (p) (d) (n:pnat):
- p ฯต ๐โจd+nโฉ โ pโ๐ฑn ฯต ๐โจdโฉ.
+lemma pcc_S_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐ฆโq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐ฆ) โฆ Hq) -Hq
+/2 width=3 by pcc_S_dx/
+qed.
-axiom pcc_L (p) (d):
- p ฯต ๐โจdโฉ โ pโ๐ ฯต ๐โจโdโฉ.
+(* Main inversions **********************************************************)
-axiom pcc_A (p) (d):
- p ฯต ๐โจdโฉ โ pโ๐ ฯต ๐โจdโฉ.
+theorem pcc_mono (q) (n1):
+ q ฯต ๐โจn1โฉ โ โn2. q ฯต ๐โจn2โฉ โ n1 = n2.
+#q1 #n1 #Hn1 elim Hn1 -q1 -n1
+[|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
+[ <(pcc_inv_empty โฆ Hn2) -n2 //
+| lapply (pcc_inv_d_dx โฆ Hn2) -Hn2 #Hn2
+ lapply (IH โฆ Hn2) -q1 #H0
+ /2 width=2 by eq_inv_nplus_bi_dx/
+| lapply (pcc_inv_m_dx โฆ Hn2) -Hn2 #Hn2
+ <(IH โฆ Hn2) -q1 -n2 //
+| elim (pcc_inv_L_dx โฆ Hn2) -Hn2 #Hn2 #H0
+ >(IH โฆ Hn2) -q1 //
+| lapply (pcc_inv_A_dx โฆ Hn2) -Hn2 #Hn2
+ <(IH โฆ Hn2) -q1 -n2 //
+| lapply (pcc_inv_S_dx โฆ Hn2) -Hn2 #Hn2
+ <(IH โฆ Hn2) -q1 -n2 //
+]
+qed-.
-axiom pcc_S (p) (d):
- p ฯต ๐โจdโฉ โ pโ๐ฆ ฯต ๐โจdโฉ.
+theorem pcc_inj_L_sn (p1) (p2) (q1) (n):
+ q1 ฯต ๐โจnโฉ โ โq2. q2 ฯต ๐โจnโฉ โ
+ p1โ๐โq1 = p2โ๐โq2 โ q1 = q2.
+#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)
+| lapply (pcc_inv_d_dx โฆ Hq2) -Hq2 #Hq2
+ <(IH โฆ Hq2) //
+| lapply (pcc_inv_m_dx โฆ Hq2) -Hq2 #Hq2
+ <(IH โฆ Hq2) //
+| lapply (pcc_inv_L_dx_succ โฆ Hq2) -Hq2 #Hq2
+ <(IH โฆ Hq2) //
+| lapply (pcc_inv_A_dx โฆ Hq2) -Hq2 #Hq2
+ <(IH โฆ Hq2) //
+| lapply (pcc_inv_S_dx โฆ Hq2) -Hq2 #Hq2
+ <(IH โฆ Hq2) //
+| elim (pcc_inv_empty_succ โฆ Hq2)
+]
+qed-.
-axiom pcc_des_gen (p) (d):
- p ฯต ๐โจdโฉ โ d + โฏp = โpโ.
+theorem pcc_inv_L_sn (q) (n) (m):
+ (๐โq) ฯต ๐โจnโฉ โ q ฯต ๐โจmโฉ โ
+ โงโง โn = m & n = โโn.
+#q #n #m #H1q #H2q
+lapply (pcc_L_sn โฆ H2q) -H2q #H2q
+<(pcc_mono โฆ H2q โฆ H1q) -q -n
+/2 width=1 by conj/
+qed-.