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 being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let i be Element of NAT ; :: thesis: ( i < card (Support p) implies Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) )

set l = Low (p,T,i);

set l1 = Low (p,T,(i + 1));

set r = Red ((Low (p,T,i)),T);

assume A1: i < card (Support p) ; :: thesis: Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

then A2: Support (Low (p,T,i)) c= Support p by Th26;

Support (Low (p,T,i)) = Lower_Support (p,T,i) by A1, Lm3;

then A3: card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;

A4: Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) by A1, Th41;

A5: i + 1 <= card (Support p) by A1, NAT_1:13;

then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;

then A6: card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (i + 1) by A5, Th24;

A7: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by A5, Lm3;

A13: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} by A1, Th42;

then Support (Low (p,T,i)) = (Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))} by A1, Th41, XBOOLE_1:45;

then A14: Support (Red ((Low (p,T,i)),T)) = ((Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))}) \ {(HT ((Low (p,T,i)),T))} by TERMORD:36

.= (Support (Low (p,T,(i + 1)))) \ {(HT ((Low (p,T,i)),T))} by XBOOLE_1:40

.= Support (Low (p,T,(i + 1))) by A12, XBOOLE_1:83 ;

.= dom (Red ((Low (p,T,i)),T)) by FUNCT_2:def 1 ;

hence Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) by A15, FUNCT_1:2; :: thesis: verum

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card (Support p) holds

Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

let i be Element of NAT ; :: thesis: ( i < card (Support p) implies Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) )

set l = Low (p,T,i);

set l1 = Low (p,T,(i + 1));

set r = Red ((Low (p,T,i)),T);

assume A1: i < card (Support p) ; :: thesis: Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)

then A2: Support (Low (p,T,i)) c= Support p by Th26;

Support (Low (p,T,i)) = Lower_Support (p,T,i) by A1, Lm3;

then A3: card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;

A4: Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) by A1, Th41;

A5: i + 1 <= card (Support p) by A1, NAT_1:13;

then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;

then A6: card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (i + 1) by A5, Th24;

A7: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by A5, Lm3;

now :: thesis: not {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) <> {}

then A12:
Support (Low (p,T,(i + 1))) misses {(HT ((Low (p,T,i)),T))}
by XBOOLE_0:def 7;set u = the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1))));

assume A8: {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) <> {} ; :: thesis: contradiction

then the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in {(HT ((Low (p,T,i)),T))} by XBOOLE_0:def 4;

then A9: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) = HT ((Low (p,T,i)),T) by TARSKI:def 1;

A10: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in Support (Low (p,T,(i + 1))) by A8, XBOOLE_0:def 4;

then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A3, A6, NAT_1:43;

then - i <= - (i + 1) by XREAL_1:6;

then i + 1 <= i by XREAL_1:24;

then (i + 1) - i <= i - i by XREAL_1:9;

then 1 <= 0 ;

hence contradiction ; :: thesis: verum

end;assume A8: {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) <> {} ; :: thesis: contradiction

then the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in {(HT ((Low (p,T,i)),T))} by XBOOLE_0:def 4;

then A9: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) = HT ((Low (p,T,i)),T) by TARSKI:def 1;

A10: the Element of {(HT ((Low (p,T,i)),T))} /\ (Support (Low (p,T,(i + 1)))) in Support (Low (p,T,(i + 1))) by A8, XBOOLE_0:def 4;

now :: thesis: for u9 being object st u9 in Support (Low (p,T,i)) holds

u9 in Support (Low (p,T,(i + 1)))

then
Support (Low (p,T,i)) c= Support (Low (p,T,(i + 1)))
;u9 in Support (Low (p,T,(i + 1)))

let u9 be object ; :: thesis: ( u9 in Support (Low (p,T,i)) implies u9 in Support (Low (p,T,(i + 1))) )

assume A11: u9 in Support (Low (p,T,i)) ; :: thesis: u9 in Support (Low (p,T,(i + 1)))

