let n be Ordinal; 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; 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 ; 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; ( 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 ( ( ( 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 ) ) implies p < q,T )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 ) )
;
p < q,Tnow ( ( p = 0_ (n,L) & q <> 0_ (n,L) & p < q,T ) or ( HT (p,T) < HT (q,T),T & p < q,T ) or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T & p < q,T ) )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 A5:
HT (
p,
T)
< HT (
q,
T),
T
;
p < q,Tthen 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 ( ( Support p = {} & p < q,T ) or ( Support p <> {} & p < q,T ) )per cases
( Support p = {} or Support p <> {} )
;
case A12:
Support p <> {}
;
p < q,TA14:
now not Support p = Support qassume A15:
Support p = Support q
;
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;
verum end;
p <> 0_ (
n,
L)
by A12, POLYNOM7:1;
then
p is
non-zero
;
then A17:
PosetMax (Support (p,T)) = HT (
p,
T)
by Th24;
q <> 0_ (
n,
L)
by A13, POLYNOM7:1;
then
q is
non-zero
;
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:35;
then
[(Support p),(Support q)] in FinOrd RelStr(#
(Bags n),
T #)
by BAGORDER:def 15;
then
p <= q,
T
;
hence
p < q,
T
by A14;
verum end; end; end; hence
p < q,
T
;
verum end; case A18:
(
HT (
p,
T)
= HT (
q,
T) &
Red (
p,
T)
< Red (
q,
T),
T )
;
p < q,Tthen
Red (
p,
T)
<= Red (
q,
T),
T
;
then A19:
[(Support (Red (p,T))),(Support (Red (q,T)))] in FinOrd RelStr(#
(Bags n),
T #)
;
now ( ( Support p = {} & contradiction ) or ( Support p <> {} & p < q,T ) )per cases
( Support p = {} or Support p <> {} )
;
case A21:
Support p <> {}
;
p < q,Tnow ( ( Support q = {} & contradiction ) or ( Support q <> {} & p < q,T ) )per cases
( Support q = {} or Support q <> {} )
;
case A23:
Support q <> {}
;
p < q,Tset rp =
Red (
p,
T);
set rq =
Red (
q,
T);
p <> 0_ (
n,
L)
by A21, POLYNOM7:1;
then A25:
p is
non-zero
;
q <> 0_ (
n,
L)
by A23, POLYNOM7:1;
then A26:
q is
non-zero
;
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 15;
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:35;
then
[(Support p),(Support q)] in FinOrd RelStr(#
(Bags n),
T #)
by BAGORDER:def 15;
then
p <= q,
T
;
hence
p < q,
T
by A24;
verum end; end; end; hence
p < q,
T
;
verum end; end; end; hence
p < q,
T
;
verum end; end; end; hence
p < q,
T
;
verum end;
now ( not p < q,T or ( 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 ) )assume A30:
p < q,
T
;
( ( 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
;
then
[(Support p),(Support q)] in FinOrd RelStr(#
(Bags n),
T #)
;
then A31:
[(Support p),(Support q)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #)))
by BAGORDER:def 15;
A32:
Support p <> Support q
by A30;
now ( ( Support (p,T) = {} & p = 0_ (n,L) & q <> 0_ (n,L) ) 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 #) & HT (p,T) < HT (q,T),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 #))) & HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) )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:35;
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 #) )
;
HT (p,T) < HT (q,T),Tthen
q <> 0_ (
n,
L)
by POLYNOM7:1;
then
q is
non-zero
;
then A34:
PosetMax (Support (q,T)) = HT (
q,
T)
by Th24;
p <> 0_ (
n,
L)
by A33, POLYNOM7:1;
then
p is
non-zero
;
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;
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 #))) )
;
( 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
;
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
;
then A40:
PosetMax (Support (q,T)) = HT (
q,
T)
by Th24;
A41:
now not Support (Red (p,T)) = Support (Red (q,T))
HT (
q,
T)
in Support q
by A36, TERMORD:def 6;
then
for
u being
object 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
object 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))
;
contradictionhence
contradiction
by A30, A36, A38, A40, A45, A43;
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 15;
then
Red (
p,
T)
<= Red (
q,
T),
T
;
hence
(
HT (
p,
T)
= HT (
q,
T) &
Red (
p,
T)
< Red (
q,
T),
T )
by A36, A39, A38, A41, Th24;
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 ) )
;
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; verum