Problem:
 if(true()) -> X
 if(false()) -> Y
 minus() -> 0()
 minus() -> minus()
 geq() -> true()
 geq() -> false()
 geq() -> geq()
 div(0()) -> 0()
 div(s(X)) -> if(geq())

Proof:
 Fresh Variable Processor: loop length: 1
                           terms:
                            if(true())
                           context: []
                           substitution:
                            X -> if(true())
  Qed