let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) )
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) )
let p, q be Polynomial of n,L; :: thesis: ( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) )
set R = RelStr(# (Bags n),T #);
set sp = Support p;
set sq = Support q;
set x = Support p,T;
set y = Support q,T;

A1: now

assume A2: p < q,T ; :: thesis: ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) )
then A3: ( p <= q,T & Support p <> Support q ) by Def3;
then [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) by Def2;
then A4: [(Support p),(Support q)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 17;

now

per cases ( Support p,T = {} or ( Support p,T <> {} & Support q,T <> {} & PosetMax (Support p,T) <> PosetMax (Support q,T) & [(PosetMax (Support p,T)),(PosetMax (Support q,T))] in the InternalRel of RelStr(# (Bags n),T #) ) or ( Support p,T <> {} & Support q,T <> {} & PosetMax (Support p,T) = PosetMax (Support q,T) & [((Support p,T) \ {(PosetMax (Support p,T))}),((Support q,T) \ {(PosetMax (Support q,T))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) ) ) by A4, BAGORDER:36;

case Support p,T = {} ; :: thesis: ( p = 0_ n,L & q <> 0_ n,L )

hence ( p = 0_ n,L & q <> 0_ n,L ) by A3, POLYNOM7:1; :: thesis: verum

end;

case A5: ( Support p,T <> {} & Support q,T <> {} & PosetMax (Support p,T) <> PosetMax (Support q,T) & [(PosetMax (Support p,T)),(PosetMax (Support q,T))] in the InternalRel of RelStr(# (Bags n),T #) ) ; :: thesis: HT p,T < HT q,T,T

then ( p <> 0_ n,L & q <> 0_ n,L ) by POLYNOM7:1;
then ( p is non-zero & q is non-zero ) by POLYNOM7:def 2;
then A6: ( PosetMax (Support p,T) = HT p,T & PosetMax (Support q,T) = HT q,T ) by Th24;
then HT p,T <= HT q,T,T by A5, TERMORD:def 2;
hence HT p,T < HT q,T,T by A5, A6, TERMORD:def 3; :: thesis: verum

end;

case A7: ( Support p,T <> {} & Support q,T <> {} & PosetMax (Support p,T) = PosetMax (Support q,T) & [((Support p,T) \ {(PosetMax (Support p,T))}),((Support q,T) \ {(PosetMax (Support q,T))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) ) ; :: thesis: ( HT p,T = HT q,T & Red p,T < Red q,T,T )

then ( p <> 0_ n,L & q <> 0_ n,L ) by POLYNOM7:1;
then A8: ( p is non-zero & q is non-zero ) by POLYNOM7:def 2;
then A9: ( PosetMax (Support p,T) = HT p,T & PosetMax (Support q,T) = HT q,T ) by Th24;
set rp = Red p,T;
set rq = Red q,T;
A10: Support (Red p,T),T = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A8, Th24 ;
Support (Red q,T),T = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A8, Th24 ;
then [(Support (Red p,T),T),(Support (Red q,T),T)] in FinOrd RelStr(# (Bags n),T #) by A7, A10, BAGORDER:def 17;
then A11: Red p,T <= Red q,T,T by Def2;

now

assume A12: Support (Red p,T) = Support (Red q,T) ; :: thesis: contradiction
A13: ( HT p,T in Support p & HT q,T in Support q ) by A7, TERMORD:def 6;
then for u being set st u in {(HT p,T)} holds
u in Support p by TARSKI:def 1;
then A14: {(HT p,T)} c= Support p by TARSKI:def 3;
Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36;
then A15: (Support (Red p,T)) \/ {(HT p,T)} = (Support p) \/ {(HT p,T)} by XBOOLE_1:39
.= Support p by A14, XBOOLE_1:12 ;
for u being set st u in {(HT q,T)} holds
u in Support q by A13, TARSKI:def 1;
then A16: {(HT q,T)} c= Support q by TARSKI:def 3;
Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36;
then (Support (Red q,T)) \/ {(HT q,T)} = (Support q) \/ {(HT q,T)} by XBOOLE_1:39
.= Support q by A16, XBOOLE_1:12 ;
hence contradiction by A2, A7, A9, A12, A15, Def3; :: thesis: verum

end;

hence ( HT p,T = HT q,T & Red p,T < Red q,T,T ) by A7, A9, A11, Def3; :: thesis: verum

end;

end;

end;

hence ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) ; :: thesis: verum

end;

now

assume A17: ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) ; :: thesis: p < q,T

now

per cases ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) by A17;

case A18: ( p = 0_ n,L & q <> 0_ n,L ) ; :: thesis: p < q,T

then A19: p <= q,T by Lm12;
Support p = {} by A18, POLYNOM7:1;
then Support p <> Support q by A18, POLYNOM7:1;
hence p < q,T by A19, Def3; :: thesis: verum

end;

case A20: HT p,T < HT q,T,T ; :: thesis: p < q,T

then A21: ( HT p,T <= HT q,T,T & HT p,T <> HT q,T ) by TERMORD:def 3;
then A22: [(HT p,T),(HT q,T)] in T by TERMORD:def 2;

now

per cases ( Support p = {} or Support p <> {} ) ;

case A23: Support p = {} ; :: thesis: p < q,T

then A24: p = 0_ n,L by POLYNOM7:1;
then A25: p <= q,T by Lm12;

now

assume Support p = Support q ; :: thesis: contradiction
then HT p,T = HT q,T by A23, A24, POLYNOM7:1;
hence contradiction by A20, TERMORD:def 3; :: thesis: verum

end;

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

end;

case A26: Support p <> {} ; :: thesis: p < q,T

A27: now

assume Support q = {} ; :: thesis: contradiction
then HT q,T = EmptyBag n by TERMORD:def 6;
then [(HT q,T),(HT p,T)] in T by BAGORDER:def 7;
then HT q,T <= HT p,T,T by TERMORD:def 2;
hence contradiction by A21, TERMORD:7; :: thesis: verum

end;

then ( p <> 0_ n,L & q <> 0_ n,L ) by A26, POLYNOM7:1;
then ( p is non-zero & q is non-zero ) by POLYNOM7:def 2;
then A28: ( PosetMax (Support p,T) = HT p,T & PosetMax (Support q,T) = HT q,T ) by Th24;

A29: now

assume A30: Support p = Support q ; :: thesis: contradiction
A31: ( HT p,T in Support p & ( for b being bag of st b in Support p holds
b <= HT p,T,T ) ) by A26, TERMORD:def 6;
( HT q,T in Support q & ( for b being bag of st b in Support q holds
b <= HT q,T,T ) ) by A27, TERMORD:def 6;
then ( HT p,T <= HT q,T,T & HT q,T <= HT p,T,T ) by A30, A31;
hence contradiction by A21, TERMORD:7; :: thesis: verum

end;

[(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A21, A22, A26, A27, A28, BAGORDER:36;
then [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 17;
then p <= q,T by Def2;
hence p < q,T by A29, Def3; :: thesis: verum

end;

end;

end;

hence p < q,T ; :: thesis: verum

end;

case A32: ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ; :: thesis: p < q,T

then ( Red p,T <= Red q,T,T & Support (Red p,T) <> Support (Red q,T) ) by Def3;
then A33: [(Support (Red p,T)),(Support (Red q,T))] in FinOrd RelStr(# (Bags n),T #) by Def2;

now

per cases ( Support p = {} or Support p <> {} ) ;

case Support p = {} ; :: thesis: contradiction

then A34: HT p,T = EmptyBag n by TERMORD:def 6;
then Red p,T = 0_ n,L by Lm14;
then Support (Red q,T) = Support (Red p,T) by A32, A34, Lm14;
hence contradiction by A32, Def3; :: thesis: verum

end;

case A35: Support p <> {} ; :: thesis: p < q,T

now

per cases ( Support q = {} or Support q <> {} ) ;

case Support q = {} ; :: thesis: contradiction

then A36: HT q,T = EmptyBag n by TERMORD:def 6;
then Red q,T = 0_ n,L by Lm14;
then Support (Red p,T) = Support (Red q,T) by A32, A36, Lm14;
hence contradiction by A32, Def3; :: thesis: verum

end;

case A37: Support q <> {} ; :: thesis: p < q,T

then ( p <> 0_ n,L & q <> 0_ n,L ) by A35, POLYNOM7:1;
then A38: ( p is non-zero & q is non-zero ) by POLYNOM7:def 2;
then A39: ( PosetMax (Support p,T) = HT p,T & PosetMax (Support q,T) = HT q,T ) by Th24;

A40: now

assume Support p = Support q ; :: thesis: contradiction
then Support (Red p,T) = (Support q) \ {(HT q,T)} by A32, TERMORD:36
.= Support (Red q,T) by TERMORD:36 ;
hence contradiction by A32, Def3; :: thesis: verum

end;

set rp = Red p,T;
set rq = Red q,T;
A41: Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A38, Th24 ;
Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A38, Th24 ;
then [((Support p,T) \ {(PosetMax (Support p,T))}),((Support q,T) \ {(PosetMax (Support q,T))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A33, A41, BAGORDER:def 17;
then [(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A32, A35, A37, A39, BAGORDER:36;
then [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 17;
then p <= q,T by Def2;
hence p < q,T by A40, Def3; :: thesis: verum

end;

end;

end;

hence p < q,T ; :: thesis: verum

end;

end;

end;

hence p < q,T ; :: thesis: verum

end;

end;

end;

hence p < q,T ; :: thesis: verum

end;

hence ( p < q,T iff ( ( p = 0_ n,L & q <> 0_ n,L ) or HT p,T < HT q,T,T or ( HT p,T = HT q,T & Red p,T < Red q,T,T ) ) ) by A1; :: thesis: verum