minAxiom {
\schemaVar \variables alpha x , y , z ;
\schemaVar \term boolean b ;
\schemaVar \term int t , t2 ;
\find ( min { x ; } ( b , t )= t2 ==> )
\varcond "Use Axiom" : \add ( \forall y ; {\subst x ; y } ( b = TRUE -> t >= t2 )& \exists y ; {\subst x ; y } ( b = TRUE & t = t2 )==> );
"Show Satisfiability" : \add ( ==> \exists x ; ( b = TRUE & \forall y ; ( {\subst x ; y } b = TRUE -> {\subst x ; y } t >= t )))
};defined in: epsilon.key Line: 26 Offset :4maxAxiom {
\schemaVar \variables alpha x , y , z ;
\schemaVar \term boolean b ;
\schemaVar \term int t , t2 ;
\find ( max { x ; } ( b , t )= t2 ==> )
\varcond "Use Axiom" : \add ( \forall y ; {\subst x ; y } ( b = TRUE -> t <= t2 )& \exists y ; {\subst x ; y } ( b = TRUE & t = t2 )==> );
"Show Satisfiability" : \add ( ==> \exists x ; ( b = TRUE & \forall y ; ( {\subst x ; y } b = TRUE -> {\subst x ; y } t <= t )))
};defined in: epsilon.key Line: 54 Offset :4