(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/rt_transition/lfpr_lfpr.ma".

(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)

definition lfxs_confluent_R: relation2 … ≝
                             λRP1,RP2.
                             ∀L0,T0,T1. RP1 L0 T0 T1 → ∀T2. RP2 L0 T0 T2 →
                             ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
                             ∃∃L. L1 ⦻*[RP2, T1] L & L2 ⦻*[RP1, T2] L.

(* Main properties **********************************************************)

fact lfpr_conf_cpr_atom_atom:
   ∀h,I,G,L0. (
      ∀L,T. ⦃G, L0, ⓪{I}⦄ ⊐+ ⦃G, L, T⦄ →
      ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
      ∀L1. ⦃G, L⦄ ⊢ ➡[h, T] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h, T] L2 →
      ∃∃K0. ⦃G, L1⦄ ⊢ ➡[h, T1] K0 & ⦃G, L2⦄ ⊢ ➡[h, T2] K0
   ) →
   ∀L1. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L2 →
   ∃∃L. ⦃G, L1⦄ ⊢ ➡[h, ⓪{I}] L & ⦃G, L2⦄ ⊢ ➡[h, ⓪{I}] L.
#h #I #G * [ | #K0 #J #V0 cases I -I [ | * | ] ]
[ #_ #L1 #HL01 #L2 #HL02
  lapply (lfpr_inv_atom_sn … HL01) -HL01 #H destruct
  lapply (lfpr_inv_atom_sn … HL02) -HL02 #H destruct
  /2 width=3 by ex2_intro/
| #s #IH #L1 #HL01 #L2 #HL02
  elim (lfxs_inv_sort_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  elim (lfxs_inv_sort_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  /3 width=5 by lfpr_sort, fqu_fqup, fqu_drop, ex2_intro/
| #IH #L1 #HL01 #L2 #HL02
  elim (lfpr_inv_zero_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
  elim (lfpr_inv_zero_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
  elim (cpr_conf_lfpr … HV01 … HV02 … HK01 … HK02) #V #HV1 #HV2
  elim (IH … HV01 … HV02 … HK01 … HK02) -IH -HV01 -HV02 -HK01 -HK02
  /3 width=5 by lfpr_zero, fqu_fqup, fqu_drop, ex2_intro/
| #i #IH #L1 #HL01 #L2 #HL02
  elim (lfxs_inv_lref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  elim (lfxs_inv_lref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  /3 width=5 by lfpr_lref, fqu_fqup, fqu_drop, ex2_intro/
| #l #IH #L1 #HL01 #L2 #HL02
  elim (lfxs_inv_gref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  elim (lfxs_inv_gref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  /3 width=5 by lfpr_gref, fqu_fqup, fqu_drop, ex2_intro/
]
qed-.

theorem lfpr_conf_cpr: ∀h,G. lfxs_confluent_R (cpm 0 h G) (cpm 0 h G).
#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
  elim (cpr_inv_atom1_drops … H1) -H1
  elim (cpr_inv_atom1_drops … H2) -H2
  [ #H2 #H1 destruct
    /3 width=7 by lfpr_conf_cpr_atom_atom/
  | * #K0 #V0 #V2 * [2: #i2 ] #HLK0 #HV02 #HVT2 #H2 #H1 destruct

(*

theorem lpr_conf: ∀G. confluent … (lpr G).
/3 width=6 by lpx_sn_conf, cpr_conf_lpr/
qed-.

*)