matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc

   1 include "delayed_updating/notation/functions/nodelabel_d_2.ma".
   2
   3 | label_d2: pnat → nat → label
   4
   5 interpretation
   6   "variable reference by depth with offset (label)"
   7   'NodeLabelD k d = (label_d2 k d).
   8
   9   | label_d2 k d ⇒ depth q
  10
  11 lemma depth_d2_dx (p) (k) (d):
  12       ♭p = ♭(p◖𝗱❨k,d❩).
  13 // qed.
  14
  15 lemma depth_d2_sn (p) (k) (d):
  16       ♭p = ♭(𝗱❨k,d❩◗p).
  17 // qed.
  18
  19    | label_d2 k d ⇒ structure q
  20
  21 lemma structure_d2_dx (p) (k) (d):
  22       ⊗p = ⊗(p◖𝗱❨k,d❩).
  23 // qed.
  24
  25 lemma structure_d2_sn (p) (k) (d):
  26       ⊗p = ⊗(𝗱❨k,d❩◗p).
  27 #p #k #d <structure_append //
  28 qed.
  29
  30 lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
  31       q◖𝗱❨h,d❩ = ⊗p → ⊥.
  32 #d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
  33 [ <structure_empty #H0 destruct
  34 | <structure_d_dx #H0 /2 width=1 by/
  35 | <structure_d2_dx #H0 /2 width=1 by/
  36 | <structure_m_dx #H0 /2 width=1 by/
  37 | <structure_L_dx #H0 destruct
  38 | <structure_A_dx #H0 destruct
  39 | <structure_S_dx #H0 destruct
  40 ]
  41 qed-.
  42
  43 lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
  44       (𝗱❨h,d❩◗q) = ⊗p → ⊥.
  45 #d #h #q #p >list_cons_comm #H0
  46 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
  47 <list_cons_comm #H0 #H1 #H2 destruct
  48 elim (eq_inv_d2_dx_structure … H0)
  49 qed-.
  50
  51 include "delayed_updating/notation/functions/tau_3.ma".
  52
  53 interpretation
  54   "inner variable reference by depth with offset (prototerm)"
  55   'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
  56
  57 lemma in_comp_iref2 (t) (q) (k) (d):
  58       q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
  59 /2 width=3 by ex2_intro/ qed.
  60
  61 lemma in_comp_inv_iref2 (t) (p) (k) (d):
  62       p ϵ 𝛕❨k,d❩.t →
  63       ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
  64 #t #p #k #d * #q #Hq #Hp
  65 /2 width=3 by ex2_intro/
  66 qed-.
  67
  68 lemma ppc_iref2 (t) (k) (d):
  69       (𝛕❨k,d❩.t) ϵ 𝐏.
  70 #t #k #d #p * #q #Hq #H0 destruct //
  71 qed.
  72
  73 lemma pic_inv_d2_dx (p) (k) (d):
  74       p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
  75 #p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
  76 #q * -q [|*: #q ] #H0 destruct
  77 qed-.