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