[ list_empty β π
| list_lcons l q β
match l with
- [ label_d n β structure q
+ [ label_d k β structure q
| label_m β structure q
- | label_L β πβstructure q
- | label_A β πβstructure q
- | label_S β π¦βstructure q
+ | label_L β (structure q)βπ
+ | label_A β (structure q)βπ
+ | label_S β (structure q)βπ¦
]
].
π = βπ.
// qed.
-lemma structure_d_sn (p) (n):
- βp = β(π±nβp).
+lemma structure_d_dx (p) (k):
+ βp = β(pβπ±k).
// qed.
-lemma structure_m_sn (p):
- βp = β(πΊβp).
+lemma structure_m_dx (p):
+ βp = β(pβπΊ).
// qed.
-lemma structure_L_sn (p):
- (πββp) = β(πβp).
+lemma structure_L_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_A_sn (p):
- (πββp) = β(πβp).
+lemma structure_A_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_S_sn (p):
- (π¦ββp) = β(π¦βp).
+lemma structure_S_dx (p):
+ (βp)βπ¦ = β(pβπ¦).
// qed.
(* Main constructions *******************************************************)
theorem structure_idem (p):
βp = ββp.
-#p elim p -p [| * [ #n ] #p #IH ] //
+#p elim p -p [| * [ #k ] #p #IH ] //
qed.
-theorem structure_append (p1) (p2):
- βp1ββp2 = β(p1βp2).
-#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+theorem structure_append (p) (q):
+ βpββq = β(pβq).
+#p #q elim q -q [| * [ #k ] #q #IH ]
[||*: <list_append_lcons_sn ] //
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma structure_d_dx (p) (n):
- βp = β(pβπ±n).
+lemma structure_d_sn (p) (k):
+ βp = β(π±kβp).
#p #n <structure_append //
qed.
-lemma structure_m_dx (p):
- βp = β(pβπΊ).
+lemma structure_m_sn (p):
+ βp = β(πΊβp).
#p <structure_append //
qed.
-lemma structure_L_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_L_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_A_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_A_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_S_dx (p):
- (βp)βπ¦ = β(pβπ¦).
+lemma structure_S_sn (p):
+ (π¦ββp) = β(π¦βp).
#p <structure_append //
qed.