proposition: Theorem Conf_trans : forall (Q : list (poly A0 eqA ltM)) (a b c d : Term A n) (p0 q r t : list (Term A n)), Reducep Q (pX a p0) (pX c r) (pX d t) -> Reducep Q (pX a p0) (pX d t) (pX b q) -> Confluent Q (pX a p0) (pX c r) (pX d t) -> Confluent Q (pX a p0) (pX d t) (pX b q) -> canonical A0 eqA ltM (pX a p0) -> canonical A0 eqA ltM (pX d t) -> Confluent Q (pX a p0) (pX c r) (pX b q).
proof: Proof. Proof using plusA os cs. intros Q a b c d p q r t H' H'0 H'1 H'2 H'3 H'4. cut (~ zeroP (A:=A) A0 eqA (n:=n) b); [ intros nZb | idtac ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) c); [ intros nZc | idtac ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) d); [ intros nZd | idtac ]. apply Confluent0 with (nZb := nZc) (nZc := nZb); auto. intros r1 s1 H'5 H'6. elim reduce0_reducestar with (eqA_dec := eqA_dec) (ltM_dec := ltM_dec) (1 := cs) (Q := Q) (p := spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a d nZd p t); auto. intros t0 E; apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := t0). apply Conf_inv1 with (Q := Q) (a := a) (b := c) (c := d) (nZb := nZc) (nZc := nZd) (p := p) (q := r) (r := t); auto. apply Conf_inv1 with (Q := Q) (a := a) (b := d) (c := b) (nZb := nZd) (nZc := nZb) (p := p) (q := t) (r := q); auto. apply canonical_spminusf with (1 := cs); auto. apply canonical_imp_canonical with (a := a); auto. apply canonical_imp_canonical with (a := d); auto. inversion_clear H'; auto. apply canonical_nzeroP with (ltM := ltM) (p := t); auto. apply canonical_nzeroP with (ltM := ltM) (p := r); auto. apply inPolySet_imp_canonical with (L := Q); auto. inversion_clear H'; auto. apply canonical_nzeroP with (ltM := ltM) (p := q); auto. apply inPolySet_imp_canonical with (L := Q); auto. inversion_clear H'0; auto. Qed.