match l with
[ label_d n ⇒
match q with
- [ list_empty ⇒ 𝗱(f@❨n❩)◗(unwind_gen f q)
+ [ list_empty ⇒ 𝗱((f n)@❨n❩)◗(unwind_gen f q)
| list_lcons _ _ ⇒ unwind_gen f q
]
| label_m ⇒ unwind_gen f q
// qed.
lemma unwind_gen_d_empty (f) (n):
- 𝗱(f@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
+ 𝗱((f n)@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
// qed.
lemma unwind_gen_d_lcons (f) (p) (l) (n):
(* Properties with tr_compose ***********************************************)
lemma unwind_gen_after (f2) (f1) (p):
- ◆[f2]◆[f1]p = ◆[f2∘f1]p.
+ ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p.
#f2 #f1 #p @(path_ind_unwind … p) -p //
+#n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
qed.
(* Constructions with stream_eq *********************************************)
-lemma unwind_gen_eq_repl (p):
- stream_eq_repl … (λf1,f2. ◆[f1]p = ◆[f2]p).
-#p @(path_ind_unwind … p) -p // [ #n |*: #p ] #IH #f1 #f2 #Hf
+lemma unwind_gen_eq_repl (p) (f1) (f2):
+ (∀n. f1 n ≗ f2 n) → ◆[f1]p = ◆[f2]p.
+#p @(path_ind_unwind … p) -p // [ #n | #n #l #p |*: #p ] #IH #f1 #f2 #Hf
[ <unwind_gen_d_empty <unwind_gen_d_empty
- <(tr_pap_eq_repl … Hf) -f2 -IH //
+ <(tr_pap_eq_repl … (Hf n)) -f2 -IH //
+| <unwind_gen_d_lcons <unwind_gen_d_lcons
+ <(IH … Hf) -f2 -IH //
+| <unwind_gen_m_sn <unwind_gen_m_sn
+ <(IH … Hf) -f2 -IH //
| <unwind_gen_L_sn <unwind_gen_L_sn
<(IH … Hf) -f2 -IH //
| <unwind_gen_A_sn <unwind_gen_A_sn
(* Advanced constructions with list_rcons ***********************************)
lemma unwind_gen_d_empty_dx (n) (p) (f):
- (⊗p)◖𝗱(f@❨n❩) = ◆[f](p◖𝗱n).
+ (⊗p)◖𝗱((f n)@❨n❩) = ◆[f](p◖𝗱n).
#n #p #f <unwind_gen_append_proper_dx //
qed.
lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
(𝗱k◗q) = ◆[f]p →
- ∃∃r,h. 𝐞 = ⊗r & f@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+ ∃∃r,h. 𝐞 = ⊗r & (f h)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
#k #q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_gen_empty #H destruct