; Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
; Command Line Options: -nologo -logPrefix:inline /proverLog:expansion2.sx expansion2.bpl
; Proof obligation: foo
; Z3 command line: c:\Program Files\Microsoft Research\Z3-2.0\bin\z3.exe /si /@ /cex:5 /t:0
; User supplied Z3 options:
; Prover options: 
; 
(SETPARAMETER MODEL_PARTIAL true)
(SETPARAMETER MODEL_VALUE_COMPLETION false)
(SETPARAMETER MODEL_HIDE_UNUSED_PARTITIONS false)
(SETPARAMETER MODEL_V1 true)
(SETPARAMETER ASYNC_COMMANDS false)
(SETPARAMETER PHASE_SELECTION 0)
(SETPARAMETER RESTART_STRATEGY 0)
(SETPARAMETER RESTART_FACTOR |1.5|)
(SETPARAMETER NNF_SK_HACK true)
(SETPARAMETER QI_EAGER_THRESHOLD 100)
(SETPARAMETER ARITH_RANDOM_INITIAL_VALUE true)
(SETPARAMETER SORT_AND_OR false)
(SETPARAMETER CASE_SPLIT 3)
(SETPARAMETER DELAY_UNITS true)
(SETPARAMETER DELAY_UNITS_THRESHOLD 16)
(SETPARAMETER TYPE_CHECK true)
(SETPARAMETER BV_REFLECT true)
; -------------------------------------------------------------------------
; Boogie 2 universal background predicate for Z3 (Simplify notation with types)
; Copyright (c) 2004-2009, Microsoft Corp.

(DEFTYPE $int :BUILTIN Int)
(DEFTYPE $bool :BUILTIN bool)
(DEFTYPE U)
(DEFTYPE T)

(DEFOP <: U U $bool)         ; used for translation with type premisses
(DEFOP <:: T U U $bool)      ; used for translation with type arguments

(BG_PUSH (AND

  ; false is not true

  (DISTINCT |@false| |@true|)

  ; we assume type correctness of the operations here
  ; a-l>=0 ==> (v ++ w:l)[a:b] = v[a-l:b-l]
  (FORALL (v lv w lw lvw a b)
    (QID bv:e:c1)
    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))
    (IMPLIES
      (>= (- a lw) 0)
      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract v lv (- a lw) (- b lw)))))

  ; b<=l ==> (v ++ w:l)[a:b] = w[a:b]
  (FORALL (v lv w lw lvw a b)
    (QID bv:e:c2)
    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))
    (IMPLIES
      (<= b lw)
      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract w lw a b))))

  ; v:l
  ; a>=x || b<=y ==> (v[x:l] ++ w ++ v[0:y])[a:b] = v[a:b]
  (FORALL (v lv x lxv w lw lwy y a b)
    (QID bv:e:c3)
    (PATS 
      ($bv_extract 
        ($bv_concat 
          ($bv_extract v lv x lv) lxv
	  ($bv_concat 
	    w lw
            ($bv_extract v lv 0 y) y) lwy) lv a b))
    (IMPLIES
      (AND
        (EQ lw (- x y))
        (EQ lxv (- lv x))
        (EQ lwy (+ w y))
        (OR (>= a x) (<= b y)))
      (EQ
        ($bv_extract 
          ($bv_concat 
            ($bv_extract v lv x lv) lxv
	    ($bv_concat 
	      w lw
              ($bv_extract v lv 0 y) y) lwy) lv a b)
	($bv_extract v lv a b))))

  ; a>=x ==> (v[x:l] ++ w)[a:b] = v[a:b]
  (FORALL (v lv x lxv w a b)
    (QID bv:e:c4)
    (PATS 
      ($bv_extract 
        ($bv_concat 
          ($bv_extract v lv x lv) lxv 
	  w x) 
	lv a b))
    (IMPLIES
      (AND
        (EQ lxv (- lv x))
        (>= a x))
      (EQ
        ($bv_extract 
          ($bv_concat 
            ($bv_extract v lv x lv) lxv 
	    w x) 
	  lv a b)
	($bv_extract v lv a b))))

  (FORALL (v l)
    (QID bv:e:0)
    (PATS ($bv_extract v l 0 l))
      (EQ ($bv_extract v l 0 l) v))

  (FORALL (n)
    (QID bv:pow)
    (PATS ($pow2 n))
      (IMPLIES (> n 0) (EQ ($pow2 n) (* 2 ($pow2 (- n 1))))))

  (EQ ($pow2 0) 1)

  ; 0 <= v < 2^Y ==> 0bvX ++ v[0:Y] == v
  (FORALL (v l a b)
    (QID bv:e:pow)
    (PATS ($bv_concat 0 b ($bv_extract v l 0 a) a))
    (IMPLIES
      (AND
        (<= 0 v)
        (< v ($pow2 a))
        (EQ l (+ a b)))
      (EQ ($bv_concat 0 b ($bv_extract v l 0 a) a) v)))
  
  ; X > 0 ==> 0bvX ++ v >= 0
  (FORALL (v a b)
    (QID bv:e:pos)
    (PATS ($bv_concat 0 b v a))
    (IMPLIES
      (> b 0)
      (>= ($bv_concat 0 b v a) 0)))

  ;; unsound?
