liquid-fixpoint-8.10.7: tests/proof/ple4.fq

// minimal reproduction of LH #1409. UNSAFE with --rewrite; SAFE with --rewrite --noincrple 
fixpoint "--rewrite"

data Peano 0 = [
  | S { prev : Peano}
  | Z { }
  ]

expand [ 1 : True ]
expand [ 2 : True ]

constant isEven : (func(0 , [Peano; int]))

define isEven (n : Peano) : int = { if (is$Z n) then 1 else (1 - ((isEven (prev n)))) }

bind 0 n :  {n: Peano | (isEven n) = 1 }
bind 1 a :  {a: Peano | n = S a }
bind 2 t2 : {v: int   |   a = Z  }

constraint:
  env [0; 1]
  lhs {v : int | true }
  rhs {v : int | 1 + 2 = 3 }
  id 1 tag []

constraint:
  env [0; 1; 2]
  lhs {v : int | true }
  rhs {v : int | false }
  id 2 tag []