include "delayed_updating/syntax/prototerm.ma".
include "delayed_updating/notation/functions/m_hook_1.ma".
include "delayed_updating/notation/functions/hash_1.ma".
-include "delayed_updating/notation/functions/phi_2.ma".
+include "delayed_updating/notation/functions/tau_2.ma".
include "delayed_updating/notation/functions/lamda_1.ma".
include "delayed_updating/notation/functions/at_2.ma".
interpretation
"outer variable reference by depth (prototerm)"
- 'Hash n = (prototerm_node_0 (label_d n)).
+ 'Hash k = (prototerm_node_0 (label_d k)).
interpretation
"inner variable reference by depth (prototerm)"
- 'Phi n t = (prototerm_node_1_2 (label_d n) label_m t).
+ 'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
interpretation
"name-free functional abstraction (prototerm)"
(* Basic constructions *******************************************************)
-lemma in_comp_iref (t) (q) (n):
- q Ļµ t ā š±nāšŗāq Ļµ šn.t.
+lemma in_comp_oref_hd (k):
+ (š±kāš) Ļµ ā§£k.
+// qed.
+
+lemma in_comp_iref_hd (t) (q) (k):
+ q Ļµ t ā š±kāšŗāq Ļµ šk.t.
/2 width=3 by ex2_intro/ qed.
-(* Basic Inversions *********************************************************)
+lemma in_comp_abst_hd (t) (q):
+ q Ļµ t ā šāq Ļµ š.t.
+/2 width=3 by ex2_intro/ qed.
-lemma in_comp_inv_iref (t) (p) (n):
- p Ļµ šn.t ā
- āāq. š±nāšŗāq = p & q Ļµ t.
-#t #p #n * #q #Hq #Hp
-/2 width=3 by ex2_intro/
-qed-.
-(* COMMENT
-lemma prototerm_in_root_inv_lcons_oref:
- āp,l,n. lāp Ļµ āµ#n ā
- ā§ā§ š±n = l & š = p.
-#p #l #n * #q
-<list_append_lcons_sn #H0 destruct -H0
-elim (eq_inv_list_empty_append ā¦ e0) -e0 #H0 #_
-/2 width=1 by conj/
-qed-.
+lemma in_comp_appl_sd (u) (t) (q):
+ q Ļµ u ā š¦āq Ļµ ļ¼ u.t.
+/3 width=3 by ex2_intro, or_introl/ qed.
-lemma prototerm_in_root_inv_lcons_iref:
- āt,p,l,n. lāp Ļµ āµšn.t ā
- ā§ā§ š±n = l & p Ļµ āµÉ±.t.
-#t #p #l #n * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct -H0
-/4 width=4 by ex2_intro, ex_intro, conj/
-qed-.
+lemma in_comp_appl_hd (u) (t) (q):
+ q Ļµ t ā šāq Ļµ ļ¼ u.t.
+/3 width=3 by ex2_intro, or_intror/ qed.
+
+(* Basic inversions *********************************************************)
-lemma prototerm_in_root_inv_lcons_mark:
- āt,p,l. lāp Ļµ āµÉ±.t ā
- ā§ā§ šŗ = l & p Ļµ āµt.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_iref (t) (p) (k):
+ p Ļµ šk.t ā
+ āāq. š±kāšŗāq = p & q Ļµ t.
+#t #p #k * #q #Hq #Hp
+/2 width=3 by ex2_intro/
qed-.
-lemma prototerm_in_root_inv_lcons_abst:
- āt,p,l. lāp Ļµ āµš.t ā
- ā§ā§ š = l & p Ļµ āµt.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_abst (t) (p):
+ p Ļµ š.t ā
+ āāq. šāq = p & q Ļµ t.
+#t #p * #q #Hq #Hp
+/2 width=3 by ex2_intro/
qed-.
-lemma prototerm_in_root_inv_lcons_appl:
- āu,t,p,l. lāp Ļµ āµ@u.t ā
- āØāØ ā§ā§ š¦ = l & p Ļµ āµu
- | ā§ā§ š = l & p Ļµ āµt.
-#u #t #p #l * #q * * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/4 width=2 by ex_intro, or_introl, or_intror, conj/
+lemma in_comp_inv_appl (u) (t) (p):
+ p Ļµ ļ¼ u.t ā
+ āØāØ āāq. š¦āq = p & q Ļµ u
+ | āāq. šāq = p & q Ļµ t.
+#u #t #p * * #q #Hq #Hp
+/3 width=3 by ex2_intro, or_introl, or_intror/
qed-.
-*)
+
+(* Advanced inversions ******************************************************)
+
+lemma in_comp_inv_abst_hd (t) (p):
+ (šāp) Ļµ š.t ā p Ļµ t.
+#t #p #H0
+elim (in_comp_inv_abst ā¦ H0) -H0 #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_sd (u) (t) (p):
+ (š¦āp) Ļµ ļ¼ u.t ā p Ļµ u.
+#u #t #p #H0
+elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_hd (u) (t) (p):
+ (šāp) Ļµ ļ¼ u.t ā p Ļµ t.
+#u #t #p #H0
+elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.