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