;  (FORALL (lv w lw)
;    (QID bv:c:0)
;    (PATS ($bv_concat 0 lv w lw))
;    (EQ ($bv_concat 0 lv w lw) w))
  ;; matching loop
;  (FORALL (v l1 a b l2 c d)
;    (QID bv:e:e)
;    (PATS ($bv_extract ($bv_extract v l1 a b) l2 c d))
;    (EQ ($bv_extract ($bv_extract v l1 a b) l2 c d) ($bv_extract v l1 (+ c a) (+ d a))))
  

  ; Reflect plus
  (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))

))  ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------



(DEFOP Ctor T $int)
(DEFOP intType T)
(DEFOP boolType T)
(DEFOP int_2_U $int U)
(DEFOP U_2_int U $int)
(DEFOP type U T)
(DEFOP bool_2_U $bool U)
(DEFOP U_2_bool U $bool)
(BG_PUSH 
(AND (EQ (Ctor (intType)) 0) (EQ (Ctor (boolType)) 1) (FORALL (arg0 :TYPE $int) (PATS (int_2_U arg0)) (QID typeInv:U_2_int) (EQ (U_2_int (int_2_U arg0)) arg0)) (FORALL (x :TYPE U) (PATS (int_2_U (U_2_int x))) (QID cast:U_2_int) (IMPLIES (EQ (type x) (intType)) (EQ (int_2_U (U_2_int x)) x))) (FORALL (arg0@@0 :TYPE $int) (PATS (int_2_U arg0@@0)) (QID funType:int_2_U) (EQ (type (int_2_U arg0@@0)) (intType))) (FORALL (arg0@@1 :TYPE $bool) (PATS (bool_2_U arg0@@1)) (QID typeInv:U_2_bool) (IFF (U_2_bool (bool_2_U arg0@@1)) arg0@@1)) (FORALL (x@@0 :TYPE U) (PATS (bool_2_U (U_2_bool x@@0))) (QID cast:U_2_bool) (IMPLIES (EQ (type x@@0) (boolType)) (EQ (bool_2_U (U_2_bool x@@0)) x@@0))) (FORALL (arg0@@2 :TYPE $bool) (PATS (bool_2_U arg0@@2)) (QID funType:bool_2_U) (EQ (type (bool_2_U arg0@@2)) (boolType))))
)
(BG_PUSH 
(AND (FORALL (x@@1 :TYPE U) (NOPATS (U_2_int x@@1) (U_2_bool x@@1)) (QID bg:subtype-refl) (<: x@@1 x@@1)) (FORALL (x@@2 :TYPE U y :TYPE U z :TYPE U) (PATS (MPAT (<: x@@2 y) (<: y z))) (QID bg:subtype-trans) (LET ((TERM alpha (type x@@2))) (IMPLIES (AND (EQ (type y) alpha) (EQ (type z) alpha)) (IMPLIES (AND (<: x@@2 y) (<: y z)) (<: x@@2 z))))) (FORALL (x@@3 :TYPE U y@@0 :TYPE U) (PATS (MPAT (<: x@@3 y@@0) (<: y@@0 x@@3))) (QID bg:subtype-antisymm) (LET ((TERM alpha@@0 (type x@@3))) (IMPLIES (EQ (type y@@0) alpha@@0) (IMPLIES (AND (<: x@@3 y@@0) (<: y@@0 x@@3)) (EQ x@@3 y@@0))))) (FORALL (z@@0 :TYPE $int) (QID expansio.6:15) (SKOLEMID 2) (IMPLIES (> z@@0 12) (> z@@0 0))) (FORALL (y@@1 :TYPE $int) (QID expansio.7:15) (SKOLEMID 3) (IMPLIES (> (+ y@@1 1) 1) (> y@@1 0))))
)
; Initialized all axioms.
(BG_PUSH 
TRUE
)
(LET ((FORMULA anon0_correct (IMPLIES (LBLPOS |+107| TRUE) (IMPLIES TRUE (AND (LBLNEG |@164| (> 12 0)) (IMPLIES (> 12 0) (AND (LBLNEG |@168| (EQ (+ 3 1) 4)) (IMPLIES (EQ (+ 3 1) 4) (IMPLIES TRUE TRUE))))))))) anon0_correct)
; Valid