let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T

let p, q be Polynomial of n,L; :: thesis: ( Support q c= Support p implies q <= p,T )
assume A1: Support q c= Support p ; :: thesis: q <= p,T
defpred S1[ Nat] means for f, g being Polynomial of n,L st Support f c= Support g & card () = \$1 holds
f <= g,T;
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for f, g being Polynomial of n,L st Support f c= Support g & card () = k + 1 holds
f <= g,T
set R = RelStr(# (Bags n),T #);
let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card () = k + 1 implies f <= g,T )
assume that
A4: Support f c= Support g and
A5: card () = k + 1 ; :: thesis: f <= g,T
set rf = Red (f,T);
set rg = Red (g,T);
A6: Support f <> {} by A5;
then A7: HT (f,T) in Support f by TERMORD:def 6;
f <> 0_ (n,L) by ;
then A8: f is non-zero by POLYNOM7:def 1;
g <> 0_ (n,L) by ;
then A9: g is non-zero by POLYNOM7:def 1;
now :: thesis: ( ( HT (f,T) = HT (g,T) & f <= g,T ) or ( HT (f,T) <> HT (g,T) & f <= g,T ) )
per cases ( HT (f,T) = HT (g,T) or HT (f,T) <> HT (g,T) ) ;
case A10: HT (f,T) = HT (g,T) ; :: thesis: f <= g,T
A11: Support (Red (f,T)) = () \ {(HT (f,T))} by TERMORD:36;
A12: Support (Red (g,T)) = () \ {(HT (g,T))} by TERMORD:36;
now :: thesis: for u being object st u in Support (Red (f,T)) holds
u in Support (Red (g,T))
let u be object ; :: thesis: ( u in Support (Red (f,T)) implies u in Support (Red (g,T)) )
assume u in Support (Red (f,T)) ; :: thesis: u in Support (Red (g,T))
then ( u in Support f & not u in {(HT (f,T))} ) by ;
hence u in Support (Red (g,T)) by ; :: thesis: verum
end;
then A13: Support (Red (f,T)) c= Support (Red (g,T)) ;
for u being object st u in {(HT (f,T))} holds
u in Support f by ;
then A14: {(HT (f,T))} c= Support f ;
A15: ( Support (f,T) <> {} & Support (g,T) <> {} ) by ;
A16: Support ((Red (f,T)),T) = Support (Red (f,T)) by POLYRED:def 4;
HT (f,T) in {(HT (f,T))} by TARSKI:def 1;
then A17: not HT (f,T) in Support (Red (f,T)) by ;
A18: PosetMax (Support (f,T)) = HT (g,T) by
.= PosetMax (Support (g,T)) by ;
A19: Support ((Red (g,T)),T) = Support (Red (g,T)) by POLYRED:def 4;
A20: Support (g,T) = Support g by POLYRED:def 4;
then A21: (Support (g,T)) \ {(PosetMax (Support (g,T)))} = Support ((Red (g,T)),T) by ;
(Support (Red (f,T))) \/ {(HT (f,T))} = () \/ {(HT (f,T))} by
.= Support f by ;
then (card (Support (Red (f,T)))) + 1 = k + 1 by ;
then Red (f,T) <= Red (g,T),T by ;
then [(Support (Red (f,T))),(Support (Red (g,T)))] in FinOrd RelStr(# (Bags n),T #) by POLYRED:def 2;
then A22: [(Support ((Red (f,T)),T)),(Support ((Red (g,T)),T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by ;
A23: Support (f,T) = Support f by POLYRED:def 4;
then (Support (f,T)) \ {(PosetMax (Support (f,T)))} = Support ((Red (f,T)),T) by ;
then [(Support (f,T)),(Support (g,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by ;
then [(),()] in FinOrd RelStr(# (Bags n),T #) by ;
hence f <= g,T by POLYRED:def 2; :: thesis: verum
end;
case A24: HT (f,T) <> HT (g,T) ; :: thesis: f <= g,T
now :: thesis: not HT (g,T) < HT (f,T),T
assume HT (g,T) < HT (f,T),T ; :: thesis: contradiction
then not HT (f,T) <= HT (g,T),T by TERMORD:5;
hence contradiction by A4, A7, TERMORD:def 6; :: thesis: verum
end;
then HT (f,T) <= HT (g,T),T by TERMORD:5;
then HT (f,T) < HT (g,T),T by ;
then f < g,T by POLYRED:32;
hence f <= g,T by POLYRED:def 3; :: thesis: verum
end;
end;
end;
hence f <= g,T ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A25: ex k being Element of NAT st card () = k ;
A26: S1[ 0 ]
proof
let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card () = 0 implies f <= g,T )
assume that
Support f c= Support g and
A27: card () = 0 ; :: thesis: f <= g,T
Support f = {} by A27;
then f = 0_ (n,L) by POLYNOM7:1;
hence f <= g,T by POLYRED:30; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A26, A2);
hence q <= p,T by ; :: thesis: verum