let a, b, c be Element of [.0,1.]; :: thesis: 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 ) ; :: thesis: 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)) = (a + b) - 1 by XXREAL_0:def 10;
max (0,((b + c) - 1)) = (b + c) - 1 by ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Z1; :: thesis: verum
end;
suppose Z0: ( 0 > (a + b) - 1 & 0 <= (b + c) - 1 ) ; :: thesis: 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 ;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum
end;
suppose Z0: ( 0 > (a + b) - 1 & 0 > (b + c) - 1 ) ; :: thesis: 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 ;
Z1: max (0,((a + b) - 1)) = 0 by ;
Z2: max (0,((b + c) - 1)) = 0 by ;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum
end;
suppose Z0: ( 0 <= (a + b) - 1 & 0 > (b + c) - 1 ) ; :: thesis: 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 ;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by
.= max (0,((a + 0) - 1)) by
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum
end;
end;