proposition: Theorem fconfl_top : forall (Q : list (poly A0 eqA ltM)) (q r : list (Term A n)), Spoly_1 Q q r -> forall p : list (Term A n), Reducep Q p q r -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> (forall q0 : list (Term A n), canonical A0 eqA ltM q0 -> ltP (A:=A) (n:=n) ltM q0 p -> ReduStarConfluent Q q0) -> Confluent Q p q r.
proof: Proof. Proof using plusA os cs. intros Q q r Spoly1; elim Spoly1; clear Spoly1 q r. intros q r Cq Cr red0 p H'1; (generalize Cq Cr red0; inversion_clear H'1; clear red0 Cq Cr). intros Cq Cr H' H'0 H'1 H'2 H'3. apply Confluent0 with (nZb := nZb) (nZc := nZc); auto. intros r1 s1 H'5 H'6. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n). apply (confl_top_simpl Q a c b nZc nZb p0 r0 q0 Cq Cr); auto. intros b c d q r H' H'0 t H'1 H'2 H'3 H'4 H'5 H'6 p H'7 H'8 H'9 H'10 H'11. generalize H'11 H'8; clear H'11 H'8; inversion_clear H'7. intros H'8 H'11. cut (divP A A0 eqA multA divA n a d); [ intros div0 | idtac ]. 2: apply (divP_trans _ _ _ _ _ _ _ _ _ cs n) with (y := ppc (A:=A) A1 (n:=n) c b); auto. 2: case ppc_is_ppcm with (1 := cs) (a := c) (b := b); auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) d); [ intros nZd | inversion div0 ]; auto. cut (Reducep Q (pX a p0) (pX d t) (pX b q)); [ intros Red0 | idtac ]. 2: apply Reducep0 with (nZb := nZd) (nZc := nZc); auto. cut (Reducep Q (pX a p0) (pX c r) (pX d t)); [ intros Red1 | idtac ]. 2: apply Reducep0 with (nZb := nZb) (nZc := nZd); auto. apply Conf_trans with (d := d) (t := t); auto. apply H'2; auto. apply inPolySet_imp_canonical with (L := Q); auto. apply H'4; auto. apply inPolySet_imp_canonical with (L := Q); auto. apply inPolySet_imp_canonical with (L := Q); auto. apply reducetop_sp with (1 := cs); auto. apply reducetop_sp with (1 := cs); auto. Qed.