Library ult_impl
Require Export impl_large.
Lemma Red3_nuevo_Red1_bis_full: (F:(list pol))(g,h:pol)
(Red3 F g h)->(~(equpol g h))->
(Ex [f:pol_full](Red1 F g (inc f))/\(Red3 F (inc f) h)).
Induction 1; Intros.
Elim H4; Auto.
Elim (can_fun h0); Intros; Trivial.
Elim p; Intros.
Clear p.
Split with (exist pol [p:pol](full_pol p) x H5).
Simpl.
Split; Auto.
Apply Red1_ext1 with h0; Auto.
Elim (equpol_dec_full_term f g0); Auto; Intros.
Cut ~(equpol h0 f); Intros.
Elim H7; Auto; Intros.
Elim H10; Intros.
Split with x.
Split; Auto.
Apply Red1_ext2 with f; Auto.
Red; Intros.
Cut (equpol g0 h0); Intros; Auto.
Apply equpol_tran with f; Auto.
Elim H5; Auto; Intros.
Elim H9; Intros.
Clear H9.
Split with x.
Split; Auto.
Apply Red3_tran with f; Auto.
Save.
Definition local_confluente_full :=
[F:(list pol_full)][f:pol_full](g:pol_full)(h:pol_full)
(Red1 (inc_list F) (inc f) (inc g))->
(Red1 (inc_list F) (inc f) (inc h))->
(common_succ_full F g h).
Definition noether_Red1_full :=
[F:(list pol_full)](x:pol_full)(P:pol_full->Prop)
((y:pol_full)((z:pol_full)(Red1 (inc_list F) (inc y) (inc z))->(P z))->(P y))->
(P x).
Lemma noeth_noether2: (F:(list pol_full))(noetheriano ? (inc_Red1 F))->
(noether_Red1_full F).
Unfold noetheriano.
Unfold well_founded.
Unfold noether_Red1_full; Intros.
Elim H with x; Intros.
Apply H0; Intros.
Apply H2.
Unfold simetrico.
Unfold inc_Red1; Trivial.
Save.
Lemma noeth_noether2_inv: (F:(list pol_full))(noether_Red1_full F)->
(noetheriano ? (inc_Red1 F)).
Unfold noether_Red1_full.
Unfold noetheriano.
Unfold well_founded; Intros.
Apply H; Intros.
Apply Acc_intro; Intros.
Apply H0; Intros.
Unfold simetrico in H1.
Unfold inc_Red1 in H1; Trivial.
Save.
Section Newman_pol.
Variable F:(list pol_full).
Hypothesis Hyp1:(noether_Red1_full F).
Hypothesis Hyp2:(x:pol_full)(local_confluente_full F x).
Section Induccion.
Variable x:pol_full.
Hypothesis hyp_ind:((u:pol_full)(Red1 (inc_list F) (inc x) (inc u))->(confluente_full F u)).
Variables y,z:pol_full.
Hypothesis h1:(Red3 (inc_list F) (inc x) (inc y)).
Hypothesis h2:(Red3 (inc_list F) (inc x) (inc z)).
Section Newman_f.
Variable u:pol_full.
Hypothesis t1:(Red1 (inc_list F) (inc x) (inc u)).
Hypothesis t2:(Red3 (inc_list F) (inc u) (inc y)).
Theorem Diagrama: (v:pol_full)(u1:(Red1 (inc_list F) (inc x) (inc v)))
(u2:(Red3 (inc_list F) (inc v) (inc z)))
(common_succ_full F y z).
Intros.
Red in Hyp2.
Cut (common_succ_full F u v); Intros.
Elim H; Intros.
Clear H.
Cut (common_succ_full F y p); Intros.
Elim H; Intros.
Clear H.
Cut (common_succ_full F p0 z); Intros.
Elim H; Intros.
Clear H.
Split with p1; Auto.
Apply Red3_trans with (inc p0); Auto.
Inversion H1; Auto.
Red in hyp_ind.
Apply hyp_ind with v; Auto.
Apply Red3_trans with (inc p); Auto.
Inversion h1; Auto.
Apply hyp_ind with u; Auto.
Apply Hyp2 with x; Auto.
Save.
Theorem caseRed1xy: (common_succ_full F y z).
Elim (equpol_dec_full_term (inc x) (inc z)); Intros.
Split with y.
Apply Red3_eq; Auto.
Inversion h1; Auto.
Apply Red3_ext2 with (inc x); Auto.
Elim Red3_nuevo_Red1_bis_full with (inc_list F) (inc x) (inc z); Intros; Trivial.
Elim H; Intros.
Clear H.
Apply Diagrama with x0; Auto.
Inversion h1; Auto.
Inversion h2; Auto.
Save.
End Newman_f.
Theorem Ind_prueba: (common_succ_full F y z).
Elim (equpol_dec_full_term (inc x) (inc y)); Intros; Auto.
Split with z.
Apply Red3_ext2 with (inc x); Auto.
Apply Red3_eq; Auto.
Inversion h1; Auto.
Elim (Red3_nuevo_Red1_bis_full (inc_list F) (inc x) (inc y)); Intros; Trivial.
Elim H; Intros.
Clear H.
Apply caseRed1xy with x0; Auto.
Save.
End Induccion.
Theorem Newmansi: (x:pol_full)(confluente_full F x).
Intros.
Apply Hyp1; Intros.
Red.
Apply Ind_prueba; Intros.
Apply H; Auto.
Save.
End Newman_pol.
Lemma G3CR_L_impl_G3CR_full: (F:(list pol_full))(full_fam (inc_list F))->
((f,g,h:pol_full)(Red1 (inc_list F) (inc f) (inc g))->
(Red1 (inc_list F) (inc f) (inc h))->
(common_succ_full F g h))->(Groebner3_CR_full F).
Intros.
Red; Split.
Assumption.
Apply Newmansi; Auto.
Apply noeth_noether2; Auto.
Apply buen_ord_red1; Auto.
Save.
Lemma G2_impl_G1_full: (G:(list pol_full))(Groebner2_full G)->
(Groebner1_full G).
Intros.
Cut (f,g,h:pol_full)
(Red1 (inc_list G) (inc f) (inc g))
->(Red1 (inc_list G) (inc f) (inc h))
->(common_succ_full G g h); Intros.
Cut (Groebner3_CR_full G); Intros.
Apply G3_CR_impl_G1_full; Trivial.
Apply G3CR_L_impl_G3CR_full; Trivial.
Red in H.
Elim H; Trivial.
Elim G2_impl_G3_LCR_full with G f g h; Auto; Intros.
Split with p; Trivial.
Save.
Index
This page has been generated by coqdoc