rule Rule1         {
assert       x>1
;}

    ghost
    noParamsWithAxioms(  )
            returns
            uint {
                                           axiom


                                           myAxiom()            >= 0; axiom
                           hereIsAnotherOne;


                      }
rule Rule2         {
assert       x>2
;}
