deffunc H_{1}( Real, Real) -> Element of REAL = In ((max ($1,$2)),REAL);

consider f being BinOp of REAL such that

A1: for x, y being Element of REAL holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

A2: for x, y being Element of REAL holds f . (x,y) = max (x,y)

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )

assume that

A3: M is calculating_type and

A4: the carrier of M = succ REAL and

A5: the FinalS of M = REAL and

A6: the InitS of M = REAL and

A7: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st

( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st

( x < y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )

assume that

A8: for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = x and

A9: for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ; :: thesis: for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M

let x, y be Element of REAL ; :: thesis: max (x,y) is_result_of [x,y],M

reconsider x = x, y = y as Element of REAL ;

hence max (x,y) is_result_of [x,y],M by A2; :: thesis: verum

consider f being BinOp of REAL such that

A1: for x, y being Element of REAL holds f . (x,y) = H

A2: for x, y being Element of REAL holds f . (x,y) = max (x,y)

proof

let M be non empty Moore-SM_Final over [: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 >= y holds
let x, y be Element of REAL ; :: thesis: f . (x,y) = max (x,y)

f . (x,y) = H_{1}(x,y)
by A1;

hence f . (x,y) = max (x,y) ; :: thesis: verum

end;f . (x,y) = H

hence f . (x,y) = max (x,y) ; :: thesis: verum

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )

assume that

A3: M is calculating_type and

A4: the carrier of M = succ REAL and

A5: the FinalS of M = REAL and

A6: the InitS of M = REAL and

A7: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st

( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st

( x < y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )

assume that

A8: for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = x and

A9: for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ; :: thesis: for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M

let x, y be Element of REAL ; :: thesis: max (x,y) is_result_of [x,y],M

reconsider x = x, y = y as Element of REAL ;

now :: thesis: for x, y being Element of REAL holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)

then
f . (x,y) is_result_of [x,y],M
by A3, A4, A5, A6, A7, Th22;let x, y be Element of REAL ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)

A10: ( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A8;

( x < y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A9;

then the Tran of M . [ the InitS of M,[x,y]] = max (x,y) by A10, XXREAL_0:def 10;

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

end;A10: ( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A8;

( x < y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A9;

then the Tran of M . [ the InitS of M,[x,y]] = max (x,y) by A10, XXREAL_0:def 10;

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

hence max (x,y) is_result_of [x,y],M by A2; :: thesis: verum