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 S_{1}[ Nat] means for f, g being Polynomial of n,L st Support f c= Support g & card (Support f) = $1 holds

f <= g,T;

A26: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A26, A2);

hence q <= p,T by A1, A25; :: thesis: verum

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 S

f <= g,T;

A2: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A25:
ex k being Element of NAT st card (Support q) = k
;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for f, g being Polynomial of n,L st Support f c= Support g & card (Support f) = k + 1 holds

f <= g,T

hence
Sf <= g,T

set R = RelStr(# (Bags n),T #);

let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = k + 1 implies f <= g,T )

assume that

A4: Support f c= Support g and

A5: card (Support f) = 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 A6, POLYNOM7:1;

then A8: f is non-zero by POLYNOM7:def 1;

g <> 0_ (n,L) by A4, A7, POLYNOM7:1;

then A9: g is non-zero by POLYNOM7:def 1;

end;let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = k + 1 implies f <= g,T )

assume that

A4: Support f c= Support g and

A5: card (Support f) = 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 A6, POLYNOM7:1;

then A8: f is non-zero by POLYNOM7:def 1;

g <> 0_ (n,L) by A4, A7, POLYNOM7:1;

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 ) )end;

hence
f <= g,T
; :: thesis: verumper cases
( HT (f,T) = HT (g,T) or HT (f,T) <> HT (g,T) )
;

end;

case A10:
HT (f,T) = HT (g,T)
; :: thesis: f <= g,T

A11:
Support (Red (f,T)) = (Support f) \ {(HT (f,T))}
by TERMORD:36;

A12: Support (Red (g,T)) = (Support g) \ {(HT (g,T))} by TERMORD:36;

for u being object st u in {(HT (f,T))} holds

u in Support f by A7, TARSKI:def 1;

then A14: {(HT (f,T))} c= Support f ;

A15: ( Support (f,T) <> {} & Support (g,T) <> {} ) by A4, A7, POLYRED:def 4;

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 A11, XBOOLE_0:def 5;

A18: PosetMax (Support (f,T)) = HT (g,T) by A8, A10, POLYRED:24

.= PosetMax (Support (g,T)) by A9, POLYRED:24 ;

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 A9, A12, A19, POLYRED:24;

(Support (Red (f,T))) \/ {(HT (f,T))} = (Support f) \/ {(HT (f,T))} by A11, XBOOLE_1:39

.= Support f by A14, XBOOLE_1:12 ;

then (card (Support (Red (f,T)))) + 1 = k + 1 by A5, A17, CARD_2:41;

then Red (f,T) <= Red (g,T),T by A3, A13;

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 A16, A19, BAGORDER:def 15;

A23: Support (f,T) = Support f by POLYRED:def 4;

then (Support (f,T)) \ {(PosetMax (Support (f,T)))} = Support ((Red (f,T)),T) by A8, A11, A16, POLYRED:24;

then [(Support (f,T)),(Support (g,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A22, A15, A18, A21, BAGORDER:35;

then [(Support f),(Support g)] in FinOrd RelStr(# (Bags n),T #) by A23, A20, BAGORDER:def 15;

hence f <= g,T by POLYRED:def 2; :: thesis: verum

end;A12: Support (Red (g,T)) = (Support g) \ {(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))

then A13:
Support (Red (f,T)) c= Support (Red (g,T))
;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 A11, XBOOLE_0:def 5;

hence u in Support (Red (g,T)) by A4, A10, A12, XBOOLE_0:def 5; :: thesis: verum

end;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 A11, XBOOLE_0:def 5;

hence u in Support (Red (g,T)) by A4, A10, A12, XBOOLE_0:def 5; :: thesis: verum

for u being object st u in {(HT (f,T))} holds

u in Support f by A7, TARSKI:def 1;

then A14: {(HT (f,T))} c= Support f ;

A15: ( Support (f,T) <> {} & Support (g,T) <> {} ) by A4, A7, POLYRED:def 4;

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 A11, XBOOLE_0:def 5;

A18: PosetMax (Support (f,T)) = HT (g,T) by A8, A10, POLYRED:24

.= PosetMax (Support (g,T)) by A9, POLYRED:24 ;

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 A9, A12, A19, POLYRED:24;

(Support (Red (f,T))) \/ {(HT (f,T))} = (Support f) \/ {(HT (f,T))} by A11, XBOOLE_1:39

.= Support f by A14, XBOOLE_1:12 ;

then (card (Support (Red (f,T)))) + 1 = k + 1 by A5, A17, CARD_2:41;

then Red (f,T) <= Red (g,T),T by A3, A13;

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 A16, A19, BAGORDER:def 15;

A23: Support (f,T) = Support f by POLYRED:def 4;

then (Support (f,T)) \ {(PosetMax (Support (f,T)))} = Support ((Red (f,T)),T) by A8, A11, A16, POLYRED:24;

then [(Support (f,T)),(Support (g,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A22, A15, A18, A21, BAGORDER:35;

then [(Support f),(Support g)] in FinOrd RelStr(# (Bags n),T #) by A23, A20, BAGORDER:def 15;

hence f <= g,T by POLYRED:def 2; :: thesis: verum

case A24:
HT (f,T) <> HT (g,T)
; :: thesis: f <= g,T

then HT (f,T) < HT (g,T),T by A24, TERMORD:def 3;

then f < g,T by POLYRED:32;

hence f <= g,T by POLYRED:def 3; :: thesis: verum

end;

now :: thesis: not HT (g,T) < HT (f,T),T

then
HT (f,T) <= HT (g,T),T
by TERMORD:5;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 not HT (f,T) <= HT (g,T),T by TERMORD:5;

hence contradiction by A4, A7, TERMORD:def 6; :: thesis: verum

then HT (f,T) < HT (g,T),T by A24, TERMORD:def 3;

then f < g,T by POLYRED:32;

hence f <= g,T by POLYRED:def 3; :: thesis: verum

A26: S

proof

for k being Nat holds S
let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = 0 implies f <= g,T )

assume that

Support f c= Support g and

A27: card (Support f) = 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;assume that

Support f c= Support g and

A27: card (Support f) = 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

hence q <= p,T by A1, A25; :: thesis: verum