deffunc H₁( Real, Real) -> Element of REAL = max ((sgn $1),(sgn $2));
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
let M be non empty Moore-SM_Final of [:REAL,REAL:], succ REAL; :: thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds
the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st
( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st
( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st
( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )
assume that
A7: for x, y being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 and
A8: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds
the Tran of M . [ the InitS of M,[x,y]] = 0 and
A9: for x, y being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ; :: thesis: for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M
let x, y be Real; :: thesis: max ((sgn x),(sgn y)) is_result_of [x,y],M

now

let x, y be Real; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

proof

now

per cases ( x > 0 or x = 0 or x < 0 ) ;

suppose A10: x > 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then A11: sgn x = 1 by ABSVALUE:def 2;

now

per cases ( y > 0 or y = 0 or y < 0 ) ;

suppose y > 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 1 by ABSVALUE:def 2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10, A11; :: thesis: verum

end;

suppose y = 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 0 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; :: thesis: verum

end;

suppose y < 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = - 1 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; :: thesis: verum

end;

end;

end;

hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; :: thesis: verum

end;

suppose A12: x = 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then A13: sgn x = 0 by ABSVALUE:def 2;

now

per cases ( y > 0 or y = 0 or y < 0 ) ;

suppose A14: y > 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 1 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 1 by A13, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A14; :: thesis: verum

end;

suppose A15: y = 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 0 by ABSVALUE:def 2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A15; :: thesis: verum

end;

suppose A16: y < 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = - 1 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 0 by A13, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A16; :: thesis: verum

end;

end;

end;

hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; :: thesis: verum

end;

suppose A17: x < 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then A18: sgn x = - 1 by ABSVALUE:def 2;

now

per cases ( y > 0 or y = 0 or y < 0 ) ;

suppose A19: y > 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 1 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 1 by A18, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A19; :: thesis: verum

end;

suppose A20: y = 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = 0 by ABSVALUE:def 2;
then max ((sgn x),(sgn y)) = 0 by A18, XXREAL_0:def 10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A17, A20; :: thesis: verum

end;

suppose A21: y < 0 ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))

then sgn y = - 1 by ABSVALUE:def 2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A9, A17, A18, A21; :: thesis: verum

end;

end;

end;

hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; :: thesis: verum

end;

end;

end;

hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; :: thesis: verum

end;

hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; :: thesis: verum

end;

then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence max ((sgn x),(sgn y)) is_result_of [x,y],M by A1; :: thesis: verum