let n be Ordinal; for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
let O be connected admissible TermOrder of n; for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let L be non empty right_zeroed addLoopStr ; for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let p, q be Polynomial of n,L; HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
per cases
( HT ((p + q),O) in Support (p + q) or not HT ((p + q),O) in Support (p + q) )
;
suppose A1:
HT (
(p + q),
O)
in Support (p + q)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),OA2:
Support (p + q) c= (Support p) \/ (Support q)
by POLYNOM1:20;
now ( ( HT ((p + q),O) in Support p & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( HT ((p + q),O) in Support q & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )per cases
( HT ((p + q),O) in Support p or HT ((p + q),O) in Support q )
by A1, A2, XBOOLE_0:def 3;
case A3:
HT (
(p + q),
O)
in Support p
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Othen A4:
HT (
(p + q),
O)
<= HT (
p,
O),
O
by Def6;
now ( ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )per cases
( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) )
by Th12;
case
max (
(HT (p,O)),
(HT (q,O)),
O)
= HT (
p,
O)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Oend; case A5:
max (
(HT (p,O)),
(HT (q,O)),
O)
= HT (
q,
O)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Othen
HT (
p,
O)
<= HT (
q,
O),
O
by Th14;
hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
by A4, A5, Th8;
verum end; end; end; hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
;
verum end; case A6:
HT (
(p + q),
O)
in Support q
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Othen A7:
HT (
(p + q),
O)
<= HT (
q,
O),
O
by Def6;
now ( ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )per cases
( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) )
by Th12;
case
max (
(HT (p,O)),
(HT (q,O)),
O)
= HT (
q,
O)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Oend; case A8:
max (
(HT (p,O)),
(HT (q,O)),
O)
= HT (
p,
O)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Othen
HT (
q,
O)
<= HT (
p,
O),
O
by Th14;
hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
by A7, A8, Th8;
verum end; end; end; hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
;
verum end; end; end; hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
;
verum end; suppose
not
HT (
(p + q),
O)
in Support (p + q)
;
HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),Othen
HT (
(p + q),
O)
= EmptyBag n
by Def6;
then
[(HT ((p + q),O)),(max ((HT (p,O)),(HT (q,O)),O))] in O
by BAGORDER:def 5;
hence
HT (
(p + q),
O)
<= max (
(HT (p,O)),
(HT (q,O)),
O),
O
;
verum end; end;