ite_normalize.coma

module M_ite_normalize__qyi15119799284333837974__clone [#"ite_normalize.rs" 55 9 55 14] (* <Expr as creusot_contracts::Clone> *)
  let%span site_normalize0 = "ite_normalize.rs" 55 9 55 14
  let%span sclone1 = "../../creusot-contracts/src/std/clone.rs" 15 26 15 41
  let%span site_normalize2 = "ite_normalize.rs" 72 26 72 41
  
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  let rec v_Var'0 (input:t_Expr'0) (ret  (v:UInt64.t))= any
    [ good (v:UInt64.t)-> {C_Var'0 v = input} (! ret {v})
    | bad -> {forall v : UInt64.t [C_Var'0 v : t_Expr'0] . C_Var'0 v <> input} (! {false} any) ]
  
  
  let rec clone'1 (self:UInt64.t) (return'  (ret:UInt64.t))= any
    [ return' (result:UInt64.t)-> {[%#sclone1] result = self} (! return' {result}) ]
  
  
  let rec v_IfThenElse'0 (input:t_Expr'0) (ret  (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0))= any
    [ good (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0)-> {C_IfThenElse'0 c t e = input} (! ret {c} {t} {e})
    | bad -> {forall c : t_Expr'0, t : t_Expr'0, e : t_Expr'0 [C_IfThenElse'0 c t e : t_Expr'0] . C_IfThenElse'0 c t e
      <> input}
      (! {false}
      any) ]
  
  
  let rec clone'2 (self:t_Expr'0) (return'  (ret:t_Expr'0))= any
    [ return' (result:t_Expr'0)-> {[%#site_normalize2] result = self} (! return' {result}) ]
  
  
  meta "compute_max_steps" 1000000
  
  let rec clone'0[#"ite_normalize.rs" 55 9 55 14] (self:t_Expr'0) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = any
      [ br0 (x0:t_Expr'0) (x1:t_Expr'0) (x2:t_Expr'0)-> {self = C_IfThenElse'0 x0 x1 x2} (! bb2)
      | br1 (x0:UInt64.t)-> {self = C_Var'0 x0} (! bb3)
      | br2 -> {self = C_True'0} (! bb4)
      | br3 -> {self = C_False'0} (! bb5) ]
    
    | bb5 = s0 [ s0 =  [ &_0 <- C_False'0 ] s1 | s1 = bb16 ] 
    | bb4 = bb6
    | bb6 = s0 [ s0 =  [ &_0 <- C_True'0 ] s1 | s1 = bb16 ] 
    | bb3 = bb7
    | bb7 = s0
      [ s0 = v_Var'0 {self} (fun (rv'0:UInt64.t) ->  [ &v_1 <- rv'0 ] s1)
      | s1 =  [ &_19 <- v_1 ] s2
      | s2 = clone'1 {_19} (fun (_ret':UInt64.t) ->  [ &_17 <- _ret' ] s3)
      | s3 = bb15 ]
    
    | bb15 = s0 [ s0 =  [ &_0 <- C_Var'0 _17 ] s1 | s1 = bb16 ] 
    | bb2 = bb8
    | bb8 = s0
      [ s0 = v_IfThenElse'0 {self} (fun (rc'0:t_Expr'0) (rt'0:t_Expr'0) (re'0:t_Expr'0) ->  [ &c_1 <- rc'0 ] s1)
      | s1 = v_IfThenElse'0 {self} (fun (rc'1:t_Expr'0) (rt'1:t_Expr'0) (re'1:t_Expr'0) ->  [ &t_1 <- rt'1 ] s2)
      | s2 = v_IfThenElse'0 {self} (fun (rc'2:t_Expr'0) (rt'2:t_Expr'0) (re'2:t_Expr'0) ->  [ &e_1 <- re'2 ] s3)
      | s3 =  [ &_9 <- c_1 ] s4
      | s4 = clone'2 {_9} (fun (_ret':t_Expr'0) ->  [ &_7 <- _ret' ] s5)
      | s5 = bb9 ]
    
    | bb9 = s0
      [ s0 =  [ &_12 <- t_1 ] s1 | s1 = clone'2 {_12} (fun (_ret':t_Expr'0) ->  [ &_10 <- _ret' ] s2) | s2 = bb10 ]
    
    | bb10 = s0
      [ s0 =  [ &_15 <- e_1 ] s1 | s1 = clone'2 {_15} (fun (_ret':t_Expr'0) ->  [ &_13 <- _ret' ] s2) | s2 = bb11 ]
    
    | bb11 = s0 [ s0 =  [ &_0 <- C_IfThenElse'0 _7 _10 _13 ] s1 | s1 = bb12 ] 
    | bb12 = bb13
    | bb13 = bb14
    | bb14 = bb16
    | bb16 = return' {_0} ]
    )
    [ & _0 : t_Expr'0 = Any.any_l ()
    | & self : t_Expr'0 = self
    | & c_1 : t_Expr'0 = Any.any_l ()
    | & t_1 : t_Expr'0 = Any.any_l ()
    | & e_1 : t_Expr'0 = Any.any_l ()
    | & _7 : t_Expr'0 = Any.any_l ()
    | & _9 : t_Expr'0 = Any.any_l ()
    | & _10 : t_Expr'0 = Any.any_l ()
    | & _12 : t_Expr'0 = Any.any_l ()
    | & _13 : t_Expr'0 = Any.any_l ()
    | & _15 : t_Expr'0 = Any.any_l ()
    | & v_1 : UInt64.t = Any.any_l ()
    | & _17 : UInt64.t = Any.any_l ()
    | & _19 : UInt64.t = Any.any_l () ]
     [ return' (result:t_Expr'0)-> {[@expl:clone ensures] [%#site_normalize0] result = self} (! return' {result}) ] 
end
module M_ite_normalize__qyi12210208226808281580__from [#"ite_normalize.rs" 80 4 80 29] (* <Expr as std::convert::From<usize>> *)
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  let rec variable'0 (v:UInt64.t) (return'  (ret:t_Expr'0))= any [ return' (result:t_Expr'0)-> (! return' {result}) ] 
  
  meta "compute_max_steps" 1000000
  
  let rec from'0[#"ite_normalize.rs" 80 4 80 29] (a:UInt64.t) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = s0 [ s0 = variable'0 {a} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb1 ]  | bb1 = return' {_0} ]
    ) [ & _0 : t_Expr'0 = Any.any_l () | & a : UInt64.t = a ]  [ return' (result:t_Expr'0)-> (! return' {result}) ] 
end
module M_ite_normalize__qyi1874907776010341903__from [#"ite_normalize.rs" 86 4 86 28] (* <Expr as std::convert::From<bool>> *)
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  meta "compute_max_steps" 1000000
  
  let rec from'0[#"ite_normalize.rs" 86 4 86 28] (b:bool) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = any [ br0 -> {b = false} (! bb2) | br1 -> {b} (! bb1) ] 
    | bb1 = s0 [ s0 =  [ &_0 <- C_True'0 ] s1 | s1 = bb3 ] 
    | bb2 = s0 [ s0 =  [ &_0 <- C_False'0 ] s1 | s1 = bb3 ] 
    | bb3 = return' {_0} ]
    ) [ & _0 : t_Expr'0 = Any.any_l () | & b : bool = b ]  [ return' (result:t_Expr'0)-> (! return' {result}) ] 
end
module M_ite_normalize__qyi17570407315987535457__ite [#"ite_normalize.rs" 93 4 93 49] (* Expr *)
  let%span site_normalize0 = "ite_normalize.rs" 92 14 92 91
  
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  meta "compute_max_steps" 1000000
  
  let rec ite'0[#"ite_normalize.rs" 93 4 93 49] (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = bb1
    | bb1 = bb2
    | bb2 = bb3
    | bb3 = bb4
    | bb4 = s0 [ s0 =  [ &_0 <- C_IfThenElse'0 c t e ] s1 | s1 = bb5 ] 
    | bb5 = bb6
    | bb6 = bb7
    | bb7 = bb8
    | bb8 = bb9
    | bb9 = bb10
    | bb10 = return' {_0} ]
    ) [ & _0 : t_Expr'0 = Any.any_l () | & c : t_Expr'0 = c | & t : t_Expr'0 = t | & e : t_Expr'0 = e ] 
    [ return' (result:t_Expr'0)-> {[@expl:ite ensures] [%#site_normalize0] result = C_IfThenElse'0 c t e}
      (! return' {result}) ]

end
module M_ite_normalize__qyi17570407315987535457__variable [#"ite_normalize.rs" 97 4 97 37] (* Expr *)
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  meta "compute_max_steps" 1000000
  
  let rec variable'0[#"ite_normalize.rs" 97 4 97 37] (v:UInt64.t) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = s0 [ s0 =  [ &_0 <- C_Var'0 v ] s1 | s1 = return' {_0} ]  ]
    ) [ & _0 : t_Expr'0 = Any.any_l () | & v : UInt64.t = v ]  [ return' (result:t_Expr'0)-> (! return' {result}) ] 
end
module M_ite_normalize__qyi17570407315987535457__transpose [#"ite_normalize.rs" 106 4 106 52] (* Expr *)
  let%span site_normalize0 = "ite_normalize.rs" 101 15 101 35
  let%span site_normalize1 = "ite_normalize.rs" 102 15 102 32
  let%span site_normalize2 = "ite_normalize.rs" 103 15 103 32
  let%span site_normalize3 = "ite_normalize.rs" 104 14 104 36
  let%span site_normalize4 = "ite_normalize.rs" 105 14 105 18
  let%span site_normalize5 = "ite_normalize.rs" 55 9 55 14
  let%span site_normalize6 = "ite_normalize.rs" 123 8 136 9
  
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  let rec v_IfThenElse'0 (input:t_Expr'0) (ret  (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0))= any
    [ good (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0)-> {C_IfThenElse'0 c t e = input} (! ret {c} {t} {e})
    | bad -> {forall c : t_Expr'0, t : t_Expr'0, e : t_Expr'0 [C_IfThenElse'0 c t e : t_Expr'0] . C_IfThenElse'0 c t e
      <> input}
      (! {false}
      any) ]
  
  
  let rec clone'0 (self:t_Expr'0) (return'  (ret:t_Expr'0))= any
    [ return' (result:t_Expr'0)-> {[%#site_normalize5] result = self} (! return' {result}) ]
  
  
  predicate is_normalized'0 [#"ite_normalize.rs" 122 4 122 34] (self : t_Expr'0) =
    [%#site_normalize6] match self with
      | C_IfThenElse'0 c t e -> is_normalized'0 c
      /\ is_normalized'0 t
      /\ is_normalized'0 e
      /\ match c with
        | C_IfThenElse'0 _ _ _ -> false
        | _ -> true
        end
      | C_Var'0 _ -> true
      | C_True'0 -> true
      | C_False'0 -> true
      end
  
  meta "compute_max_steps" 1000000
  
  let rec transpose'0[#"ite_normalize.rs" 106 4 106 52] (self:t_Expr'0) (a:t_Expr'0) (b:t_Expr'0) (return'  (ret:t_Expr'0))= {[@expl:transpose requires #0] [%#site_normalize0] is_normalized'0 self}
    {[@expl:transpose requires #1] [%#site_normalize1] is_normalized'0 a}
    {[@expl:transpose requires #2] [%#site_normalize2] is_normalized'0 b}
    (! bb0
    [ bb0 = bb1
    | bb1 = bb2
    | bb2 = bb3
    | bb3 = bb4
    | bb4 = any
      [ br0 (x0:t_Expr'0) (x1:t_Expr'0) (x2:t_Expr'0)-> {self = C_IfThenElse'0 x0 x1 x2} (! bb6)
      | br1 (x0:UInt64.t)-> {self = C_Var'0 x0} (! bb7)
      | br2 -> {self = C_True'0} (! bb8)
      | br3 -> {self = C_False'0} (! bb9) ]
    
    | bb9 = s0 [ s0 =  [ &_0 <- b ] s1 | s1 = bb31 ] 
    | bb8 = bb10
    | bb10 = s0 [ s0 =  [ &_0 <- a ] s1 | s1 = bb31 ] 
    | bb7 = bb11
    | bb11 = bb25
    | bb25 = bb26
    | bb26 = bb27
    | bb27 = s0 [ s0 =  [ &_0 <- C_IfThenElse'0 self a b ] s1 | s1 = bb28 ] 
    | bb28 = bb29
    | bb29 = bb30
    | bb30 = bb31
    | bb6 = bb12
    | bb12 = s0
      [ s0 = v_IfThenElse'0 {self} (fun (rc'0:t_Expr'0) (rt'0:t_Expr'0) (re'0:t_Expr'0) ->  [ &c <- rc'0 ] s1)
      | s1 = v_IfThenElse'0 {self} (fun (rc'1:t_Expr'0) (rt'1:t_Expr'0) (re'1:t_Expr'0) ->  [ &t <- rt'1 ] s2)
      | s2 = v_IfThenElse'0 {self} (fun (rc'2:t_Expr'0) (rt'2:t_Expr'0) (re'2:t_Expr'0) ->  [ &e <- re'2 ] s3)
      | s3 = clone'0 {a} (fun (_ret':t_Expr'0) ->  [ &_17 <- _ret' ] s4)
      | s4 = bb13 ]
    
    | bb13 = s0 [ s0 = clone'0 {b} (fun (_ret':t_Expr'0) ->  [ &_19 <- _ret' ] s1) | s1 = bb14 ] 
    | bb14 = s0 [ s0 = transpose'0 {t} {_17} {_19} (fun (_ret':t_Expr'0) ->  [ &_15 <- _ret' ] s1) | s1 = bb15 ] 
    | bb15 = bb16
    | bb16 = s0 [ s0 = transpose'0 {e} {a} {b} (fun (_ret':t_Expr'0) ->  [ &_22 <- _ret' ] s1) | s1 = bb17 ] 
    | bb17 = bb18
    | bb18 = s0 [ s0 =  [ &_0 <- C_IfThenElse'0 c _15 _22 ] s1 | s1 = bb19 ] 
    | bb19 = bb20
    | bb20 = bb21
    | bb21 = bb22
    | bb22 = bb23
    | bb23 = bb24
    | bb24 = bb31
    | bb31 = bb32
    | bb32 = bb33
    | bb33 = bb34
    | bb34 = return' {_0} ]
    )
    [ & _0 : t_Expr'0 = Any.any_l ()
    | & self : t_Expr'0 = self
    | & a : t_Expr'0 = a
    | & b : t_Expr'0 = b
    | & c : t_Expr'0 = Any.any_l ()
    | & t : t_Expr'0 = Any.any_l ()
    | & e : t_Expr'0 = Any.any_l ()
    | & _15 : t_Expr'0 = Any.any_l ()
    | & _17 : t_Expr'0 = Any.any_l ()
    | & _19 : t_Expr'0 = Any.any_l ()
    | & _22 : t_Expr'0 = Any.any_l () ]
    
    [ return' (result:t_Expr'0)-> {[@expl:transpose ensures] [%#site_normalize3] is_normalized'0 result}
      (! return' {result}) ]

end
module M_ite_normalize__qyi17570407315987535457__normalize [#"ite_normalize.rs" 141 4 141 35] (* Expr *)
  let%span site_normalize0 = "ite_normalize.rs" 139 14 139 36
  let%span site_normalize1 = "ite_normalize.rs" 140 14 140 18
  let%span site_normalize2 = "ite_normalize.rs" 55 9 55 14
  let%span site_normalize3 = "ite_normalize.rs" 101 15 101 35
  let%span site_normalize4 = "ite_normalize.rs" 102 15 102 32
  let%span site_normalize5 = "ite_normalize.rs" 103 15 103 32
  let%span site_normalize6 = "ite_normalize.rs" 104 14 104 36
  let%span site_normalize7 = "ite_normalize.rs" 105 14 105 18
  let%span site_normalize8 = "ite_normalize.rs" 123 8 136 9
  
  use creusot.int.UInt64
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  let rec clone'0 (self:t_Expr'0) (return'  (ret:t_Expr'0))= any
    [ return' (result:t_Expr'0)-> {[%#site_normalize2] result = self} (! return' {result}) ]
  
  
  let rec v_IfThenElse'0 (input:t_Expr'0) (ret  (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0))= any
    [ good (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0)-> {C_IfThenElse'0 c t e = input} (! ret {c} {t} {e})
    | bad -> {forall c : t_Expr'0, t : t_Expr'0, e : t_Expr'0 [C_IfThenElse'0 c t e : t_Expr'0] . C_IfThenElse'0 c t e
      <> input}
      (! {false}
      any) ]
  
  
  predicate is_normalized'0 [#"ite_normalize.rs" 122 4 122 34] (self : t_Expr'0) =
    [%#site_normalize8] match self with
      | C_IfThenElse'0 c t e -> is_normalized'0 c
      /\ is_normalized'0 t
      /\ is_normalized'0 e
      /\ match c with
        | C_IfThenElse'0 _ _ _ -> false
        | _ -> true
        end
      | C_Var'0 _ -> true
      | C_True'0 -> true
      | C_False'0 -> true
      end
  
  let rec transpose'0 (self:t_Expr'0) (a:t_Expr'0) (b:t_Expr'0) (return'  (ret:t_Expr'0))= {[@expl:transpose requires #0] [%#site_normalize3] is_normalized'0 self}
    {[@expl:transpose requires #1] [%#site_normalize4] is_normalized'0 a}
    {[@expl:transpose requires #2] [%#site_normalize5] is_normalized'0 b}
    any [ return' (result:t_Expr'0)-> {[%#site_normalize6] is_normalized'0 result} (! return' {result}) ] 
  
  meta "compute_max_steps" 1000000
  
  let rec normalize'0[#"ite_normalize.rs" 141 4 141 35] (self:t_Expr'0) (return'  (ret:t_Expr'0))= (! bb0
    [ bb0 = any
      [ br0 (x0:t_Expr'0) (x1:t_Expr'0) (x2:t_Expr'0)-> {self = C_IfThenElse'0 x0 x1 x2} (! bb2)
      | br1 (x0:UInt64.t)-> {self = C_Var'0 x0} (! bb1)
      | br2 -> {self = C_True'0} (! bb1)
      | br3 -> {self = C_False'0} (! bb1) ]
    
    | bb1 = s0
      [ s0 =  [ &e1 <- self ] s1 | s1 = clone'0 {e1} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s2) | s2 = bb11 ]
    
    | bb11 = bb12
    | bb2 = bb3
    | bb3 = s0
      [ s0 = v_IfThenElse'0 {self} (fun (rc'0:t_Expr'0) (rt'0:t_Expr'0) (re'0:t_Expr'0) ->  [ &c <- rc'0 ] s1)
      | s1 = v_IfThenElse'0 {self} (fun (rc'1:t_Expr'0) (rt'1:t_Expr'0) (re'1:t_Expr'0) ->  [ &t <- rt'1 ] s2)
      | s2 = v_IfThenElse'0 {self} (fun (rc'2:t_Expr'0) (rt'2:t_Expr'0) (re'2:t_Expr'0) ->  [ &e <- re'2 ] s3)
      | s3 = normalize'0 {c} (fun (_ret':t_Expr'0) ->  [ &cp <- _ret' ] s4)
      | s4 = bb4 ]
    
    | bb4 = s0 [ s0 = normalize'0 {t} (fun (_ret':t_Expr'0) ->  [ &tp <- _ret' ] s1) | s1 = bb5 ] 
    | bb5 = s0 [ s0 = normalize'0 {e} (fun (_ret':t_Expr'0) ->  [ &ep <- _ret' ] s1) | s1 = bb6 ] 
    | bb6 = s0 [ s0 = transpose'0 {cp} {tp} {ep} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb7 ] 
    | bb7 = bb8
    | bb8 = bb9
    | bb9 = bb10
    | bb10 = bb12
    | bb12 = return' {_0} ]
    )
    [ & _0 : t_Expr'0 = Any.any_l ()
    | & self : t_Expr'0 = self
    | & c : t_Expr'0 = Any.any_l ()
    | & t : t_Expr'0 = Any.any_l ()
    | & e : t_Expr'0 = Any.any_l ()
    | & cp : t_Expr'0 = Any.any_l ()
    | & tp : t_Expr'0 = Any.any_l ()
    | & ep : t_Expr'0 = Any.any_l ()
    | & e1 : t_Expr'0 = Any.any_l () ]
    
    [ return' (result:t_Expr'0)-> {[@expl:normalize ensures] [%#site_normalize0] is_normalized'0 result}
      (! return' {result}) ]

end
module M_ite_normalize__qyi17570407315987535457__simplify [#"ite_normalize.rs" 177 4 177 33] (* Expr *)
  let%span site_normalize0 = "ite_normalize.rs" 175 15 175 35
  let%span site_normalize1 = "ite_normalize.rs" 176 14 176 36
  let%span site_normalize2 = "ite_normalize.rs" 181 15 181 35
  let%span site_normalize3 = "ite_normalize.rs" 182 14 182 105
  let%span site_normalize4 = "ite_normalize.rs" 183 14 183 36
  let%span site_normalize5 = "ite_normalize.rs" 184 14 184 18
  let%span site_normalize6 = "ite_normalize.rs" 123 8 136 9
  let%span site_normalize7 = "ite_normalize.rs" 155 8 161 9
  let%span site_normalize8 = "ite_normalize.rs" 166 8 172 9
  
  use creusot.int.UInt64
  use map.Map
  use creusot.prelude.Any
  
  type t_BTreeMap'0
  
  let rec new'0 (return'  (ret:t_BTreeMap'0))= any [ return' (result:t_BTreeMap'0)-> (! return' {result}) ] 
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  predicate is_normalized'0 [#"ite_normalize.rs" 122 4 122 34] (self : t_Expr'0) =
    [%#site_normalize6] match self with
      | C_IfThenElse'0 c t e -> is_normalized'0 c
      /\ is_normalized'0 t
      /\ is_normalized'0 e
      /\ match c with
        | C_IfThenElse'0 _ _ _ -> false
        | _ -> true
        end
      | C_Var'0 _ -> true
      | C_True'0 -> true
      | C_False'0 -> true
      end
  
  type t_Option'0  =
    | C_None'0
    | C_Some'0 bool
  
  function view'0 [#"ite_normalize.rs" 50 4 50 33] (self : t_BTreeMap'0) : Map.map int t_Option'0
  
  predicate does_not_contain'0 [#"ite_normalize.rs" 165 4 165 48] (self : t_Expr'0) (vp : UInt64.t) =
    [%#site_normalize8] match self with
      | C_IfThenElse'0 c t e -> does_not_contain'0 c vp /\ does_not_contain'0 t vp /\ does_not_contain'0 e vp
      | C_Var'0 v -> v <> vp
      | _ -> true
      end
  
  predicate is_simplified'0 [#"ite_normalize.rs" 154 4 154 34] (self : t_Expr'0) =
    [%#site_normalize7] match self with
      | C_IfThenElse'0 c t e -> match c with
        | C_Var'0 v -> does_not_contain'0 t v /\ does_not_contain'0 e v
        | c -> is_simplified'0 c /\ is_simplified'0 t /\ is_simplified'0 e
        end
      | _ -> true
      end
  
  let rec simplify_helper'0 (self:t_Expr'0) (state:t_BTreeMap'0) (return'  (ret:t_Expr'0))= {[@expl:simplify_helper requires] [%#site_normalize2] is_normalized'0 self}
    any
    [ return' (result:t_Expr'0)-> {[%#site_normalize3] forall i : UInt64.t . (exists v : bool . Map.get (view'0 state) (UInt64.t'int i)
      = C_Some'0 v)  -> does_not_contain'0 result i}
      {[%#site_normalize4] is_simplified'0 result}
      (! return' {result}) ]
  
  
  meta "compute_max_steps" 1000000
  
  let rec simplify'0[#"ite_normalize.rs" 177 4 177 33] (self:t_Expr'0) (return'  (ret:t_Expr'0))= {[@expl:simplify requires] [%#site_normalize0] is_normalized'0 self}
    (! bb0
    [ bb0 = bb1
    | bb1 = s0 [ s0 = new'0 (fun (_ret':t_BTreeMap'0) ->  [ &_5 <- _ret' ] s1) | s1 = bb2 ] 
    | bb2 = s0 [ s0 = simplify_helper'0 {self} {_5} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb3 ] 
    | bb3 = bb4
    | bb4 = return' {_0} ]
    ) [ & _0 : t_Expr'0 = Any.any_l () | & self : t_Expr'0 = self | & _5 : t_BTreeMap'0 = Any.any_l () ] 
    [ return' (result:t_Expr'0)-> {[@expl:simplify ensures] [%#site_normalize1] is_simplified'0 result}
      (! return' {result}) ]

end
module M_ite_normalize__qyi17570407315987535457__simplify_helper [#"ite_normalize.rs" 185 4 185 66] (* Expr *)
  let%span site_normalize0 = "ite_normalize.rs" 195 46 195 50
  let%span site_normalize1 = "ite_normalize.rs" 200 46 200 51
  let%span site_normalize2 = "ite_normalize.rs" 181 15 181 35
  let%span site_normalize3 = "ite_normalize.rs" 182 14 182 105
  let%span site_normalize4 = "ite_normalize.rs" 183 14 183 36
  let%span site_normalize5 = "ite_normalize.rs" 184 14 184 18
  let%span site_normalize6 = "ite_normalize.rs" 17 14 17 68
  let%span site_normalize7 = "ite_normalize.rs" 18 14 18 89
  let%span site_normalize8 = "ite_normalize.rs" 38 14 38 29
  let%span site_normalize9 = "ite_normalize.rs" 27 14 27 123
  let%span site_normalize10 = "ite_normalize.rs" 123 8 136 9
  let%span site_normalize11 = "ite_normalize.rs" 166 8 172 9
  let%span site_normalize12 = "ite_normalize.rs" 155 8 161 9
  let%span smodel13 = "../../creusot-contracts/src/model.rs" 54 8 54 22
  let%span smodel14 = "../../creusot-contracts/src/model.rs" 45 8 45 28
  let%span snum15 = "../../creusot-contracts/src/std/num.rs" 25 28 25 33
  let%span smodel16 = "../../creusot-contracts/src/model.rs" 72 8 72 22
  
  use creusot.int.UInt64
  use map.Map
  use creusot.prelude.MutBorrow
  use creusot.prelude.Any
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  let rec v_Var'0 (input:t_Expr'0) (ret  (v:UInt64.t))= any
    [ good (v:UInt64.t)-> {C_Var'0 v = input} (! ret {v})
    | bad -> {forall v : UInt64.t [C_Var'0 v : t_Expr'0] . C_Var'0 v <> input} (! {false} any) ]
  
  
  type t_BTreeMap'0
  
  type t_Option'0  =
    | C_None'0
    | C_Some'0 bool
  
  type t_Option'1  =
    | C_None'1
    | C_Some'1 bool
  
  function view'0 [#"ite_normalize.rs" 50 4 50 33] (self : t_BTreeMap'0) : Map.map int t_Option'1
  
  function view'1 (self : t_BTreeMap'0) : Map.map int t_Option'1 =
    [%#smodel13] view'0 self
  
  function deep_model'1 (self : UInt64.t) : int =
    [%#snum15] UInt64.t'int self
  
  function deep_model'0 (self : UInt64.t) : int =
    [%#smodel14] deep_model'1 self
  
  let rec get'0 (self:t_BTreeMap'0) (key:UInt64.t) (return'  (ret:t_Option'0))= any
    [ return' (result:t_Option'0)-> {[%#site_normalize6] result = C_None'0
       -> Map.get (view'1 self) (deep_model'0 key) = C_None'1}
      {[%#site_normalize7] forall v : bool . result = C_Some'0 v
       -> Map.get (view'1 self) (deep_model'0 key) = C_Some'1 v}
      (! return' {result}) ]
  
  
  let rec v_Some'0 (input:t_Option'0) (ret  (field_0:bool))= any
    [ good (field_0:bool)-> {C_Some'0 field_0 = input} (! ret {field_0})
    | bad -> {forall field_0 : bool [C_Some'0 field_0 : t_Option'0] . C_Some'0 field_0 <> input} (! {false} any) ]
  
  
  let rec v_IfThenElse'0 (input:t_Expr'0) (ret  (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0))= any
    [ good (c:t_Expr'0) (t:t_Expr'0) (e:t_Expr'0)-> {C_IfThenElse'0 c t e = input} (! ret {c} {t} {e})
    | bad -> {forall c : t_Expr'0, t : t_Expr'0, e : t_Expr'0 [C_IfThenElse'0 c t e : t_Expr'0] . C_IfThenElse'0 c t e
      <> input}
      (! {false}
      any) ]
  
  
  let rec clone'0 (self:t_BTreeMap'0) (return'  (ret:t_BTreeMap'0))= any
    [ return' (result:t_BTreeMap'0)-> {[%#site_normalize8] self = result} (! return' {result}) ]
  
  
  function view'2 (self : MutBorrow.t t_BTreeMap'0) : Map.map int t_Option'1 =
    [%#smodel16] view'0 self.current
  
  let rec insert'0 (self:MutBorrow.t t_BTreeMap'0) (key:UInt64.t) (value:bool) (return'  (ret:t_Option'1))= any
    [ return' (result:t_Option'1)-> {[%#site_normalize9] forall i : int . Map.get (view'0 self.final) i
      = (if i = deep_model'1 key then C_Some'1 value else Map.get (view'2 self) i)}
      (! return' {result}) ]
  
  
  predicate is_normalized'0 [#"ite_normalize.rs" 122 4 122 34] (self : t_Expr'0) =
    [%#site_normalize10] match self with
      | C_IfThenElse'0 c t e -> is_normalized'0 c
      /\ is_normalized'0 t
      /\ is_normalized'0 e
      /\ match c with
        | C_IfThenElse'0 _ _ _ -> false
        | _ -> true
        end
      | C_Var'0 _ -> true
      | C_True'0 -> true
      | C_False'0 -> true
      end
  
  predicate does_not_contain'0 [#"ite_normalize.rs" 165 4 165 48] (self : t_Expr'0) (vp : UInt64.t) =
    [%#site_normalize11] match self with
      | C_IfThenElse'0 c t e -> does_not_contain'0 c vp /\ does_not_contain'0 t vp /\ does_not_contain'0 e vp
      | C_Var'0 v -> v <> vp
      | _ -> true
      end
  
  predicate is_simplified'0 [#"ite_normalize.rs" 154 4 154 34] (self : t_Expr'0) =
    [%#site_normalize12] match self with
      | C_IfThenElse'0 c t e -> match c with
        | C_Var'0 v -> does_not_contain'0 t v /\ does_not_contain'0 e v
        | c -> is_simplified'0 c /\ is_simplified'0 t /\ is_simplified'0 e
        end
      | _ -> true
      end
  
  meta "compute_max_steps" 1000000
  
  let rec simplify_helper'0[#"ite_normalize.rs" 185 4 185 66] (self:t_Expr'0) (state:t_BTreeMap'0) (return'  (ret:t_Expr'0))= {[@expl:simplify_helper requires] [%#site_normalize2] is_normalized'0 self}
    (! bb0
    [ bb0 = bb1
    | bb1 = bb2
    | bb2 = bb3
    | bb3 = any
      [ br0 (x0:t_Expr'0) (x1:t_Expr'0) (x2:t_Expr'0)-> {self = C_IfThenElse'0 x0 x1 x2} (! bb5)
      | br1 (x0:UInt64.t)-> {self = C_Var'0 x0} (! bb6)
      | br2 -> {self = C_True'0} (! bb4)
      | br3 -> {self = C_False'0} (! bb4) ]
    
    | bb4 = s0 [ s0 =  [ &c2 <- self ] s1 | s1 =  [ &_0 <- c2 ] s2 | s2 = bb51 ] 
    | bb51 = bb52
    | bb6 = bb7
    | bb7 = s0
      [ s0 = v_Var'0 {self} (fun (rv'0:UInt64.t) ->  [ &v1 <- rv'0 ] s1)
      | s1 =  [ &_52 <- v1 ] s2
      | s2 = get'0 {state} {_52} (fun (_ret':t_Option'0) ->  [ &_49 <- _ret' ] s3)
      | s3 = bb43 ]
    
    | bb43 = any [ br0 -> {_49 = C_None'0} (! bb49) | br1 (x0:bool)-> {_49 = C_Some'0 x0} (! bb44) ] 
    | bb49 = s0 [ s0 =  [ &_0 <- C_Var'0 v1 ] s1 | s1 = bb50 ] 
    | bb44 = bb45
    | bb45 = s0
      [ s0 = v_Some'0 {_49} (fun (r0'0:bool) ->  [ &b1 <- r0'0 ] s1)
      | s1 = any [ br0 -> {b1 = false} (! bb47) | br1 -> {b1} (! bb46) ]  ]
    
    | bb46 = s0 [ s0 =  [ &_0 <- C_True'0 ] s1 | s1 = bb48 ] 
    | bb47 = s0 [ s0 =  [ &_0 <- C_False'0 ] s1 | s1 = bb48 ] 
    | bb48 = bb50
    | bb50 = bb52
    | bb5 = bb8
    | bb8 = s0
      [ s0 = v_IfThenElse'0 {self} (fun (rc'0:t_Expr'0) (rt'0:t_Expr'0) (re'0:t_Expr'0) ->  [ &c <- rc'0 ] s1)
      | s1 = v_IfThenElse'0 {self} (fun (rc'1:t_Expr'0) (rt'1:t_Expr'0) (re'1:t_Expr'0) ->  [ &t <- rt'1 ] s2)
      | s2 = v_IfThenElse'0 {self} (fun (rc'2:t_Expr'0) (rt'2:t_Expr'0) (re'2:t_Expr'0) ->  [ &e <- re'2 ] s3)
      | s3 = any
        [ br0 (x0:t_Expr'0) (x1:t_Expr'0) (x2:t_Expr'0)-> {c = C_IfThenElse'0 x0 x1 x2} (! bb9)
        | br1 (x0:UInt64.t)-> {c = C_Var'0 x0} (! bb10)
        | br2 -> {c = C_True'0} (! bb9)
        | br3 -> {c = C_False'0} (! bb9) ]
       ]
    
    | bb9 = s0
      [ s0 =  [ &c1 <- c ] s1
      | s1 = simplify_helper'0 {c1} {state} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s2)
      | s2 = bb37 ]
    
    | bb37 = bb38
    | bb38 = bb39
    | bb10 = bb11
    | bb11 = s0
      [ s0 = v_Var'0 {c} (fun (rv'0:UInt64.t) ->  [ &v <- rv'0 ] s1)
      | s1 =  [ &_16 <- v ] s2
      | s2 = get'0 {state} {_16} (fun (_ret':t_Option'0) ->  [ &_13 <- _ret' ] s3)
      | s3 = bb12 ]
    
    | bb12 = any [ br0 -> {_13 = C_None'0} (! bb20) | br1 (x0:bool)-> {_13 = C_Some'0 x0} (! bb13) ] 
    | bb20 = s0 [ s0 = clone'0 {state} (fun (_ret':t_BTreeMap'0) ->  [ &state_t <- _ret' ] s1) | s1 = bb21 ] 
    | bb21 = s0
      [ s0 = MutBorrow.borrow_mut <t_BTreeMap'0> {state_t}
          (fun (_ret':MutBorrow.t t_BTreeMap'0) ->  [ &_27 <- _ret' ]  [ &state_t <- _ret'.final ] s1)
      | s1 = insert'0 {_27} {v} {[%#site_normalize0] true} (fun (_ret':t_Option'1) ->  [ &_26 <- _ret' ] s2)
      | s2 = bb22 ]
    
    | bb22 = s0 [ s0 = simplify_helper'0 {t} {state_t} (fun (_ret':t_Expr'0) ->  [ &tp <- _ret' ] s1) | s1 = bb23 ] 
    | bb23 = s0 [ s0 = clone'0 {state} (fun (_ret':t_BTreeMap'0) ->  [ &state_e <- _ret' ] s1) | s1 = bb24 ] 
    | bb24 = s0
      [ s0 = MutBorrow.borrow_mut <t_BTreeMap'0> {state_e}
          (fun (_ret':MutBorrow.t t_BTreeMap'0) ->  [ &_35 <- _ret' ]  [ &state_e <- _ret'.final ] s1)
      | s1 = insert'0 {_35} {v} {[%#site_normalize1] false} (fun (_ret':t_Option'1) ->  [ &_34 <- _ret' ] s2)
      | s2 = bb25 ]
    
    | bb25 = s0 [ s0 = simplify_helper'0 {e} {state_e} (fun (_ret':t_Expr'0) ->  [ &ep <- _ret' ] s1) | s1 = bb26 ] 
    | bb26 = bb27
    | bb27 = bb28
    | bb28 = s0 [ s0 =  [ &_0 <- C_IfThenElse'0 c tp ep ] s1 | s1 = bb29 ] 
    | bb29 = bb30
    | bb30 = bb31
    | bb31 = bb32
    | bb32 = bb33
    | bb33 = bb34
    | bb34 = bb35
    | bb35 = bb36
    | bb13 = bb14
    | bb14 = s0
      [ s0 = v_Some'0 {_13} (fun (r0'0:bool) ->  [ &b <- r0'0 ] s1)
      | s1 = any [ br0 -> {b = false} (! bb17) | br1 -> {b} (! bb15) ]  ]
    
    | bb15 = s0 [ s0 = simplify_helper'0 {t} {state} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb16 ] 
    | bb16 = bb19
    | bb17 = s0 [ s0 = simplify_helper'0 {e} {state} (fun (_ret':t_Expr'0) ->  [ &_0 <- _ret' ] s1) | s1 = bb18 ] 
    | bb18 = bb19
    | bb19 = bb36
    | bb36 = bb39
    | bb39 = bb40
    | bb40 = bb41
    | bb41 = bb42
    | bb42 = bb52
    | bb52 = bb53
    | bb53 = bb54
    | bb54 = return' {_0} ]
    )
    [ & _0 : t_Expr'0 = Any.any_l ()
    | & self : t_Expr'0 = self
    | & state : t_BTreeMap'0 = state
    | & c : t_Expr'0 = Any.any_l ()
    | & t : t_Expr'0 = Any.any_l ()
    | & e : t_Expr'0 = Any.any_l ()
    | & v : UInt64.t = Any.any_l ()
    | & _13 : t_Option'0 = Any.any_l ()
    | & _16 : UInt64.t = Any.any_l ()
    | & b : bool = Any.any_l ()
    | & state_t : t_BTreeMap'0 = Any.any_l ()
    | & _26 : t_Option'1 = Any.any_l ()
    | & _27 : MutBorrow.t t_BTreeMap'0 = Any.any_l ()
    | & tp : t_Expr'0 = Any.any_l ()
    | & state_e : t_BTreeMap'0 = Any.any_l ()
    | & _34 : t_Option'1 = Any.any_l ()
    | & _35 : MutBorrow.t t_BTreeMap'0 = Any.any_l ()
    | & ep : t_Expr'0 = Any.any_l ()
    | & c1 : t_Expr'0 = Any.any_l ()
    | & v1 : UInt64.t = Any.any_l ()
    | & _49 : t_Option'0 = Any.any_l ()
    | & _52 : UInt64.t = Any.any_l ()
    | & b1 : bool = Any.any_l ()
    | & c2 : t_Expr'0 = Any.any_l () ]
    
    [ return' (result:t_Expr'0)-> {[@expl:simplify_helper ensures #0] [%#site_normalize3] forall i : UInt64.t . (exists v : bool . Map.get (view'0 state) (UInt64.t'int i)
      = C_Some'1 v)  -> does_not_contain'0 result i}
      {[@expl:simplify_helper ensures #1] [%#site_normalize4] is_simplified'0 result}
      (! return' {result}) ]

end
module M_ite_normalize__qyi8160480900349400821__clone__refines [#"ite_normalize.rs" 39 4 39 27] (* <BTreeMap<K, V> as creusot_contracts::Clone> *)
  let%span site_normalize0 = "ite_normalize.rs" 39 4 39 27
  
  type t_BTreeMap'0
  
  goal refines : [%#site_normalize0] forall self : t_BTreeMap'0 . forall result : t_BTreeMap'0 . self = result
   -> result = self
end
module M_ite_normalize__qyi15119799284333837974__clone__refines [#"ite_normalize.rs" 55 9 55 14] (* <Expr as creusot_contracts::Clone> *)
  let%span site_normalize0 = "ite_normalize.rs" 55 9 55 14
  
  use creusot.int.UInt64
  
  type t_Expr'0  =
    | C_IfThenElse'0 t_Expr'0 t_Expr'0 t_Expr'0
    | C_Var'0 UInt64.t
    | C_True'0
    | C_False'0
  
  goal refines : [%#site_normalize0] forall self : t_Expr'0 . forall result : t_Expr'0 . result = self  -> result = self
end