let a, b, c be Element of [.0,1.]; max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))
A1:
( 0 <= a & 0 <= b & 0 <= c )
by XXREAL_1:1;
zz:
c - 0 <= 1
by XXREAL_1:1;
then
c - 1 <= 0
by XREAL_1:12;
then y2:
(c - 1) + ((a + b) - 1) <= 0 + ((a + b) - 1)
by XREAL_1:6;
per cases
( ( 0 <= (a + b) - 1 & 0 <= (b + c) - 1 ) or ( 0 > (a + b) - 1 & 0 <= (b + c) - 1 ) or ( 0 > (a + b) - 1 & 0 > (b + c) - 1 ) or ( 0 <= (a + b) - 1 & 0 > (b + c) - 1 ) )
;
suppose Z0:
(
0 > (a + b) - 1 &
0 <= (b + c) - 1 )
;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))then Z1:
max (
0,
((a + b) - 1))
= 0
by XXREAL_0:def 10;
Z2:
max (
0,
((b + c) - 1))
= (b + c) - 1
by Z0, XXREAL_0:def 10;
max (
0,
(((max (0,((a + b) - 1))) + c) - 1)) =
0
by zz, XXREAL_0:def 10, Z1, XREAL_1:12
.=
max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
by Z2, y2, Z0, XXREAL_0:def 10
;
hence
max (
0,
(((max (0,((a + b) - 1))) + c) - 1))
= max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
;
verum end; suppose Z0:
(
0 > (a + b) - 1 &
0 > (b + c) - 1 )
;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))then Z3:
(
c - 1
< 0 &
a - 1
< 0 )
by XREAL_1:9, A1, XREAL_1:31;
Z1:
max (
0,
((a + b) - 1))
= 0
by Z0, XXREAL_0:def 10;
Z2:
max (
0,
((b + c) - 1))
= 0
by Z0, XXREAL_0:def 10;
max (
0,
(((max (0,((a + b) - 1))) + c) - 1)) =
0
by Z3, XXREAL_0:def 10, Z1
.=
max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
by Z2, Z3, XXREAL_0:def 10
;
hence
max (
0,
(((max (0,((a + b) - 1))) + c) - 1))
= max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
;
verum end; suppose Z0:
(
0 <= (a + b) - 1 &
0 > (b + c) - 1 )
;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))ds:
a - 0 <= 1
by XXREAL_1:1;
then
a - 1
<= 0
by XREAL_1:12;
then sb:
(a - 1) + ((b + c) - 1) <= 0 + 0
by Z0;
Z1:
max (
0,
((a + b) - 1))
= (a + b) - 1
by Z0, XXREAL_0:def 10;
max (
0,
(((max (0,((a + b) - 1))) + c) - 1)) =
0
by sb, XXREAL_0:def 10, Z1
.=
max (
0,
((a + 0) - 1))
by XXREAL_0:def 10, XREAL_1:12, ds
.=
max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
by Z0, XXREAL_0:def 10
;
hence
max (
0,
(((max (0,((a + b) - 1))) + c) - 1))
= max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
;
verum end;