[ list_empty ā š
| list_lcons l q ā
match l with
- [ label_d k ā structure q
- | label_d2 k d ā structure q
- | label_m ā structure q
- | label_L ā (structure q)āš
- | label_A ā (structure q)āš
- | label_S ā (structure q)āš¦
+ [ label_d k ā structure q
+ | label_m ā structure q
+ | label_L ā (structure q)āš
+ | label_A ā (structure q)āš
+ | label_S ā (structure q)āš¦
]
].
āp = ā(pāš±k).
// qed.
-lemma structure_d2_dx (p) (k) (d):
- āp = ā(pāš±āØk,dā©).
-// qed.
-
lemma structure_m_dx (p):
āp = ā(pāšŗ).
// qed.
theorem structure_idem (p):
āp = āāp.
#p elim p -p //
-* [ #k | #k #d ] #p #IH //
+* [ #k ] #p #IH //
qed.
theorem structure_append (p) (q):
āpāāq = ā(pāq).
#p #q elim q -q //
-* [ #k | #k #d ] #q #IH //
+* [ #k ] #q #IH //
<list_append_lcons_sn //
qed.
#p #k <structure_append //
qed.
-lemma structure_d2_sn (p) (k) (d):
- āp = ā(š±āØk,dā©āp).
-#p #k #d <structure_append //
-qed.
-
lemma structure_m_sn (p):
āp = ā(šŗāp).
#p <structure_append //
lemma eq_inv_d_dx_structure (h) (q) (p):
qāš±h = āp ā ā„.
-#h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#h #q #p elim p -p [| * [ #k ] #p #IH ]
[ <structure_empty #H0 destruct
| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
-| <structure_m_dx #H0 /2 width=1 by/
-| <structure_L_dx #H0 destruct
-| <structure_A_dx #H0 destruct
-| <structure_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
- qāš±āØh,dā© = āp ā ā„.
-#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
-[ <structure_empty #H0 destruct
-| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
| <structure_m_dx #H0 /2 width=1 by/
| <structure_L_dx #H0 destruct
| <structure_A_dx #H0 destruct
lemma eq_inv_m_dx_structure (q) (p):
qāšŗ = āp ā ā„.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
[ <structure_empty #H0 destruct
| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
| <structure_m_dx #H0 /2 width=1 by/
| <structure_L_dx #H0 destruct
| <structure_A_dx #H0 destruct
lemma eq_inv_L_dx_structure (q) (p):
qāš = āp ā
āār1,r2. q = ār1 & š = ār2 & r1āšār2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
[ <structure_empty #H0 destruct
| <structure_d_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
- elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
- /2 width=5 by ex3_2_intro/
| <structure_m_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
lemma eq_inv_A_dx_structure (q) (p):
qāš = āp ā
āār1,r2. q = ār1 & š = ār2 & r1āšār2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
[ <structure_empty #H0 destruct
| <structure_d_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
- elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
- /2 width=5 by ex3_2_intro/
| <structure_m_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
lemma eq_inv_S_dx_structure (q) (p):
qāš¦ = āp ā
āār1,r2. q = ār1 & š = ār2 & r1āš¦ār2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
[ <structure_empty #H0 destruct
| <structure_d_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
- elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
- /2 width=5 by ex3_2_intro/
| <structure_m_dx #H0
elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
/2 width=5 by ex3_2_intro/
theorem eq_inv_append_structure (p) (q) (r):
pāq = ār ā
āār1,r2.p = ār1 & q = ār2 & r1ār2 = r.
-#p #q elim q -q [| * [ #k | #k #d ] #q #IH ] #r
+#p #q elim q -q [| * [ #k ] #q #IH ] #r
[ <list_append_empty_sn #H0 destruct
/2 width=5 by ex3_2_intro/
| #H0 elim (eq_inv_d_dx_structure ā¦ H0)
-| #H0 elim (eq_inv_d2_dx_structure ā¦ H0)
| #H0 elim (eq_inv_m_dx_structure ā¦ H0)
| #H0 elim (eq_inv_L_dx_structure ā¦ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (IH ā¦ Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
elim (eq_inv_d_dx_structure ā¦ H0)
qed-.
-lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
- (š±āØh,dā©āq) = āp ā ā„.
-#d #h #q #p >list_cons_comm #H0
-elim (eq_inv_append_structure ā¦ H0) -H0 #r1 #r2
-<list_cons_comm #H0 #H1 #H2 destruct
-elim (eq_inv_d2_dx_structure ā¦ H0)
-qed-.
-
lemma eq_inv_m_sn_structure (q) (p):
(šŗ āq) = āp ā ā„.
#q #p >list_cons_comm #H0