/*@ <webex id="RISCAL" type="riscal"
       header="RISCAL Web Interface" 
       href="https://www.risc.jku.at/research/formal/software/RISCAL">
@*/

//@ <option id="silent" label="Silent:" type="bool">
//@ <option id="nondet" label="Nondeterminism:" type="bool">
//@ <option id="multi" label="Multithreaded:" type="bool">
//@ <option id="threads" label="Threads:" type="int" min="2" max="4">

//@ <input id="in" cols="98" rows="15">
// enter your specification
val N = 5;
type D = ℕ[N];

theorem T(x:D) ⇔ x > 0 ⇒ ∃y:D. y+1 = x;

// provide entry point for execution
proc main():()
{
  check T;
}
//@ </input>

/*@ <button id="run" label="Run main()" action="main">
    <argument value="-opt-si"> <argument option="silent">
    <argument value="-opt-nd"> <argument option="nondet">
    <argument value="-opt-mt"> <argument option="multi">
    <argument value="-opt-tr"> <argument option="threads">
    </button>
@*/