proposition: Theorem confl_top : forall Q : list (poly A0 eqA ltM), SpolyQ Q -> forall (a b c : Term A n) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (p q r : list (Term A n)), canonical A0 eqA ltM (pX a p) -> divP A A0 eqA multA divA n a b -> inPolySet A A0 eqA n ltM (pX b q) Q -> divP A A0 eqA multA divA n a c -> inPolySet A A0 eqA n ltM (pX c r) Q -> (forall q : list (Term A n), canonical A0 eqA ltM q -> ltP (A:=A) (n:=n) ltM q (pX a p) -> ReduStarConfluent Q q) -> reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (pX a p) (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p q) -> reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (pX a p) (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a c nZc p r) -> forall r1 s1 : list (Term A n), reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p q) r1 -> reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a c nZc p r) s1 -> eqP A eqA n r1 s1.
proof: Proof. Proof using plusA os cs. intros Q H' a b c nZb nZc p q r H'0 H'1 H'2 H'3 H'4 H'5 H'6 H'7 r1 s1 H'8 H'9. cut (canonical A0 eqA ltM (pX b q)); [ intros Op0 | idtac ]. cut (canonical A0 eqA ltM (pX c r)); [ intros Op0bis | idtac ]. cut (Confluent Q (pX a p) (pX b q) (pX c r)); auto. 2: apply fconfl_top; auto. 2: inversion_clear H'; auto. 2: apply Reducep0 with (nZb := nZb) (nZc := nZc); auto. 2: apply inPolySet_imp_canonical with (L := Q); auto. 2: apply inPolySet_imp_canonical with (L := Q); auto. intros H'10. apply (Conf_inv1 Q a b c nZb nZc p q r r1 s1); auto. Qed.