Library ConvECC


Require Export TermECC.

Section Church_Rosser.

  Definition str_confluent R := commut _ R (transp term R).

  Lemma str_confluence_par_red1 : str_confluent par_red1.

  Lemma strip_lemma : commut _ par_red (transp _ par_red1).

  Lemma confluence_par_red : str_confluent par_red.

  Lemma confluence_red : str_confluent red.

  Theorem church_rosser :
   forall u v, conv u v -> exists2 t : _, red u t & red v t.

  Lemma inv_conv_prod_l :
   forall a b c d, conv (Prod a c) (Prod b d) -> conv a b.

  Lemma inv_conv_prod_r :
   forall a b c d, conv (Prod a c) (Prod b d) -> conv c d.

  Lemma nf_uniqueness : forall u v, conv u v -> normal u -> normal v -> u = v.

  Lemma conv_sort : forall s1 s2, conv (Srt s1) (Srt s2) -> s1 = s2.

  Lemma conv_kind_prop : forall n, ~ conv (Srt (kind n)) (Srt prop).

  Lemma conv_sort_prod : forall s t u, ~ conv (Srt s) (Prod t u).

End Church_Rosser.