matita/matita/contribs/lambda-delta/Ground-2/star.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/star.ma".
  16 include "Ground-2/xoa_props.ma".
  17
  18 (* PROPERTIES of RELATIONS **************************************************)
  19
  20 definition confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
  21                       ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
  22                       ∃∃a. R a1 a & R a2 a.
  23
  24 lemma TC_strip: ∀A,R. confluent A R →
  25                 ∀a0,a1. TC … R a0 a1 → ∀a2. R a0 a2 →
  26                 ∃∃a. R a1 a & TC … R a2 a.
  27 #A #R #HR #a0 #a1 #H elim H -H a1
  28 [ #a1 #Ha01 #a2 #Ha02
  29   elim (HR … Ha01 … Ha02) -HR a0 /3/
  30 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  31   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
  32   elim (HR … Ha1 … Ha0) -HR a /4/
  33 ]
  34 qed.
  35
  36 lemma TC_confluent: ∀A,R. confluent A R → confluent A (TC … R).
  37 #A #R #HR #a0 #a1 #H elim H -H a1
  38 [ #a1 #Ha01 #a2 #Ha02
  39   elim (TC_strip … HR … Ha02 … Ha01) -HR a0 /3/
  40 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  41   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
  42   elim (TC_strip … HR … Ha0 … Ha1) -HR a /4/
  43 ]
  44 qed.
  45
  46 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
  47 /2/ qed.
  48