proposition: Theorem confl_restar : forall Q : list (poly A0 eqA ltM), SpolyQ Q -> forall p : poly A0 eqA ltM, ReduStarConfluent Q (s2p A A0 eqA n ltM p).
proof: Proof. Proof using plusA os cs. intros Q H'. intros p; pattern p in |- *; apply well_founded_ind with (R := sltP (A:=A) (A0:=A0) (eqA:=eqA) (n:=n) (ltM:=ltM)); auto. apply sltp_wf; auto. intros x; elim x; clear x. intros x Op_x Rec; simpl in |- *. apply ReduStarConfluent0; auto. intros r s H'1 H'2. case reducestar_inv with (1 := cs) (3 := H'2); auto; intros H'8; elim H'8; clear H'8. case reducestar_inv with (1 := cs) (3 := H'1); auto; intros H'9; elim H'9; clear H'9. intros H H0 H1 H2; apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := x); auto; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros x0 H H0 H1; elim H; intros H2 H3; absurd (reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q x x0); auto. intros x0 H; elim H; intros H0 H1; clear H. case reducestar_inv with (1 := cs) (3 := H'1); auto; intros H'9; elim H'9; clear H'9. intros H H2; absurd (reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q x x0); auto. intros x1 H; elim H; intros H2 H3; clear H. generalize H3 H0 H'1 Op_x Rec; clear H3 H0 H'1 Rec Op_x; inversion H2. intros H'3 H'4 H'5 Op_x H'6. generalize Op_x H'6 H'5 H'3; clear H'5 H'3 H'6 Op_x. inversion H'4. intros Op_x H'6 H'5 H'3. apply confl_top with (Q := Q) (a := a) (b := b) (c := b0) (nZb := nZb) (nZc := nZb0) (p := p0) (q := q) (r := q0); auto. intros q1 H'9 H'10. generalize (H'6 (mks A A0 eqA n ltM q1 H'9)); simpl in |- *; auto. apply reducetop_sp with (1 := cs); auto. apply reducetop_sp with (1 := cs); auto. apply reducestar_eqp_com with (1 := cs) (p := x1) (q := r); auto. apply canonical_reduce with (1 := cs) (3 := H2); auto. rewrite <- H4; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply reducestar_eqp_com with (1 := cs) (p := x0) (q := s); auto. apply canonical_reduce with (1 := cs) (3 := H'4); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros Op_x H'6 H'5 H'3. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n). apply confl_mix with (Q := Q) (a := a) (b := b) (nZb := nZb) (p := p0) (q := q0) (r := q); auto. intros q1 H'9 H'10. generalize (H'6 (mks A A0 eqA n ltM q1 H'9)); simpl in |- *; auto. apply reducetop_sp with (1 := cs); auto. apply reducestar_eqp_com with (p := pX b0 q0) (q := s) (1 := cs); auto. rewrite H9; auto. rewrite H9. apply canonical_reduce with (1 := cs) (3 := H'4); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply reducestar_eqp_com with (1 := cs) (p := x1) (q := r); auto. apply canonical_reduce with (1 := cs) (3 := H2); auto. rewrite <- H4; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros H'3 H'4 H'5 Op_x H'6. inversion H'4. apply (confl_mix Q a b0 nZb p0 q q0); auto. intros q1 H'9 H'10. generalize (H'6 (mks A A0 eqA n ltM q1 H'9)); simpl in |- *; auto. apply reducetop_sp with (1 := cs); auto. apply reducestar_eqp_com with (1 := cs) (p := pX b q) (q := r); auto. rewrite H4; auto. apply canonical_reduce with (1 := cs) (3 := H2); auto. rewrite <- H3; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply reducestar_eqp_com with (1 := cs) (p := x0) (q := s); auto. apply canonical_reduce with (1 := cs) (3 := H'4); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply confl_under with (Q := Q) (a := a) (p := p0) (r := q) (s := q0); auto. intros q1 H'9 H'10. generalize (H'6 (mks A A0 eqA n ltM q1 H'9)); simpl in |- *; auto. apply reducestar_eqp_com with (1 := cs) (p := pX b q) (q := r); auto. rewrite H4. apply canonical_reduce with (1 := cs) (3 := H2); auto. rewrite <- H3; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply reducestar_eqp_com with (p := pX b0 q0) (q := s) (1 := cs); auto. rewrite H8; auto. rewrite H8; apply canonical_reduce with (1 := cs) (3 := H'4); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.