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 = 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 A2;

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

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

end;

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

then A6: HT p,T <> HT q,T by TERMORD:def 3;
A7: HT p,T <= HT q,T,T by A5, TERMORD:def 3;
then A8: [(HT p,T),(HT q,T)] in T by TERMORD:def 2;

now

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

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

then A10: p = 0_ n,L by POLYNOM7:1;

A11: now

assume Support p = Support q ; :: thesis: contradiction
then HT p,T = HT q,T by A9, A10, POLYNOM7:1;
hence contradiction by A5, TERMORD:def 3; :: thesis: verum

end;

p <= q,T by A10, Lm12;
hence p < q,T by A11, Def3; :: thesis: verum

end;

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

A13: 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 A7, A6, TERMORD:7; :: thesis: verum

end;

A14: now

assume A15: Support p = Support q ; :: thesis: contradiction
HT q,T in Support q by A13, TERMORD:def 6;
then A16: HT q,T <= HT p,T,T by A15, TERMORD:def 6;
HT p,T in Support p by A12, TERMORD:def 6;
then HT p,T <= HT q,T,T by A15, TERMORD:def 6;
hence contradiction by A6, A16, TERMORD:7; :: thesis: verum

end;

p <> 0_ n,L by A12, POLYNOM7:1;
then p is non-zero by POLYNOM7:def 2;
then A17: PosetMax (Support p,T) = HT p,T by Th24;
q <> 0_ n,L by A13, POLYNOM7:1;
then q is non-zero by POLYNOM7:def 2;
then PosetMax (Support q,T) = HT q,T by Th24;
then [(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A6, A8, A12, A13, A17, 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 A14, Def3; :: thesis: verum

end;

end;

end;

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

end;

case A18: ( 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 by Def3;
then A19: [(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 A20: 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 A18, A20, Lm14;
hence contradiction by A18, Def3; :: thesis: verum

end;

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

now

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

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

then A22: 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 A18, A22, Lm14;
hence contradiction by A18, Def3; :: thesis: verum

end;

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

A24: now

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

end;

set rp = Red p,T;
set rq = Red q,T;
p <> 0_ n,L by A21, POLYNOM7:1;
then A25: p is non-zero by POLYNOM7:def 2;
q <> 0_ n,L by A23, POLYNOM7:1;
then A26: q is non-zero by POLYNOM7:def 2;
then A27: PosetMax (Support q,T) = HT q,T by Th24;
A28: Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A26, Th24 ;
Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A25, Th24 ;
then A29: [((Support p,T) \ {(PosetMax (Support p,T))}),((Support q,T) \ {(PosetMax (Support q,T))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A19, A28, BAGORDER:def 17;
PosetMax (Support p,T) = HT p,T by A25, Th24;
then [(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A18, A21, A23, A27, A29, 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 A24, 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;

now

assume A30: 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 p <= q,T by Def3;
then [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) by Def2;
then A31: [(Support p),(Support q)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 17;
A32: Support p <> Support q by A30, Def3;

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 A31, 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 A32, POLYNOM7:1; :: thesis: verum

end;

case A33: ( 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 q <> 0_ n,L by POLYNOM7:1;
then q is non-zero by POLYNOM7:def 2;
then A34: PosetMax (Support q,T) = HT q,T by Th24;
p <> 0_ n,L by A33, POLYNOM7:1;
then p is non-zero by POLYNOM7:def 2;
then A35: PosetMax (Support p,T) = HT p,T by Th24;
then HT p,T <= HT q,T,T by A33, A34, TERMORD:def 2;
hence HT p,T < HT q,T,T by A33, A35, A34, TERMORD:def 3; :: thesis: verum

end;

case A36: ( 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 )

set rp = Red p,T;
set rq = Red q,T;
p <> 0_ n,L by A36, POLYNOM7:1;
then A37: p is non-zero by POLYNOM7:def 2;
then A38: PosetMax (Support p,T) = HT p,T by Th24;
q <> 0_ n,L by A36, POLYNOM7:1;
then A39: q is non-zero by POLYNOM7:def 2;
then A40: PosetMax (Support q,T) = HT q,T by Th24;

A41: now

HT q,T in Support q by A36, TERMORD:def 6;
then for u being set st u in {(HT q,T)} holds
u in Support q by TARSKI:def 1;
then A42: {(HT q,T)} c= Support q by TARSKI:def 3;
Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36;
then A43: (Support (Red q,T)) \/ {(HT q,T)} = (Support q) \/ {(HT q,T)} by XBOOLE_1:39
.= Support q by A42, XBOOLE_1:12 ;
HT p,T in Support p by A36, TERMORD:def 6;
then for u being set st u in {(HT p,T)} holds
u in Support p by TARSKI:def 1;
then A44: {(HT p,T)} c= Support p by TARSKI:def 3;
Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36;
then A45: (Support (Red p,T)) \/ {(HT p,T)} = (Support p) \/ {(HT p,T)} by XBOOLE_1:39
.= Support p by A44, XBOOLE_1:12 ;
assume Support (Red p,T) = Support (Red q,T) ; :: thesis: contradiction
hence contradiction by A30, A36, A38, A40, A45, A43, Def3; :: thesis: verum

end;

A46: Support (Red p,T),T = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A37, Th24 ;
Support (Red q,T),T = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A39, Th24 ;
then [(Support (Red p,T),T),(Support (Red q,T),T)] in FinOrd RelStr(# (Bags n),T #) by A36, A46, BAGORDER:def 17;
then Red p,T <= Red q,T,T by Def2;
hence ( HT p,T = HT q,T & Red p,T < Red q,T,T ) by A36, A39, A38, A41, Def3, Th24; :: 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;

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