Library lemma_cong_red2_tes


Require Export congr_y_red2_tes.




Inductive common_succ [F:(list pol);g,h:pol]: Prop:=

           common_succ_red: (p:pol)(Red3 F g p)->(Red3 F h p)->(common_succ F g h).

Hints Resolve common_succ_red.




Inductive common_succ_step [f1,f,g:pol]: Prop:=

   common_succ_step_red: (h,p:pol)(full_term_pol h)->

    (full_term_pol p)->(red f1 (suma_app f h) p)->

     (red f1 (suma_app g h) p)->(common_succ_step f1 f g).




Lemma common_is_Red_equiv : (f,g:pol)(F:(list pol))

 (common_succ F f g)->

           (Red_equiv F f g).

(Intros f g F c; Inversion c).

Apply Red_equiv_tran with p; Auto.

Save.

Hints Resolve common_is_Red_equiv.




Lemma trans_equiv_common: (f,g,h:pol)(F:(list pol))

 (Red_equiv F f g)->

   (common_succ F g h)->

           (Red_equiv F f h).

Intros f g h F e c.

(Apply Red_equiv_tran with g; Auto).

Save.




Hints Resolve trans_equiv_common.




Lemma conmt_common_succ: (p,q:pol)(F:(list pol))(common_succ F p q)->

   (common_succ F q p).

Induction 1.

Intros.

Exists p0; Assumption.

Save.

Hints Resolve conmt_common_succ.




Lemma trans_common_red:(f,g,h:pol)(F:(list pol))

 (Red1 F h f)->(common_succ F g f)->

    (common_succ F g h).

Intros.

Inversion H0.

(Apply common_succ_red with p; Trivial).

(Apply Red3_tran with f; Trivial).

(Apply Red3_ste; Trivial).

Save.  

Hints Resolve trans_common_red.
Index
This page has been generated by coqdoc