matita/matita/contribs/lambdadelta/static_2/syntax/teqg_teqg.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 "static_2/syntax/teqg.ma".
  16
  17 (* GENERIC EQUIVALENCE ON TERMS *********************************************)
  18
  19 (* Main properties **********************************************************)
  20
  21 theorem teqg_trans (S):
  22         Transitive … S → Transitive … (teqg S).
  23 #S #HS #T1 #T #H elim H -T1 -T //
  24 [ #s1 #s #Hs1 #X #H
  25   elim (teqg_inv_sort1 … H) -H /3 width=3 by teqg_sort/
  26 | #I #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H
  27   elim (teqg_inv_pair1 … H) -H /3 width=1 by teqg_pair/
  28 ]
  29 qed-.
  30
  31 theorem teqg_canc_sn (S):
  32         symmetric … S → Transitive … S →
  33         left_cancellable … (teqg S).
  34 /3 width=3 by teqg_trans, teqg_sym/ qed-.
  35
  36 theorem teqg_canc_dx (S):
  37         symmetric … S → Transitive … S →
  38         right_cancellable … (teqg S).
  39 /3 width=3 by teqg_trans, teqg_sym/ qed-.
  40
  41 theorem teqg_repl (S):
  42         symmetric … S → Transitive … S →
  43         replace_2 … (teqg S) (teqg S) (teqg S).
  44 /3 width=3 by teqg_canc_sn, teqg_trans/ qed-.
  45
  46 (* Negated main properies ***************************************************)
  47
  48 theorem teqg_tneqg_trans (S):
  49         symmetric … S → Transitive … S →
  50         ∀T1,T. T1 ≛[S] T → ∀T2. (T ≛[S] T2 → ⊥) → T1 ≛[S] T2 → ⊥.
  51 /3 width=3 by teqg_canc_sn/ qed-.
  52
  53 theorem tneqg_teqg_canc_dx (S):
  54         Transitive … S →
  55         ∀T1,T. (T1 ≛[S] T → ⊥) → ∀T2. T2 ≛[S] T → T1 ≛[S] T2 → ⊥.
  56 /3 width=3 by teqg_trans/ qed-.