matita/matita/contribs/lambdadelta/delayed_updating/etc/lift_path.etc

   1 lemma lift_path_inv_d_sn (f) (p) (q) (k):
   2       (𝗱k◗q) = ↑[f]p →
   3       ∃∃r,h. k = f＠⧣❨h❩ & q = ↑[⇂*[h]f]r & 𝗱h◗r = p.
   4 #f * [| * [ #n ] #p ] #q #k
   5 [ <lift_path_empty
   6 | <lift_path_d_sn
   7 | <lift_path_m_sn
   8 | <lift_path_L_sn
   9 | <lift_path_A_sn
  10 | <lift_path_S_sn
  11 ] #H destruct
  12 /2 width=5 by ex3_2_intro/
  13 qed-.
  14
  15 lemma lift_path_inv_m_sn (f) (p) (q):
  16       (𝗺◗q) = ↑[f]p →
  17       ∃∃r. q = ↑[f]r & 𝗺◗r = p.
  18 #f * [| * [ #n ] #p ] #q
  19 [ <lift_path_empty
  20 | <lift_path_d_sn
  21 | <lift_path_m_sn
  22 | <lift_path_L_sn
  23 | <lift_path_A_sn
  24 | <lift_path_S_sn
  25 ] #H destruct
  26 /2 width=3 by ex2_intro/
  27 qed-.
  28
  29 lemma lift_path_inv_L_sn (f) (p) (q):
  30       (𝗟◗q) = ↑[f]p →
  31       ∃∃r. q = ↑[⫯f]r & 𝗟◗r = p.
  32 #f * [| * [ #n ] #p ] #q
  33 [ <lift_path_empty
  34 | <lift_path_d_sn
  35 | <lift_path_m_sn
  36 | <lift_path_L_sn
  37 | <lift_path_A_sn
  38 | <lift_path_S_sn
  39 ] #H destruct
  40 /2 width=3 by ex2_intro/
  41 qed-.
  42
  43 lemma lift_path_inv_A_sn (f) (p) (q):
  44       (𝗔◗q) = ↑[f]p →
  45       ∃∃r. q = ↑[f]r & 𝗔◗r = p.
  46 #f * [| * [ #n ] #p ] #q
  47 [ <lift_path_empty
  48 | <lift_path_d_sn
  49 | <lift_path_m_sn
  50 | <lift_path_L_sn
  51 | <lift_path_A_sn
  52 | <lift_path_S_sn
  53 ] #H destruct
  54 /2 width=3 by ex2_intro/
  55 qed-.
  56
  57 lemma lift_path_inv_S_sn (f) (p) (q):
  58       (𝗦◗q) = ↑[f]p →
  59       ∃∃r. q = ↑[f]r & 𝗦◗r = p.
  60 #f * [| * [ #n ] #p ] #q
  61 [ <lift_path_empty
  62 | <lift_path_d_sn
  63 | <lift_path_m_sn
  64 | <lift_path_L_sn
  65 | <lift_path_A_sn
  66 | <lift_path_S_sn
  67 ] #H destruct
  68 /2 width=3 by ex2_intro/
  69 qed-.