matita/matita/contribs/lambdadelta/ground_2/etc/lib/star.etc

   1 lemma TC_case_sn: ∀A,R. reflexive A R →
   2                   ∀a1,a2. TC … R a1 a2 → ∃∃a. R a1 a & TC … R a a2.
   3 #A #R #HR #a1 #a2 #H @(TC_ind_dx … a1 H) -a1
   4 [ /3 width=3 by inj, ex2_intro/
   5 | #a1 #a0 #Ha10 #Ha02 #_ /2 width=3 by ex2_intro/ (**) (* auto fails withput #_ *)
   6 ]
   7 qed-.
   8
   9 lemma TC_case_dx: ∀A,R. reflexive A R →
  10                   ∀a1,a2. TC … R a1 a2 → ∃∃a. TC … R a1 a & R a a2.
  11 #A #R #HR #a1 #a2 #H @(TC_ind … a2 H) -a2
  12 [ /3 width=3 by inj, ex2_intro/
  13 | #a0 #a2 #Ha10 #Ha02 #_ /2 width=3 by ex2_intro/ (**) (* auto fails withput #_ *)
  14 ]
  15 qed-.
  16
  17 definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
  18                       ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
  19
  20 definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
  21                        ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
  22
  23 lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S.
  24 #A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
  25 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
  26 lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/
  27 qed-.
  28
  29 lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S).
  30 #A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/
  31 qed-.