import stainless.annotation._
object Unfolding {
   @extern
   def assume(b: Boolean): Unit = {
     ()
   } ensuring(_ => b)

/*
   def q(x:BigInt): BigInt = {
     x*x*x*x + 1
   } ensuring(res => res >= x + 1)

   def testQ(u: BigInt, v: BigInt): Unit = {
     val r = q((u - v)*(u - v - 17))       // x = 1000
     //assume(r >= BigInt(1000) + BigInt(1)) // from res >= x + 1
     assert(r >= (u - v)*(u - v - 17) + 1)
   } 
   */

   def plusG(x: BigInt, y: BigInt): BigInt = {
     if (x <= 0) y
     else plusG(x - 1, y + 1)
   }.ensuring(res => res >= y)
/*

   def plusG0(x: BigInt, y: BigInt, any: BigInt): BigInt = {
     if (x <= 0) y
     else any
   }.ensuring(res => res >= y)
*/

   def plusG1(x: BigInt, y: BigInt, any: BigInt): BigInt = {
     if (x <= 0) y
     else {
       val r = {       
         val x1 = x - 1
         val y1 = y + 1
         if (x1 <= 0) y1
         else ???      
       }
       assume(r >= y + 1)
       r
     }
   }.ensuring(res => res >= y)
   /*
                                                           // P(0)   P(n) ==> P(n+1)     P(0) ==> P(1) ==> P(2) ==>...
   def testPlusG4(x: BigInt, y: BigInt): BigInt = {
     val r = {
       if (x <= 0) y
       else {
         val x1 = x - 1
         val y1 = y + 1
         if (x1 <= 0) y1
         else {
           val x2 = x1 - 1
           val y2 = y1 + 1
           if (x2 <= 0) y2
           else {
             val x3 = x2 - 1
             val y3 = y2 + 1
             if (x3 <= 0) y3
             else BigInt(0) // irrelevant, branch not taken for given x,y
           }
         }
       }
     }
     r
   }      
  */
}