then reconsider u = u9 as Element of Bags n ;

u <= HT ((Low (p,T,i)),T),T by A11, TERMORD:def 6;

hence u9 in Support (Low (p,T,(i + 1))) by A5, A2, A7, A10, A9, A11, Th24; :: thesis: verum

end;assume A11: u9 in Support (Low (p,T,i)) ; :: thesis: u9 in Support (Low (p,T,(i + 1)))

then reconsider u = u9 as Element of Bags n ;

u <= HT ((Low (p,T,i)),T),T by A11, TERMORD:def 6;

hence u9 in Support (Low (p,T,(i + 1))) by A5, A2, A7, A10, A9, A11, Th24; :: thesis: verum

then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A3, A6, NAT_1:43;

then - i <= - (i + 1) by XREAL_1:6;

then i + 1 <= i by XREAL_1:24;

then (i + 1) - i <= i - i by XREAL_1:9;

then 1 <= 0 ;

hence contradiction ; :: thesis: verum

A13: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} by A1, Th42;

then Support (Low (p,T,i)) = (Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))} by A1, Th41, XBOOLE_1:45;

then A14: Support (Red ((Low (p,T,i)),T)) = ((Support (Low (p,T,(i + 1)))) \/ {(HT ((Low (p,T,i)),T))}) \ {(HT ((Low (p,T,i)),T))} by TERMORD:36

.= (Support (Low (p,T,(i + 1)))) \ {(HT ((Low (p,T,i)),T))} by XBOOLE_1:40

.= Support (Low (p,T,(i + 1))) by A12, XBOOLE_1:83 ;

A15: now :: thesis: for x being object st x in dom (Low (p,T,(i + 1))) holds

(Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x

dom (Low (p,T,(i + 1))) =
Bags n
by FUNCT_2:def 1
(Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x

let x be object ; :: thesis: ( x in dom (Low (p,T,(i + 1))) implies (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x )

assume x in dom (Low (p,T,(i + 1))) ; :: thesis: (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x

then reconsider b = x as Element of Bags n ;

end;assume x in dom (Low (p,T,(i + 1))) ; :: thesis: (Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x

then reconsider b = x as Element of Bags n ;

now :: thesis: ( ( b in Support (Low (p,T,(i + 1))) & (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b ) or ( not b in Support (Low (p,T,(i + 1))) & (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b ) )end;

hence
(Low (p,T,(i + 1))) . x = (Red ((Low (p,T,i)),T)) . x
; :: thesis: verumper cases
( b in Support (Low (p,T,(i + 1))) or not b in Support (Low (p,T,(i + 1))) )
;

end;

case A16:
b in Support (Low (p,T,(i + 1)))
; :: thesis: (Low (p,T,(i + 1))) . b = (Red ((Low (p,T,i)),T)) . b

then
not b in {(HT ((Low (p,T,i)),T))}
by A13, XBOOLE_0:def 5;

then A17: b <> HT ((Low (p,T,i)),T) by TARSKI:def 1;

thus (Low (p,T,(i + 1))) . b = p . b by A5, A16, Th31

.= (Low (p,T,i)) . b by A1, A4, A16, Th31

.= (Red ((Low (p,T,i)),T)) . b by A4, A16, A17, TERMORD:40 ; :: thesis: verum

end;then A17: b <> HT ((Low (p,T,i)),T) by TARSKI:def 1;

thus (Low (p,T,(i + 1))) . b = p . b by A5, A16, Th31

.= (Low (p,T,i)) . b by A1, A4, A16, Th31

.= (Red ((Low (p,T,i)),T)) . b by A4, A16, A17, TERMORD:40 ; :: thesis: verum

.= dom (Red ((Low (p,T,i)),T)) by FUNCT_2:def 1 ;

hence Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T) by A15, FUNCT_1:2; :: thesis: verum