domain Type  {
  
  
}

domain s_Param  {
  
  function typ(arg0: s_Param): Type 
}

domain s_2_Tuple  {
  
  function s_2_Tuple_typeof(arg0: s_2_Tuple): Type 
  
  function s_2_Tuple_cons(arg0: s_Param, arg1: s_Param): s_2_Tuple 
  
  function s_2_Tuple_read_0(arg0: s_2_Tuple): s_Param 
  
  function s_2_Tuple_read_1(arg0: s_2_Tuple): s_Param 
  
  function s_2_Tuple_write_0(arg0: s_2_Tuple, arg1: s_Param): s_2_Tuple 
  
  function s_2_Tuple_write_1(arg0: s_2_Tuple, arg1: s_Param): s_2_Tuple 
  
  axiom s_2_Tuple_ax_typeof {
    (forall s: s_2_Tuple ::
      { s_2_Tuple_typeof(s) }
      s_2_Tuple_typeof(s) ==
      s_2_Tuple_type(s_2_Tuple_typaram_T0(s_2_Tuple_typeof(s)), s_2_Tuple_typaram_T1(s_2_Tuple_typeof(s))))
  }
  
  axiom s_2_Tuple_ax_cons_read_0 {
    (forall f0: s_Param, f1: s_Param ::
      { s_2_Tuple_cons(f0, f1) }
      s_2_Tuple_read_0(s_2_Tuple_cons(f0, f1)) == f0)
  }
  
  axiom s_2_Tuple_ax_type_read_0 {
    (forall s: s_2_Tuple ::
      { s_2_Tuple_read_0(s) }
      typ(s_2_Tuple_read_0(s)) == s_2_Tuple_typaram_T0(s_2_Tuple_typeof(s)))
  }
  
  axiom s_2_Tuple_ax_cons_read_1 {
    (forall f0: s_Param, f1: s_Param ::
      { s_2_Tuple_cons(f0, f1) }
      s_2_Tuple_read_1(s_2_Tuple_cons(f0, f1)) == f1)
  }
  
  axiom s_2_Tuple_ax_type_read_1 {
    (forall s: s_2_Tuple ::
      { s_2_Tuple_read_1(s) }
      typ(s_2_Tuple_read_1(s)) == s_2_Tuple_typaram_T1(s_2_Tuple_typeof(s)))
  }
  
  axiom s_2_Tuple_ax_write_0_read_0 {
    (forall s: s_2_Tuple, value: s_Param ::
      { s_2_Tuple_read_0(s_2_Tuple_write_0(s, value)) }
      s_2_Tuple_read_0(s_2_Tuple_write_0(s, value)) == value)
  }
  
  axiom s_2_Tuple_ax_write_0_read_1 {
    (forall s: s_2_Tuple, value: s_Param ::
      { s_2_Tuple_read_1(s_2_Tuple_write_0(s, value)) }
      s_2_Tuple_read_1(s_2_Tuple_write_0(s, value)) == s_2_Tuple_read_1(s))
  }
  
  axiom s_2_Tuple_ax_write_1_read_0 {
    (forall s: s_2_Tuple, value: s_Param ::
      { s_2_Tuple_read_0(s_2_Tuple_write_1(s, value)) }
      s_2_Tuple_read_0(s_2_Tuple_write_1(s, value)) == s_2_Tuple_read_0(s))
  }
  
  axiom s_2_Tuple_ax_write_1_read_1 {
    (forall s: s_2_Tuple, value: s_Param ::
      { s_2_Tuple_read_1(s_2_Tuple_write_1(s, value)) }
      s_2_Tuple_read_1(s_2_Tuple_write_1(s, value)) == value)
  }
}

domain s_Int_i32  {
  
  function s_Int_i32_typeof(arg0: s_Int_i32): Type 
  
  function s_Int_i32_value(arg0: s_Int_i32): Int 
  
  function s_Int_i32_cons(arg0: Int): s_Int_i32 
  
  axiom s_Int_i32_ax_cons {
    (forall s: s_Int_i32 ::
      { s_Int_i32_value(s) }
      s_Int_i32_cons(s_Int_i32_value(s)) == s)
  }
  
  axiom s_Int_i32_ax_bounds {
    (forall s: s_Int_i32 ::
      { s_Int_i32_value(s) }
      -2147483648 <= s_Int_i32_value(s) && s_Int_i32_value(s) <= 2147483647)
  }
  
  axiom s_Int_i32_ax_value {
    (forall value: Int ::
      { s_Int_i32_cons(value) }
      -2147483648 <= value && value <= 2147483647 ==>
      s_Int_i32_value(s_Int_i32_cons(value)) == value)
  }
}

domain s_UInt_usize  {
  
  function s_UInt_usize_typeof(arg0: s_UInt_usize): Type 
  
  function s_UInt_usize_value(arg0: s_UInt_usize): Int 
  
  function s_UInt_usize_cons(arg0: Int): s_UInt_usize 
  
  axiom s_UInt_usize_ax_cons {
    (forall s: s_UInt_usize ::
      { s_UInt_usize_value(s) }
      s_UInt_usize_cons(s_UInt_usize_value(s)) == s)
  }
  
  axiom s_UInt_usize_ax_bounds {
    (forall s: s_UInt_usize ::
      { s_UInt_usize_value(s) }
      0 <= s_UInt_usize_value(s) &&
      s_UInt_usize_value(s) <= 18446744073709551615)
  }
  
  axiom s_UInt_usize_ax_value {
    (forall value: Int ::
      { s_UInt_usize_cons(value) }
      0 <= value && value <= 18446744073709551615 ==>
      s_UInt_usize_value(s_UInt_usize_cons(value)) == value)
  }
}

domain s_Vector  {
  
  function s_Vector_typeof(arg0: s_Vector): Type 
  
  function s_Vector_cons(arg0: s_UInt_usize, arg1: s_Int_i32): s_Vector 
  
  function s_Vector_read_0(arg0: s_Vector): s_UInt_usize 
  
  function s_Vector_read_1(arg0: s_Vector): s_Int_i32 
  
  function s_Vector_write_0(arg0: s_Vector, arg1: s_UInt_usize): s_Vector 
  
  function s_Vector_write_1(arg0: s_Vector, arg1: s_Int_i32): s_Vector 
  
  axiom s_Vector_ax_typeof {
    (forall s: s_Vector ::
      { s_Vector_typeof(s) }
      s_Vector_typeof(s) == s_Vector_type())
  }
  
  axiom s_Vector_ax_cons_read_0 {
    (forall f0: s_UInt_usize, f1: s_Int_i32 ::
      { s_Vector_cons(f0, f1) }
      s_Vector_read_0(s_Vector_cons(f0, f1)) == f0)
  }
  
  axiom s_Vector_ax_cons_read_1 {
    (forall f0: s_UInt_usize, f1: s_Int_i32 ::
      { s_Vector_cons(f0, f1) }
      s_Vector_read_1(s_Vector_cons(f0, f1)) == f1)
  }
  
  axiom s_Vector_ax_write_0_read_0 {
    (forall s: s_Vector, value: s_UInt_usize ::
      { s_Vector_read_0(s_Vector_write_0(s, value)) }
      s_Vector_read_0(s_Vector_write_0(s, value)) == value)
  }
  
  axiom s_Vector_ax_write_0_read_1 {
    (forall s: s_Vector, value: s_UInt_usize ::
      { s_Vector_read_1(s_Vector_write_0(s, value)) }
      s_Vector_read_1(s_Vector_write_0(s, value)) == s_Vector_read_1(s))
  }
  
  axiom s_Vector_ax_write_1_read_0 {
    (forall s: s_Vector, value: s_Int_i32 ::
      { s_Vector_read_0(s_Vector_write_1(s, value)) }
      s_Vector_read_0(s_Vector_write_1(s, value)) == s_Vector_read_0(s))
  }
  
  axiom s_Vector_ax_write_1_read_1 {
    (forall s: s_Vector, value: s_Int_i32 ::
      { s_Vector_read_1(s_Vector_write_1(s, value)) }
      s_Vector_read_1(s_Vector_write_1(s, value)) == value)
  }
}

domain s_Never  {
  
  function s_Never_typeof(arg0: s_Never): Type 
}

domain s_Bool  {
  
  function s_Bool_typeof(arg0: s_Bool): Type 
  
  function s_Bool_value(arg0: s_Bool): Bool 
  
  function s_Bool_cons(arg0: Bool): s_Bool 
  
  axiom s_Bool_ax_cons {
    (forall s: s_Bool ::
      { s_Bool_value(s) }
      s_Bool_cons(s_Bool_value(s)) == s)
  }
  
  axiom s_Bool_ax_value {
    (forall value: Bool ::
      { s_Bool_cons(value) }
      s_Bool_value(s_Bool_cons(value)) == value)
  }
}

domain s_Ref_immutable  {
  
  function s_Ref_immutable_typeof(arg0: s_Ref_immutable): Type 
  
  function s_Ref_immutable_deref(arg0: s_Ref_immutable): Ref 
  
  function s_Ref_immutable_value(arg0: s_Ref_immutable): s_Param 
  
  function s_Ref_immutable_cons(arg0: Ref, arg1: s_Param): s_Ref_immutable 
  
  axiom s_Ref_immutable_ax_deref {
    (forall r: Ref, value: s_Param ::
      { s_Ref_immutable_cons(r, value) }
      s_Ref_immutable_deref(s_Ref_immutable_cons(r, value)) == r)
  }
  
  axiom s_Ref_immutable_ax_value {
    (forall r: Ref, value: s_Param ::
      { s_Ref_immutable_cons(r, value) }
      s_Ref_immutable_value(s_Ref_immutable_cons(r, value)) == value)
  }
}

domain s_0_Tuple  {
  
  function s_0_Tuple_typeof(arg0: s_0_Tuple): Type 
  
  function s_0_Tuple_cons(): s_0_Tuple 
  
  axiom s_0_Tuple_ax_typeof {
    (forall s: s_0_Tuple ::
      { s_0_Tuple_typeof(s) }
      s_0_Tuple_typeof(s) == s_0_Tuple_type())
  }
}

domain s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0  {
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_typeof(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0): Type 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(arg0: s_Vector,
  arg1: s_Ref_immutable, arg2: s_Vector): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0): s_Vector 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0): s_Vector 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
  arg1: s_Vector): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0 
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(arg0: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
  arg1: s_Vector): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0 
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_typeof {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0 ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_typeof(s) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_typeof(s) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_type())
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_cons_read_0 {
    (forall f0: s_Vector, f1: s_Ref_immutable, f2: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2)) ==
      f0)
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_cons_read_1 {
    (forall f0: s_Vector, f1: s_Ref_immutable, f2: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2)) ==
      f1)
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_cons_read_2 {
    (forall f0: s_Vector, f1: s_Ref_immutable, f2: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(f0,
      f1, f2)) ==
      f2)
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_0_read_0 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_0_read_1 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_0_read_2 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_1_read_0 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_1_read_1 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_1_read_2 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_2_read_0 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_2_read_1 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ax_write_2_read_2 {
    (forall s: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_write_2(s,
      value)) ==
      value)
  }
}

domain s_Int_isize  {
  
  function s_Int_isize_typeof(arg0: s_Int_isize): Type 
  
  function s_Int_isize_value(arg0: s_Int_isize): Int 
  
  function s_Int_isize_cons(arg0: Int): s_Int_isize 
  
  axiom s_Int_isize_ax_cons {
    (forall s: s_Int_isize ::
      { s_Int_isize_value(s) }
      s_Int_isize_cons(s_Int_isize_value(s)) == s)
  }
  
  axiom s_Int_isize_ax_bounds {
    (forall s: s_Int_isize ::
      { s_Int_isize_value(s) }
      -9223372036854775808 <= s_Int_isize_value(s) &&
      s_Int_isize_value(s) <= 9223372036854775807)
  }
  
  axiom s_Int_isize_ax_value {
    (forall value: Int ::
      { s_Int_isize_cons(value) }
      -9223372036854775808 <= value && value <= 9223372036854775807 ==>
      s_Int_isize_value(s_Int_isize_cons(value)) == value)
  }
}

domain s_FallibleVec  {
  
  function s_FallibleVec_typeof(arg0: s_FallibleVec): Type 
  
  function s_FallibleVec_discr(arg0: s_FallibleVec): s_Int_isize 
  
  function s_FallibleVec_0_cons(arg0: s_Vector): s_FallibleVec 
  
  function s_FallibleVec_0_read_0(arg0: s_FallibleVec): s_Vector 
  
  function s_FallibleVec_0_write_0(arg0: s_FallibleVec, arg1: s_Vector): s_FallibleVec 
  
  function s_FallibleVec_1_cons(): s_FallibleVec 
  
  axiom s_FallibleVec_ax_0_cons_read_0 {
    (forall f0: s_Vector ::
      { s_FallibleVec_0_cons(f0) }
      s_FallibleVec_0_read_0(s_FallibleVec_0_cons(f0)) == f0)
  }
  
  axiom s_FallibleVec_ax_0_write_0_read_0 {
    (forall s: s_FallibleVec, value: s_Vector ::
      { s_FallibleVec_0_read_0(s_FallibleVec_0_write_0(s, value)) }
      s_FallibleVec_0_read_0(s_FallibleVec_0_write_0(s, value)) == value)
  }
  
  axiom s_FallibleVec_ax_0_cons_discr {
    (forall f0: s_Vector ::
      { s_FallibleVec_0_cons(f0) }
      s_FallibleVec_discr(s_FallibleVec_0_cons(f0)) == s_Int_isize_cons(0))
  }
  
  axiom s_FallibleVec_ax_1_cons_discr {
    s_FallibleVec_discr(s_FallibleVec_1_cons()) == s_Int_isize_cons(1)
  }
  
  axiom s_FallibleVec_ax_discr_values {
    (forall s: s_FallibleVec ::
      { s_FallibleVec_discr(s) }
      s_FallibleVec_discr(s) == s_Int_isize_cons(0) ||
      s_FallibleVec_discr(s) == s_Int_isize_cons(1))
  }
}

domain s_Bounds  {
  
  function s_Bounds_typeof(arg0: s_Bounds): Type 
  
  function s_Bounds_cons(arg0: s_Int_i32, arg1: s_Int_i32): s_Bounds 
  
  function s_Bounds_read_0(arg0: s_Bounds): s_Int_i32 
  
  function s_Bounds_read_1(arg0: s_Bounds): s_Int_i32 
  
  function s_Bounds_write_0(arg0: s_Bounds, arg1: s_Int_i32): s_Bounds 
  
  function s_Bounds_write_1(arg0: s_Bounds, arg1: s_Int_i32): s_Bounds 
  
  axiom s_Bounds_ax_typeof {
    (forall s: s_Bounds ::
      { s_Bounds_typeof(s) }
      s_Bounds_typeof(s) == s_Bounds_type())
  }
  
  axiom s_Bounds_ax_cons_read_0 {
    (forall f0: s_Int_i32, f1: s_Int_i32 ::
      { s_Bounds_cons(f0, f1) }
      s_Bounds_read_0(s_Bounds_cons(f0, f1)) == f0)
  }
  
  axiom s_Bounds_ax_cons_read_1 {
    (forall f0: s_Int_i32, f1: s_Int_i32 ::
      { s_Bounds_cons(f0, f1) }
      s_Bounds_read_1(s_Bounds_cons(f0, f1)) == f1)
  }
  
  axiom s_Bounds_ax_write_0_read_0 {
    (forall s: s_Bounds, value: s_Int_i32 ::
      { s_Bounds_read_0(s_Bounds_write_0(s, value)) }
      s_Bounds_read_0(s_Bounds_write_0(s, value)) == value)
  }
  
  axiom s_Bounds_ax_write_0_read_1 {
    (forall s: s_Bounds, value: s_Int_i32 ::
      { s_Bounds_read_1(s_Bounds_write_0(s, value)) }
      s_Bounds_read_1(s_Bounds_write_0(s, value)) == s_Bounds_read_1(s))
  }
  
  axiom s_Bounds_ax_write_1_read_0 {
    (forall s: s_Bounds, value: s_Int_i32 ::
      { s_Bounds_read_0(s_Bounds_write_1(s, value)) }
      s_Bounds_read_0(s_Bounds_write_1(s, value)) == s_Bounds_read_0(s))
  }
  
  axiom s_Bounds_ax_write_1_read_1 {
    (forall s: s_Bounds, value: s_Int_i32 ::
      { s_Bounds_read_1(s_Bounds_write_1(s, value)) }
      s_Bounds_read_1(s_Bounds_write_1(s, value)) == value)
  }
}

domain s_ClampTransform  {
  
  function s_ClampTransform_typeof(arg0: s_ClampTransform): Type 
  
  function s_ClampTransform_cons(arg0: s_Bounds): s_ClampTransform 
  
  function s_ClampTransform_read_0(arg0: s_ClampTransform): s_Bounds 
  
  function s_ClampTransform_write_0(arg0: s_ClampTransform, arg1: s_Bounds): s_ClampTransform 
  
  axiom s_ClampTransform_ax_typeof {
    (forall s: s_ClampTransform ::
      { s_ClampTransform_typeof(s) }
      s_ClampTransform_typeof(s) == s_ClampTransform_type())
  }
  
  axiom s_ClampTransform_ax_cons_read_0 {
    (forall f0: s_Bounds ::
      { s_ClampTransform_cons(f0) }
      s_ClampTransform_read_0(s_ClampTransform_cons(f0)) == f0)
  }
  
  axiom s_ClampTransform_ax_write_0_read_0 {
    (forall s: s_ClampTransform, value: s_Bounds ::
      { s_ClampTransform_read_0(s_ClampTransform_write_0(s, value)) }
      s_ClampTransform_read_0(s_ClampTransform_write_0(s, value)) == value)
  }
}

domain s_Output  {
  
  function s_Output_typeof(arg0: s_Output): Type 
  
  function s_Output_cons(arg0: s_FallibleVec, arg1: s_ClampTransform): s_Output 
  
  function s_Output_read_0(arg0: s_Output): s_FallibleVec 
  
  function s_Output_read_1(arg0: s_Output): s_ClampTransform 
  
  function s_Output_write_0(arg0: s_Output, arg1: s_FallibleVec): s_Output 
  
  function s_Output_write_1(arg0: s_Output, arg1: s_ClampTransform): s_Output 
  
  axiom s_Output_ax_typeof {
    (forall s: s_Output ::
      { s_Output_typeof(s) }
      s_Output_typeof(s) == s_Output_type())
  }
  
  axiom s_Output_ax_cons_read_0 {
    (forall f0: s_FallibleVec, f1: s_ClampTransform ::
      { s_Output_cons(f0, f1) }
      s_Output_read_0(s_Output_cons(f0, f1)) == f0)
  }
  
  axiom s_Output_ax_cons_read_1 {
    (forall f0: s_FallibleVec, f1: s_ClampTransform ::
      { s_Output_cons(f0, f1) }
      s_Output_read_1(s_Output_cons(f0, f1)) == f1)
  }
  
  axiom s_Output_ax_write_0_read_0 {
    (forall s: s_Output, value: s_FallibleVec ::
      { s_Output_read_0(s_Output_write_0(s, value)) }
      s_Output_read_0(s_Output_write_0(s, value)) == value)
  }
  
  axiom s_Output_ax_write_0_read_1 {
    (forall s: s_Output, value: s_FallibleVec ::
      { s_Output_read_1(s_Output_write_0(s, value)) }
      s_Output_read_1(s_Output_write_0(s, value)) == s_Output_read_1(s))
  }
  
  axiom s_Output_ax_write_1_read_0 {
    (forall s: s_Output, value: s_ClampTransform ::
      { s_Output_read_0(s_Output_write_1(s, value)) }
      s_Output_read_0(s_Output_write_1(s, value)) == s_Output_read_0(s))
  }
  
  axiom s_Output_ax_write_1_read_1 {
    (forall s: s_Output, value: s_ClampTransform ::
      { s_Output_read_1(s_Output_write_1(s, value)) }
      s_Output_read_1(s_Output_write_1(s, value)) == value)
  }
}

domain s_FallibleI32  {
  
  function s_FallibleI32_typeof(arg0: s_FallibleI32): Type 
  
  function s_FallibleI32_discr(arg0: s_FallibleI32): s_Int_isize 
  
  function s_FallibleI32_0_cons(arg0: s_Int_i32): s_FallibleI32 
  
  function s_FallibleI32_0_read_0(arg0: s_FallibleI32): s_Int_i32 
  
  function s_FallibleI32_0_write_0(arg0: s_FallibleI32, arg1: s_Int_i32): s_FallibleI32 
  
  function s_FallibleI32_1_cons(): s_FallibleI32 
  
  axiom s_FallibleI32_ax_0_cons_read_0 {
    (forall f0: s_Int_i32 ::
      { s_FallibleI32_0_cons(f0) }
      s_FallibleI32_0_read_0(s_FallibleI32_0_cons(f0)) == f0)
  }
  
  axiom s_FallibleI32_ax_0_write_0_read_0 {
    (forall s: s_FallibleI32, value: s_Int_i32 ::
      { s_FallibleI32_0_read_0(s_FallibleI32_0_write_0(s, value)) }
      s_FallibleI32_0_read_0(s_FallibleI32_0_write_0(s, value)) == value)
  }
  
  axiom s_FallibleI32_ax_0_cons_discr {
    (forall f0: s_Int_i32 ::
      { s_FallibleI32_0_cons(f0) }
      s_FallibleI32_discr(s_FallibleI32_0_cons(f0)) == s_Int_isize_cons(0))
  }
  
  axiom s_FallibleI32_ax_1_cons_discr {
    s_FallibleI32_discr(s_FallibleI32_1_cons()) == s_Int_isize_cons(1)
  }
  
  axiom s_FallibleI32_ax_discr_values {
    (forall s: s_FallibleI32 ::
      { s_FallibleI32_discr(s) }
      s_FallibleI32_discr(s) == s_Int_isize_cons(0) ||
      s_FallibleI32_discr(s) == s_Int_isize_cons(1))
  }
}

domain s_ImpureOutput  {
  
  function s_ImpureOutput_typeof(arg0: s_ImpureOutput): Type 
  
  function s_ImpureOutput_cons(arg0: s_FallibleI32, arg1: s_ClampTransform): s_ImpureOutput 
  
  function s_ImpureOutput_read_0(arg0: s_ImpureOutput): s_FallibleI32 
  
  function s_ImpureOutput_read_1(arg0: s_ImpureOutput): s_ClampTransform 
  
  function s_ImpureOutput_write_0(arg0: s_ImpureOutput, arg1: s_FallibleI32): s_ImpureOutput 
  
  function s_ImpureOutput_write_1(arg0: s_ImpureOutput, arg1: s_ClampTransform): s_ImpureOutput 
  
  axiom s_ImpureOutput_ax_typeof {
    (forall s: s_ImpureOutput ::
      { s_ImpureOutput_typeof(s) }
      s_ImpureOutput_typeof(s) == s_ImpureOutput_type())
  }
  
  axiom s_ImpureOutput_ax_cons_read_0 {
    (forall f0: s_FallibleI32, f1: s_ClampTransform ::
      { s_ImpureOutput_cons(f0, f1) }
      s_ImpureOutput_read_0(s_ImpureOutput_cons(f0, f1)) == f0)
  }
  
  axiom s_ImpureOutput_ax_cons_read_1 {
    (forall f0: s_FallibleI32, f1: s_ClampTransform ::
      { s_ImpureOutput_cons(f0, f1) }
      s_ImpureOutput_read_1(s_ImpureOutput_cons(f0, f1)) == f1)
  }
  
  axiom s_ImpureOutput_ax_write_0_read_0 {
    (forall s: s_ImpureOutput, value: s_FallibleI32 ::
      { s_ImpureOutput_read_0(s_ImpureOutput_write_0(s, value)) }
      s_ImpureOutput_read_0(s_ImpureOutput_write_0(s, value)) == value)
  }
  
  axiom s_ImpureOutput_ax_write_0_read_1 {
    (forall s: s_ImpureOutput, value: s_FallibleI32 ::
      { s_ImpureOutput_read_1(s_ImpureOutput_write_0(s, value)) }
      s_ImpureOutput_read_1(s_ImpureOutput_write_0(s, value)) ==
      s_ImpureOutput_read_1(s))
  }
  
  axiom s_ImpureOutput_ax_write_1_read_0 {
    (forall s: s_ImpureOutput, value: s_ClampTransform ::
      { s_ImpureOutput_read_0(s_ImpureOutput_write_1(s, value)) }
      s_ImpureOutput_read_0(s_ImpureOutput_write_1(s, value)) ==
      s_ImpureOutput_read_0(s))
  }
  
  axiom s_ImpureOutput_ax_write_1_read_1 {
    (forall s: s_ImpureOutput, value: s_ClampTransform ::
      { s_ImpureOutput_read_1(s_ImpureOutput_write_1(s, value)) }
      s_ImpureOutput_read_1(s_ImpureOutput_write_1(s, value)) == value)
  }
}

domain s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0  {
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_typeof(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0): Type 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(arg0: s_Ref_immutable,
  arg1: s_Vector, arg2: s_FallibleVec): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0): s_Vector 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0): s_FallibleVec 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
  arg1: s_Vector): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(arg0: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
  arg1: s_FallibleVec): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0 
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_typeof {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0 ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_typeof(s) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_typeof(s) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_type())
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_cons_read_0 {
    (forall f0: s_Ref_immutable, f1: s_Vector, f2: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2)) ==
      f0)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_cons_read_1 {
    (forall f0: s_Ref_immutable, f1: s_Vector, f2: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2)) ==
      f1)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_cons_read_2 {
    (forall f0: s_Ref_immutable, f1: s_Vector, f2: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(f0,
      f1, f2)) ==
      f2)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_0_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_0_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_0_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_1_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_1_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_1_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_2_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_2_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ax_write_2_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_write_2(s,
      value)) ==
      value)
  }
}

domain s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0  {
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_typeof(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): Type 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(arg0: s_Ref_immutable,
  arg1: s_FallibleVec, arg2: s_ClampTransform, arg3: s_Vector): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): s_FallibleVec 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): s_ClampTransform 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): s_Vector 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
  arg1: s_FallibleVec): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
  arg1: s_ClampTransform): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(arg0: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
  arg1: s_Vector): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_typeof {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0 ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_typeof(s) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_typeof(s) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_type())
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_cons_read_0 {
    (forall f0: s_Ref_immutable, f1: s_FallibleVec, f2: s_ClampTransform, f3: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f0)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_cons_read_1 {
    (forall f0: s_Ref_immutable, f1: s_FallibleVec, f2: s_ClampTransform, f3: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f1)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_cons_read_2 {
    (forall f0: s_Ref_immutable, f1: s_FallibleVec, f2: s_ClampTransform, f3: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f2)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_cons_read_3 {
    (forall f0: s_Ref_immutable, f1: s_FallibleVec, f2: s_ClampTransform, f3: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f3)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_0_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_0_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_0_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_0_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_1_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_1_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_1_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_1_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_2_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_ClampTransform ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_2_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_ClampTransform ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_2_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_ClampTransform ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_2_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_ClampTransform ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_3_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_3_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_3_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ax_write_3_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0,
    value: s_Vector ::
      { s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_write_3(s,
      value)) ==
      value)
  }
}

domain s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0  {
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_typeof(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): Type 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(arg0: s_FallibleVec,
  arg1: s_Ref_immutable, arg2: s_Ref_immutable, arg3: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): s_FallibleVec 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): s_Ref_immutable 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
  arg1: s_FallibleVec): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(arg0: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
  arg1: s_Ref_immutable): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_typeof {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0 ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_typeof(s) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_typeof(s) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_type())
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_cons_read_0 {
    (forall f0: s_FallibleVec, f1: s_Ref_immutable, f2: s_Ref_immutable, f3: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f0)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_cons_read_1 {
    (forall f0: s_FallibleVec, f1: s_Ref_immutable, f2: s_Ref_immutable, f3: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f1)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_cons_read_2 {
    (forall f0: s_FallibleVec, f1: s_Ref_immutable, f2: s_Ref_immutable, f3: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f2)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_cons_read_3 {
    (forall f0: s_FallibleVec, f1: s_Ref_immutable, f2: s_Ref_immutable, f3: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(f0,
      f1, f2, f3)) ==
      f3)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_0_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_0_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_0_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_0_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_FallibleVec ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_0(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_1_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_1_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_1_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_1_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_1(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_2_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_2_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_2_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) ==
      value)
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_2_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_2(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_3_read_0 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_3_read_1 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_3_read_2 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) ==
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(s))
  }
  
  axiom s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ax_write_3_read_3 {
    (forall s: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0,
    value: s_Ref_immutable ::
      { s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) }
      s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_write_3(s,
      value)) ==
      value)
  }
}

domain s_2_Tuple_ty_constructor  {
  
  function s_2_Tuple_type(arg0: Type, arg1: Type): Type 
  
  function s_2_Tuple_typaram_T0(arg0: Type): Type 
  
  function s_2_Tuple_typaram_T1(arg0: Type): Type 
  
  axiom ax_s_2_Tuple_typaram_T0 {
    (forall arg_0: Type, arg_1: Type ::
      { s_2_Tuple_type(arg_0, arg_1) }
      s_2_Tuple_typaram_T0(s_2_Tuple_type(arg_0, arg_1)) == arg_0)
  }
  
  axiom ax_s_2_Tuple_typaram_T1 {
    (forall arg_0: Type, arg_1: Type ::
      { s_2_Tuple_type(arg_0, arg_1) }
      s_2_Tuple_typaram_T1(s_2_Tuple_type(arg_0, arg_1)) == arg_1)
  }
}

domain s_Int_i32_ty_constructor  {
  
  function s_Int_i32_type(): Type 
}

domain s_Vector_ty_constructor  {
  
  function s_Vector_type(): Type 
}

domain s_UInt_usize_ty_constructor  {
  
  function s_UInt_usize_type(): Type 
}

domain s_Never_ty_constructor  {
  
  function s_Never_type(): Type 
}

domain s_Bool_ty_constructor  {
  
  function s_Bool_type(): Type 
}

domain s_Ref_immutable_ty_constructor  {
  
  function s_Ref_immutable_type(arg0: Type): Type 
  
  function s_Ref_immutable_typaram_T(arg0: Type): Type 
  
  axiom ax_s_Ref_immutable_typaram_T {
    (forall arg_0: Type ::
      { s_Ref_immutable_type(arg_0) }
      s_Ref_immutable_typaram_T(s_Ref_immutable_type(arg_0)) == arg_0)
  }
}

domain s_0_Tuple_ty_constructor  {
  
  function s_0_Tuple_type(): Type 
}

domain s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_ty_constructor  {
  
  function s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_type(): Type 
}

domain s_Output_ty_constructor  {
  
  function s_Output_type(): Type 
}

domain s_FallibleVec_ty_constructor  {
  
  function s_FallibleVec_type(): Type 
}

domain s_Int_isize_ty_constructor  {
  
  function s_Int_isize_type(): Type 
}

domain s_ClampTransform_ty_constructor  {
  
  function s_ClampTransform_type(): Type 
}

domain s_Bounds_ty_constructor  {
  
  function s_Bounds_type(): Type 
}

domain s_ImpureOutput_ty_constructor  {
  
  function s_ImpureOutput_type(): Type 
}

domain s_FallibleI32_ty_constructor  {
  
  function s_FallibleI32_type(): Type 
}

domain s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_ty_constructor  {
  
  function s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_type(): Type 
}

domain s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_ty_constructor  {
  
  function s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_type(): Type 
}

domain s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_ty_constructor  {
  
  function s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_type(): Type 
}

field p_Int_i32_val: s_Int_i32

field p_UInt_usize_val: s_UInt_usize

field p_Bool_val: s_Bool

field p_Ref_immutable_val: s_Ref_immutable

field p_Int_isize_val: s_Int_isize

function f_Vector$colon$$colon$get(_1p: s_Vector, _2p: s_UInt_usize): s_Int_i32
  requires s_Bool_value(mir_binop_Lt_usize_usize(_2p, s_Vector_read_0(_1p)))


function f_unreachable_vec(): s_Vector
  requires s_Bool_value(s_Bool_cons(false))


function f_FallibleVec$colon$$colon$unwrap_vec(_1p: s_FallibleVec): s_Vector
  requires s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(_1p)) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false)))))
{
  make_concrete_s_Vector(make_generic_s_Vector((s_Int_isize_value(s_FallibleVec_discr(_1p)) ==
  1 ?
    f_unreachable_vec() :
    (s_Int_isize_value(s_FallibleVec_discr(_1p)) == 0 ?
      s_FallibleVec_0_read_0(_1p) :
      p_Vector_unreachable()))))
}

function f_ClampTransform$colon$$colon$do_transform(_1p: s_ClampTransform, _2p: s_Int_i32): s_Int_i32
  requires s_Bool_value(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(_1p)),
    s_Bounds_read_0(s_ClampTransform_read_0(_1p))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ge_i32_i32(result,
    s_Bounds_read_1(s_ClampTransform_read_0(_1p)))) ?
      s_Bool_cons(false) :
      mir_binop_Le_i32_i32(result, s_Bounds_read_0(s_ClampTransform_read_0(_1p)))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Lt_i32_i32(_2p,
    s_Bounds_read_1(s_ClampTransform_read_0(_1p)))) ?
      s_Bool_cons(true) :
      mir_binop_Eq_i32_i32(result, s_Bounds_read_1(s_ClampTransform_read_0(_1p)))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Gt_i32_i32(_2p,
    s_Bounds_read_0(s_ClampTransform_read_0(_1p)))) ?
      s_Bool_cons(true) :
      mir_binop_Eq_i32_i32(result, s_Bounds_read_0(s_ClampTransform_read_0(_1p)))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ge_i32_i32(_2p,
    s_Bounds_read_1(s_ClampTransform_read_0(_1p)))) ?
      s_Bool_cons(true) :
      make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_i32_i32(_2p,
      s_Bounds_read_0(s_ClampTransform_read_0(_1p)))) ?
        s_Bool_cons(true) :
        mir_binop_Eq_i32_i32(result, _2p))))))))
{
  make_concrete_s_Int_i32(make_generic_s_Int_i32((!s_Bool_value(mir_binop_Lt_i32_i32(_2p,
  s_Bounds_read_1(s_ClampTransform_read_0(_1p)))) ?
    make_concrete_s_Int_i32(make_generic_s_Int_i32((!s_Bool_value(mir_binop_Gt_i32_i32(_2p,
    s_Bounds_read_0(s_ClampTransform_read_0(_1p)))) ?
      _2p :
      s_Bounds_read_0(s_ClampTransform_read_0(_1p))))) :
    s_Bounds_read_1(s_ClampTransform_read_0(_1p)))))
}

function f_unreachable_i32(): s_Int_i32
  requires s_Bool_value(s_Bool_cons(false))


function f_FallibleI32$colon$$colon$unwrap_i32(_1p: s_FallibleI32): s_Int_i32
  requires s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleI32_discr(_1p)) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false)))))
{
  make_concrete_s_Int_i32(make_generic_s_Int_i32((s_Int_isize_value(s_FallibleI32_discr(_1p)) ==
  1 ?
    f_unreachable_i32() :
    (s_Int_isize_value(s_FallibleI32_discr(_1p)) == 0 ?
      s_FallibleI32_0_read_0(_1p) :
      p_Int_i32_unreachable()))))
}

function mir_binop_Lt_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) < s_UInt_usize_value(arg2))
}

function mir_binop_Eq_i32_i32(arg1: s_Int_i32, arg2: s_Int_i32): s_Bool
{
  s_Bool_cons(s_Int_i32_value(arg1) == s_Int_i32_value(arg2))
}

function mir_binop_Eq_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) == s_UInt_usize_value(arg2))
}

function mir_binop_Ne_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) != s_UInt_usize_value(arg2))
}

function mir_binop_Ge_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) >= s_UInt_usize_value(arg2))
}

function mir_binop_Le_i32_i32(arg1: s_Int_i32, arg2: s_Int_i32): s_Bool
{
  s_Bool_cons(s_Int_i32_value(arg1) <= s_Int_i32_value(arg2))
}

function mir_binop_Eq_bool_bool(arg1: s_Bool, arg2: s_Bool): s_Bool
{
  s_Bool_cons(s_Bool_value(arg1) == s_Bool_value(arg2))
}

function mir_binop_Gt_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) > s_UInt_usize_value(arg2))
}

function mir_binop_Le_usize_usize(arg1: s_UInt_usize, arg2: s_UInt_usize): s_Bool
{
  s_Bool_cons(s_UInt_usize_value(arg1) <= s_UInt_usize_value(arg2))
}

function mir_binop_Ge_i32_i32(arg1: s_Int_i32, arg2: s_Int_i32): s_Bool
{
  s_Bool_cons(s_Int_i32_value(arg1) >= s_Int_i32_value(arg2))
}

function mir_binop_Lt_i32_i32(arg1: s_Int_i32, arg2: s_Int_i32): s_Bool
{
  s_Bool_cons(s_Int_i32_value(arg1) < s_Int_i32_value(arg2))
}

function mir_binop_Gt_i32_i32(arg1: s_Int_i32, arg2: s_Int_i32): s_Bool
{
  s_Bool_cons(s_Int_i32_value(arg1) > s_Int_i32_value(arg2))
}

function make_generic_s_Int_i32(self: s_Int_i32): s_Param
  ensures typ(result) == s_Int_i32_type()
  ensures make_concrete_s_Int_i32(result) == self


function make_concrete_s_Int_i32(snap: s_Param): s_Int_i32
  requires typ(snap) == s_Int_i32_type()
  ensures make_generic_s_Int_i32(result) == snap


function make_generic_s_Vector(self: s_Vector): s_Param
  ensures typ(result) == s_Vector_type()
  ensures make_concrete_s_Vector(result) == self


function make_concrete_s_Vector(snap: s_Param): s_Vector
  requires typ(snap) == s_Vector_type()
  ensures make_generic_s_Vector(result) == snap


function make_generic_s_UInt_usize(self: s_UInt_usize): s_Param
  ensures typ(result) == s_UInt_usize_type()
  ensures make_concrete_s_UInt_usize(result) == self


function make_concrete_s_UInt_usize(snap: s_Param): s_UInt_usize
  requires typ(snap) == s_UInt_usize_type()
  ensures make_generic_s_UInt_usize(result) == snap


function make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(self: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0): s_Param
  ensures typ(result) ==
    s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_type()
  ensures make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(result) ==
    self


function make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(snap: s_Param): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0
  requires typ(snap) ==
    s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_type()
  ensures make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(result) ==
    snap


function make_generic_s_0_Tuple(self: s_0_Tuple): s_Param
  ensures typ(result) == s_0_Tuple_type()
  ensures make_concrete_s_0_Tuple(result) == self


function make_concrete_s_0_Tuple(snap: s_Param): s_0_Tuple
  requires typ(snap) == s_0_Tuple_type()
  ensures make_generic_s_0_Tuple(result) == snap


function make_generic_s_Bool(self: s_Bool): s_Param
  ensures typ(result) == s_Bool_type()
  ensures make_concrete_s_Bool(result) == self


function make_concrete_s_Bool(snap: s_Param): s_Bool
  requires typ(snap) == s_Bool_type()
  ensures make_generic_s_Bool(result) == snap


function make_generic_s_ClampTransform(self: s_ClampTransform): s_Param
  ensures typ(result) == s_ClampTransform_type()
  ensures make_concrete_s_ClampTransform(result) == self


function make_concrete_s_ClampTransform(snap: s_Param): s_ClampTransform
  requires typ(snap) == s_ClampTransform_type()
  ensures make_generic_s_ClampTransform(result) == snap


function make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(self: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0): s_Param
  ensures typ(result) ==
    s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_type()
  ensures make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(result) ==
    self


function make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(snap: s_Param): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0
  requires typ(snap) ==
    s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_type()
  ensures make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(result) ==
    snap


function make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(self: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0): s_Param
  ensures typ(result) ==
    s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_type()
  ensures make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(result) ==
    self


function make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(snap: s_Param): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0
  requires typ(snap) ==
    s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_type()
  ensures make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(result) ==
    snap


function make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(self: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0): s_Param
  ensures typ(result) ==
    s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_type()
  ensures make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(result) ==
    self


function make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(snap: s_Param): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0
  requires typ(snap) ==
    s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_type()
  ensures make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(result) ==
    snap


function make_generic_s_Bounds(self: s_Bounds): s_Param
  ensures typ(result) == s_Bounds_type()
  ensures make_concrete_s_Bounds(result) == self


function make_concrete_s_Bounds(snap: s_Param): s_Bounds
  requires typ(snap) == s_Bounds_type()
  ensures make_generic_s_Bounds(result) == snap


function p_Param_unreachable(): s_Param
  requires false
  ensures false


function p_Param_snap(self: Ref, t: Type): s_Param
  requires acc(p_Param(self, t), wildcard)
  ensures typ(result) == t


function p_2_Tuple_field_0(self: Ref, T0: Type, T1: Type): Ref
  ensures (self == null) == (result == null)


function p_2_Tuple_field_1(self: Ref, T0: Type, T1: Type): Ref
  ensures (self == null) == (result == null)


function p_2_Tuple_unreachable(): s_2_Tuple
  requires false
  ensures false


function p_2_Tuple_snap(self: Ref, T0: Type, T1: Type): s_2_Tuple
  requires acc(p_2_Tuple(self, T0, T1), wildcard)
{
  (unfolding acc(p_2_Tuple(self, T0, T1), wildcard) in
    s_2_Tuple_cons(p_Param_snap(p_2_Tuple_field_0(self, T0, T1), T0), p_Param_snap(p_2_Tuple_field_1(self,
    T0, T1), T1)))
}

function p_Int_i32_unreachable(): s_Int_i32
  requires false
  ensures false


function p_Int_i32_snap(self: Ref): s_Int_i32
  requires acc(p_Int_i32(self), wildcard)
{
  (unfolding acc(p_Int_i32(self), wildcard) in self.p_Int_i32_val)
}

function p_UInt_usize_unreachable(): s_UInt_usize
  requires false
  ensures false


function p_UInt_usize_snap(self: Ref): s_UInt_usize
  requires acc(p_UInt_usize(self), wildcard)
{
  (unfolding acc(p_UInt_usize(self), wildcard) in self.p_UInt_usize_val)
}

function p_Vector_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Vector_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Vector_unreachable(): s_Vector
  requires false
  ensures false


function p_Vector_snap(self: Ref): s_Vector
  requires acc(p_Vector(self), wildcard)
{
  (unfolding acc(p_Vector(self), wildcard) in
    s_Vector_cons(p_UInt_usize_snap(p_Vector_field_0(self)), p_Int_i32_snap(p_Vector_field_1(self))))
}

function p_Never_unreachable(): s_Never
  requires false
  ensures false


function p_Never_snap(self: Ref): s_Never


function p_Bool_unreachable(): s_Bool
  requires false
  ensures false


function p_Bool_snap(self: Ref): s_Bool
  requires acc(p_Bool(self), wildcard)
{
  (unfolding acc(p_Bool(self), wildcard) in self.p_Bool_val)
}

function p_0_Tuple_unreachable(): s_0_Tuple
  requires false
  ensures false


function p_0_Tuple_snap(self: Ref): s_0_Tuple
  requires acc(p_0_Tuple(self), wildcard)
{
  (unfolding acc(p_0_Tuple(self), wildcard) in s_0_Tuple_cons())
}

function p_Ref_immutable_deref(self: Ref, T: Type): Ref
  requires acc(p_Ref_immutable(self, T), wildcard)
{
  (unfolding acc(p_Ref_immutable(self, T), wildcard) in
    s_Ref_immutable_deref(self.p_Ref_immutable_val))
}

function p_Ref_immutable_unreachable(): s_Ref_immutable
  requires false
  ensures false


function p_Ref_immutable_snap(self: Ref, T: Type): s_Ref_immutable
  requires acc(p_Ref_immutable(self, T), wildcard)
  ensures typ(s_Ref_immutable_value(result)) == T
{
  (unfolding acc(p_Ref_immutable(self, T), wildcard) in
    self.p_Ref_immutable_val)
}

function p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_2(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_unreachable(): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0
  requires false
  ensures false


function p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_snap(self: Ref): s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0
  requires acc(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(self), wildcard)
{
  (unfolding acc(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(self), wildcard) in
    s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(p_Vector_snap(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_0(self)),
    p_Ref_immutable_snap(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_1(self),
    s_UInt_usize_type()), p_Vector_snap(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_2(self))))
}

function p_Int_isize_unreachable(): s_Int_isize
  requires false
  ensures false


function p_Int_isize_snap(self: Ref): s_Int_isize
  requires acc(p_Int_isize(self), wildcard)
{
  (unfolding acc(p_Int_isize(self), wildcard) in self.p_Int_isize_val)
}

function p_FallibleVec_field_discr(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_FallibleVec_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_FallibleVec_unreachable(): s_FallibleVec
  requires false
  ensures false


function p_FallibleVec_snap(self: Ref): s_FallibleVec
  requires acc(p_FallibleVec(self), wildcard)
{
  (unfolding acc(p_FallibleVec(self), wildcard) in
    (p_Int_isize_snap(p_FallibleVec_field_discr(self)) ==
    s_Int_isize_cons(1) ?
      (unfolding acc(p_FallibleVec_1_owned(self), wildcard) in
        s_FallibleVec_1_cons()) :
      (p_Int_isize_snap(p_FallibleVec_field_discr(self)) ==
      s_Int_isize_cons(0) ?
        (unfolding acc(p_FallibleVec_0_owned(self), wildcard) in
          s_FallibleVec_0_cons(p_Vector_snap(p_FallibleVec_0_field_0(self)))) :
        p_FallibleVec_unreachable())))
}

function p_Bounds_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Bounds_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Bounds_unreachable(): s_Bounds
  requires false
  ensures false


function p_Bounds_snap(self: Ref): s_Bounds
  requires acc(p_Bounds(self), wildcard)
{
  (unfolding acc(p_Bounds(self), wildcard) in
    s_Bounds_cons(p_Int_i32_snap(p_Bounds_field_0(self)), p_Int_i32_snap(p_Bounds_field_1(self))))
}

function p_ClampTransform_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_ClampTransform_unreachable(): s_ClampTransform
  requires false
  ensures false


function p_ClampTransform_snap(self: Ref): s_ClampTransform
  requires acc(p_ClampTransform(self), wildcard)
{
  (unfolding acc(p_ClampTransform(self), wildcard) in
    s_ClampTransform_cons(p_Bounds_snap(p_ClampTransform_field_0(self))))
}

function p_Output_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Output_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_Output_unreachable(): s_Output
  requires false
  ensures false


function p_Output_snap(self: Ref): s_Output
  requires acc(p_Output(self), wildcard)
{
  (unfolding acc(p_Output(self), wildcard) in
    s_Output_cons(p_FallibleVec_snap(p_Output_field_0(self)), p_ClampTransform_snap(p_Output_field_1(self))))
}

function p_FallibleI32_field_discr(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_FallibleI32_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_FallibleI32_unreachable(): s_FallibleI32
  requires false
  ensures false


function p_FallibleI32_snap(self: Ref): s_FallibleI32
  requires acc(p_FallibleI32(self), wildcard)
{
  (unfolding acc(p_FallibleI32(self), wildcard) in
    (p_Int_isize_snap(p_FallibleI32_field_discr(self)) ==
    s_Int_isize_cons(1) ?
      (unfolding acc(p_FallibleI32_1_owned(self), wildcard) in
        s_FallibleI32_1_cons()) :
      (p_Int_isize_snap(p_FallibleI32_field_discr(self)) ==
      s_Int_isize_cons(0) ?
        (unfolding acc(p_FallibleI32_0_owned(self), wildcard) in
          s_FallibleI32_0_cons(p_Int_i32_snap(p_FallibleI32_0_field_0(self)))) :
        p_FallibleI32_unreachable())))
}

function p_ImpureOutput_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_ImpureOutput_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_ImpureOutput_unreachable(): s_ImpureOutput
  requires false
  ensures false


function p_ImpureOutput_snap(self: Ref): s_ImpureOutput
  requires acc(p_ImpureOutput(self), wildcard)
{
  (unfolding acc(p_ImpureOutput(self), wildcard) in
    s_ImpureOutput_cons(p_FallibleI32_snap(p_ImpureOutput_field_0(self)), p_ClampTransform_snap(p_ImpureOutput_field_1(self))))
}

function p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_2(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_unreachable(): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0
  requires false
  ensures false


function p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_snap(self: Ref): s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0
  requires acc(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(self), wildcard)
{
  (unfolding acc(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(self), wildcard) in
    s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(p_Ref_immutable_snap(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_0(self),
    s_UInt_usize_type()), p_Vector_snap(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_1(self)),
    p_FallibleVec_snap(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_2(self))))
}

function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_2(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_3(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_unreachable(): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0
  requires false
  ensures false


function p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_snap(self: Ref): s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0
  requires acc(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(self), wildcard)
{
  (unfolding acc(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(self), wildcard) in
    s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(p_Ref_immutable_snap(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_0(self),
    s_UInt_usize_type()), p_FallibleVec_snap(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_1(self)),
    p_ClampTransform_snap(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_2(self)),
    p_Vector_snap(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_3(self))))
}

function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_0(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_1(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_2(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_3(self: Ref): Ref
  ensures (self == null) == (result == null)


function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_unreachable(): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0
  requires false
  ensures false


function p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_snap(self: Ref): s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0
  requires acc(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(self), wildcard)
{
  (unfolding acc(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(self), wildcard) in
    s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(p_FallibleVec_snap(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_0(self)),
    p_Ref_immutable_snap(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_1(self),
    s_Int_i32_type()), p_Ref_immutable_snap(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_2(self),
    s_Int_i32_type()), p_Ref_immutable_snap(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_3(self),
    s_UInt_usize_type())))
}

predicate p_Param(self_p: Ref, t: Type) 

predicate p_2_Tuple(self: Ref, T0: Type, T1: Type) {
  acc(p_Param(p_2_Tuple_field_0(self, T0, T1), T0), write) &&
  acc(p_Param(p_2_Tuple_field_1(self, T0, T1), T1), write)
}

predicate p_Int_i32(self: Ref) {
  acc(self.p_Int_i32_val, write)
}

predicate p_UInt_usize(self: Ref) {
  acc(self.p_UInt_usize_val, write)
}

predicate p_Vector(self: Ref) {
  acc(p_UInt_usize(p_Vector_field_0(self)), write) &&
  acc(p_Int_i32(p_Vector_field_1(self)), write)
}

predicate p_Never(self: Ref) {
  false
}

predicate p_Bool(self: Ref) {
  acc(self.p_Bool_val, write)
}

predicate p_0_Tuple(self: Ref) {
  true
}

predicate p_Ref_immutable(self: Ref, T: Type) {
  acc(self.p_Ref_immutable_val, write) &&
  typ(s_Ref_immutable_value(self.p_Ref_immutable_val)) == T
}

predicate p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(self: Ref) {
  acc(p_Vector(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_0(self)), write) &&
  (acc(p_Ref_immutable(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_1(self),
  s_UInt_usize_type()), write) &&
  acc(p_Vector(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_field_2(self)), write))
}

predicate p_Int_isize(self: Ref) {
  acc(self.p_Int_isize_val, write)
}

predicate p_FallibleVec_0_owned(self: Ref) {
  acc(p_Vector(p_FallibleVec_0_field_0(self)), write)
}

predicate p_FallibleVec_1_owned(self: Ref) {
  true
}

predicate p_FallibleVec(self: Ref) {
  acc(p_Int_isize(p_FallibleVec_field_discr(self)), write) &&
  ((p_Int_isize_snap(p_FallibleVec_field_discr(self)) ==
  s_Int_isize_cons(0) ||
  p_Int_isize_snap(p_FallibleVec_field_discr(self)) == s_Int_isize_cons(1)) &&
  ((p_Int_isize_snap(p_FallibleVec_field_discr(self)) ==
  s_Int_isize_cons(0) ==>
  acc(p_FallibleVec_0_owned(self), write)) &&
  (p_Int_isize_snap(p_FallibleVec_field_discr(self)) == s_Int_isize_cons(1) ==>
  acc(p_FallibleVec_1_owned(self), write))))
}

predicate p_Bounds(self: Ref) {
  acc(p_Int_i32(p_Bounds_field_0(self)), write) &&
  acc(p_Int_i32(p_Bounds_field_1(self)), write)
}

predicate p_ClampTransform(self: Ref) {
  acc(p_Bounds(p_ClampTransform_field_0(self)), write)
}

predicate p_Output(self: Ref) {
  acc(p_FallibleVec(p_Output_field_0(self)), write) &&
  acc(p_ClampTransform(p_Output_field_1(self)), write)
}

predicate p_FallibleI32_0_owned(self: Ref) {
  acc(p_Int_i32(p_FallibleI32_0_field_0(self)), write)
}

predicate p_FallibleI32_1_owned(self: Ref) {
  true
}

predicate p_FallibleI32(self: Ref) {
  acc(p_Int_isize(p_FallibleI32_field_discr(self)), write) &&
  ((p_Int_isize_snap(p_FallibleI32_field_discr(self)) ==
  s_Int_isize_cons(0) ||
  p_Int_isize_snap(p_FallibleI32_field_discr(self)) == s_Int_isize_cons(1)) &&
  ((p_Int_isize_snap(p_FallibleI32_field_discr(self)) ==
  s_Int_isize_cons(0) ==>
  acc(p_FallibleI32_0_owned(self), write)) &&
  (p_Int_isize_snap(p_FallibleI32_field_discr(self)) == s_Int_isize_cons(1) ==>
  acc(p_FallibleI32_1_owned(self), write))))
}

predicate p_ImpureOutput(self: Ref) {
  acc(p_FallibleI32(p_ImpureOutput_field_0(self)), write) &&
  acc(p_ClampTransform(p_ImpureOutput_field_1(self)), write)
}

predicate p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(self: Ref) {
  acc(p_Ref_immutable(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_0(self),
  s_UInt_usize_type()), write) &&
  (acc(p_Vector(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_1(self)), write) &&
  acc(p_FallibleVec(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_field_2(self)), write))
}

predicate p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(self: Ref) {
  acc(p_Ref_immutable(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_0(self),
  s_UInt_usize_type()), write) &&
  (acc(p_FallibleVec(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_1(self)), write) &&
  (acc(p_ClampTransform(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_2(self)), write) &&
  acc(p_Vector(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_field_3(self)), write)))
}

predicate p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(self: Ref) {
  acc(p_FallibleVec(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_0(self)), write) &&
  (acc(p_Ref_immutable(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_1(self),
  s_Int_i32_type()), write) &&
  (acc(p_Ref_immutable(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_2(self),
  s_Int_i32_type()), write) &&
  acc(p_Ref_immutable(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_field_3(self),
  s_UInt_usize_type()), write)))
}

method m_Vector$colon$$colon$impure_get(_0p: Ref, _1p: Ref, _2p: Ref)
  requires acc(p_Vector(_1p), write)
  requires acc(p_UInt_usize(_2p), write)
  requires s_Bool_value(mir_binop_Lt_usize_usize(p_UInt_usize_snap(_2p), s_Vector_read_0(p_Vector_snap(_1p))))
  ensures acc(p_2_Tuple(_0p, s_Int_i32_type(), s_Vector_type()), write)
  ensures s_Bool_value(mir_binop_Eq_i32_i32(make_concrete_s_Int_i32(s_2_Tuple_read_0(p_2_Tuple_snap(_0p,
    s_Int_i32_type(), s_Vector_type()))), f_Vector$colon$$colon$get(p_Vector_snap(_1p),
    p_UInt_usize_snap(_2p))))
  ensures s_Bool_value(s_Bool_cons(s_Ref_immutable_cons(null, make_generic_s_Vector(make_concrete_s_Vector(s_2_Tuple_read_1(p_2_Tuple_snap(_0p,
    s_Int_i32_type(), s_Vector_type()))))) ==
    s_Ref_immutable_cons(null, make_generic_s_Vector(make_concrete_s_Vector(s_Ref_immutable_value(s_Ref_immutable_cons(null,
    make_generic_s_Vector(p_Vector_snap(_1p)))))))))


method m_Vector$colon$$colon$set(_0p: Ref, _1p: Ref, _2p: Ref, _3p: Ref)
  requires acc(p_Vector(_1p), write)
  requires acc(p_UInt_usize(_2p), write)
  requires acc(p_Int_i32(_3p), write)
  requires s_Bool_value(mir_binop_Lt_usize_usize(p_UInt_usize_snap(_2p), s_Vector_read_0(p_Vector_snap(_1p))))
  ensures acc(p_Vector(_0p), write)
  ensures s_Bool_value(mir_binop_Eq_usize_usize(s_Vector_read_0(p_Vector_snap(_1p)),
    s_Vector_read_0(p_Vector_snap(_0p))))
  ensures s_Bool_value(mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(p_Vector_snap(_0p),
    p_UInt_usize_snap(_2p)), p_Int_i32_snap(_3p)))
  ensures s_Bool_value(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Lt_usize_usize(qvar_0_0,
      s_Vector_read_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(p_Vector_snap(_1p),
      s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_2p))),
      p_Vector_snap(_0p)))))))))))))) ?
        s_Bool_cons(true) :
        make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ne_usize_usize(qvar_0_0,
        make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_1(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(p_Vector_snap(_1p),
        s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_2p))),
        p_Vector_snap(_0p))))))))))))))) ?
          s_Bool_cons(true) :
          mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_2(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(p_Vector_snap(_1p),
          s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_2p))),
          p_Vector_snap(_0p))))))))))), qvar_0_0), f_Vector$colon$$colon$get(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_read_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(make_concrete_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_cons(p_Vector_snap(_1p),
          s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_2p))),
          p_Vector_snap(_0p))))))))))), qvar_0_0))))))))))))


method m_apply_row_by_row_rec(_0p: Ref, _1p: Ref, _2p: Ref, _3p: Ref)
  requires acc(p_ClampTransform(_1p), write)
  requires acc(p_Vector(_2p), write)
  requires acc(p_UInt_usize(_3p), write)
  requires s_Bool_value(mir_binop_Ge_usize_usize(s_Vector_read_0(p_Vector_snap(_2p)),
    s_UInt_usize_cons(1)))
  requires s_Bool_value(mir_binop_Lt_usize_usize(p_UInt_usize_snap(_3p), s_Vector_read_0(p_Vector_snap(_2p))))
  ensures acc(p_Output(_0p), write)
  ensures s_Bool_value(s_Bool_cons(s_Ref_immutable_cons(null, make_generic_s_ClampTransform(s_Output_read_1(p_Output_snap(_0p)))) ==
    s_Ref_immutable_cons(null, make_generic_s_ClampTransform(make_concrete_s_ClampTransform(s_Ref_immutable_value(s_Ref_immutable_cons(null,
    make_generic_s_ClampTransform(p_ClampTransform_snap(_1p)))))))))
  ensures s_Bool_value(mir_binop_Eq_bool_bool(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
    s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p)))), make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(s_Output_read_0(p_Output_snap(_0p)))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false))))))
  ensures s_Bool_value(make_concrete_s_Bool(s_2_Tuple_read_0((!s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(s_Output_read_0(p_Output_snap(_0p)))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false))))) ?
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(s_Ref_immutable_cons(null,
      make_generic_s_UInt_usize(s_Vector_read_0(f_FallibleVec$colon$$colon$unwrap_vec(s_Output_read_0(p_Output_snap(_0p)))))) ==
      s_Ref_immutable_cons(null, make_generic_s_UInt_usize(make_concrete_s_UInt_usize(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_UInt_usize(s_Vector_read_0(p_Vector_snap(_2p)))))))))),
      make_generic_s_Bool(s_Bool_cons(s_Ref_immutable_cons(null, make_generic_s_UInt_usize(s_Vector_read_0(f_FallibleVec$colon$$colon$unwrap_vec(s_Output_read_0(p_Output_snap(_0p)))))) ==
      s_Ref_immutable_cons(null, make_generic_s_UInt_usize(make_concrete_s_UInt_usize(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_UInt_usize(s_Vector_read_0(p_Vector_snap(_2p)))))))))))))))
  ensures s_Bool_value(make_concrete_s_Bool(s_2_Tuple_read_0((!s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(s_Output_read_0(p_Output_snap(_0p)))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false))))) ?
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Gt_usize_usize(qvar_0_0,
        make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
        make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
        s_Output_read_0(p_Output_snap(_0p)))))))))))))))) ?
          s_Bool_cons(true) :
          make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Lt_usize_usize(qvar_0_0,
          s_Vector_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
          s_Output_read_0(p_Output_snap(_0p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
            s_Output_read_0(p_Output_snap(_0p))))))))))))), qvar_0_0), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
            s_Output_read_0(p_Output_snap(_0p)))))))))))), qvar_0_0)))))))))))),
      make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Gt_usize_usize(qvar_0_0,
        make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
        make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
        s_Output_read_0(p_Output_snap(_0p)))))))))))))))) ?
          s_Bool_cons(true) :
          make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Lt_usize_usize(qvar_0_0,
          s_Vector_read_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
          s_Output_read_0(p_Output_snap(_0p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
            s_Output_read_0(p_Output_snap(_0p))))))))))))), qvar_0_0), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), p_Vector_snap(_2p),
            s_Output_read_0(p_Output_snap(_0p)))))))))))), qvar_0_0)))))))))))))))))
  ensures s_Bool_value(make_concrete_s_Bool(s_2_Tuple_read_0((!s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(s_Output_read_0(p_Output_snap(_0p)))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false))))) ?
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
      s_2_Tuple_cons(make_generic_s_Bool(make_concrete_s_Bool(s_2_Tuple_read_0((!s_Bool_value(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
      s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
        s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
        s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_usize_usize(qvar_0_0,
          make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
          p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p)))))))))))), qvar_0_0),
            f_ClampTransform$colon$$colon$do_transform(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), qvar_0_0)))))))))),
        make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_usize_usize(qvar_0_0,
          make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
          p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p)))))))))))), qvar_0_0),
            f_ClampTransform$colon$$colon$do_transform(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), qvar_0_0))))))))))))))),
      make_generic_s_Bool(make_concrete_s_Bool(s_2_Tuple_read_1((!s_Bool_value(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
      s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
        s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
        s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_usize_usize(qvar_0_0,
          make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
          p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p)))))))))))), qvar_0_0),
            f_ClampTransform$colon$$colon$do_transform(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), qvar_0_0)))))))))),
        make_generic_s_Bool(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_usize_usize(qvar_0_0,
          make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
          make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
          p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))))))) ?
            s_Bool_cons(true) :
            mir_binop_Eq_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p)))))))))))), qvar_0_0),
            f_ClampTransform$colon$$colon$do_transform(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), f_Vector$colon$$colon$get(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_read_3(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_cons(s_Ref_immutable_cons(null,
            make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))), s_Output_read_0(p_Output_snap(_0p)),
            p_ClampTransform_snap(_1p), p_Vector_snap(_2p))))))))))), qvar_0_0))))))))))))))))))))
  ensures s_Bool_value(s_Bool_cons((forall qvar_0_0: s_UInt_usize ::s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool(s_Bool_cons(s_Int_isize_value(s_FallibleVec_discr(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
      s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
      s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
      s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))) ==
      0)))) ?
        s_Bool_cons(true) :
        make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_i32_i32(make_concrete_s_Int_i32(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
        s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
        s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
        s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))),
        make_concrete_s_Int_i32(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
        make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
        s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
        s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
        s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))))) ?
          s_Bool_cons(true) :
          make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_usize_usize(qvar_0_0,
          make_concrete_s_UInt_usize(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_3(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
          make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
          s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
          s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
          s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))))) ?
            s_Bool_cons(true) :
            make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ge_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
            s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
            s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
            s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p)))))))))))))),
            qvar_0_0), make_concrete_s_Int_i32(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_2(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
            make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
            s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
            s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
            s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))))) ?
              s_Bool_cons(false) :
              mir_binop_Le_i32_i32(f_Vector$colon$$colon$get(f_FallibleVec$colon$$colon$unwrap_vec(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
              make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
              make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
              s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
              s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
              s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p)))))))))))))),
              qvar_0_0), make_concrete_s_Int_i32(s_Ref_immutable_value(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_read_1(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
              make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(make_concrete_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_Ref_immutable_value(s_Ref_immutable_cons(null,
              make_generic_s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_cons(s_Output_read_0(p_Output_snap(_0p)),
              s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
              s_Ref_immutable_cons(null, make_generic_s_Int_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))),
              s_Ref_immutable_cons(null, make_generic_s_UInt_usize(p_UInt_usize_snap(_3p))))))))))))))))))))))))))))))))


method m_FallibleI32$colon$$colon$unwrap_i32(_0p: Ref, _1p: Ref)
  requires acc(p_FallibleI32(_1p), write)
  requires s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleI32_discr(p_FallibleI32_snap(_1p))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false)))))
  ensures acc(p_Int_i32(_0p), write)
{
  var _2p: Ref
  var _3p: Ref
  var _from_bb0_to_bb2: Bool
  var _from_bb0_to_bb3: Bool
  var _from_bb0_to_bb1: Bool
  var _from_bb2_to_bb4: Bool
  var _from_bb4_to_bb5: Bool
  var _from_bb3_to_bb5: Bool
  var _tmp0: s_Int_isize
  label start
  // var _2p
  // var _3p
  _from_bb0_to_bb2 := false
  _from_bb0_to_bb3 := false
  _from_bb0_to_bb1 := false
  _from_bb2_to_bb4 := false
  _from_bb4_to_bb5 := false
  _from_bb3_to_bb5 := false
  goto bb_0
  label bb_0
  // [MIR] bb0[0]: PlaceMention(_1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  label _after_0_0
  // [MIR] bb0[1]: _2 = discriminant(_1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_2, bb0[1])
  // (ignoring)
  // PCG repacks_start
  // PCG repacks_middle
  p_Int_isize_assign(_2p, (unfolding acc(p_FallibleI32(_1p), wildcard) in
      p_Int_isize_snap(p_FallibleI32_field_discr(_1p))))
  label _after_0_1
  // [MIR] bb0[2]: switchInt(move _2) -> [0: bb2, 1: bb3, otherwise: bb1]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: MakePlaceOld(_2, MoveOut)
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  // var _tmp0
  _tmp0 := p_Int_isize_snap(_2p)
  exhale acc(p_Int_isize(_2p), write)
  label _after_0_2
  if (s_Int_isize_value(_tmp0) == 0) {
    _from_bb0_to_bb2 := true
    goto bb_2
  } elseif (s_Int_isize_value(_tmp0) == 1) {
    _from_bb0_to_bb3 := true
    goto bb_3
  } else {
    _from_bb0_to_bb1 := true
    goto bb_1
  }
  label bb_1
  // [MIR] bb1[0]: FakeRead(ForMatchedPlace(None), _1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  label _after_1_0
  // [MIR] bb1[1]: unreachable
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  exhale false
  label _after_1_1
  inhale false
  label bb_2
  // [MIR] bb2[0]: falseEdge -> [real: bb4, imaginary: bb3]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb2_to_bb4 := true
  label _after_2_0
  goto bb_4
  label bb_3
  // [MIR] bb3[0]: _0 = unreachable_i32() -> [return: bb5, unwind: bb6]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: SetLatest(_0, bb3[0])
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  goto bb_term_3
  label bb_term_3
  p_Int_i32_assign(_0p, f_unreachable_i32())
  _from_bb3_to_bb5 := true
  label _after_3_0
  goto bb_5
  label bb_4
  // [MIR] bb4[0]: StorageLive(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb4[1]: _3 = copy ((_1 as Ok).0: i32)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_3, bb4[1])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, (_1@Ok), R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_FallibleI32(_1p), write)
  // pcs_repack: Expand((_1@Ok), (_1@Ok).0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_FallibleI32_0_owned(_1p), write)
  // PCG repacks_middle
  p_Int_i32_assign(_3p, p_Int_i32_snap(p_FallibleI32_0_field_0(_1p)))
  label _after_4_1
  // [MIR] bb4[2]: _0 = copy _3
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_0, bb4[2])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Collapse((_1@Ok), (_1@Ok).0, E)
  fold acc(p_FallibleI32_0_owned(_1p), write)
  // pcs_repack: Collapse(_1, (_1@Ok), E)
  fold acc(p_FallibleI32(_1p), write)
  // PCG repacks_middle
  p_Int_i32_assign(_0p, p_Int_i32_snap(_3p))
  label _after_4_2
  // [MIR] bb4[3]: StorageDead(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_3, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // pcs_repack: Weaken(_3, E, W)
  // exhale due to Weaken(E, W)
  exhale acc(p_Int_i32(_3p), write)
  // [MIR] bb4[4]: goto -> bb5
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb4_to_bb5 := true
  label _after_4_4
  goto bb_5
  label bb_5
  // [MIR] bb5[0]: return
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  label package_post0
  label _after_5_0
  goto end
  label bb_6
  // cleanup block
  assert false
  label end
  // return
}

method m_FallibleVec$colon$$colon$unwrap_vec(_0p: Ref, _1p: Ref)
  requires acc(p_FallibleVec(_1p), write)
  requires s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleVec_discr(p_FallibleVec_snap(_1p))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false)))))
  ensures acc(p_Vector(_0p), write)
{
  var _2p: Ref
  var _3p: Ref
  var _from_bb0_to_bb2: Bool
  var _from_bb0_to_bb3: Bool
  var _from_bb0_to_bb1: Bool
  var _from_bb2_to_bb4: Bool
  var _from_bb4_to_bb5: Bool
  var _from_bb3_to_bb5: Bool
  var _tmp0: s_Int_isize
  var _tmp1: s_Vector
  var _tmp2: s_Vector
  label start
  // var _2p
  // var _3p
  _from_bb0_to_bb2 := false
  _from_bb0_to_bb3 := false
  _from_bb0_to_bb1 := false
  _from_bb2_to_bb4 := false
  _from_bb4_to_bb5 := false
  _from_bb3_to_bb5 := false
  goto bb_0
  label bb_0
  // [MIR] bb0[0]: PlaceMention(_1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  label _after_0_0
  // [MIR] bb0[1]: _2 = discriminant(_1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_2, bb0[1])
  // (ignoring)
  // PCG repacks_start
  // PCG repacks_middle
  p_Int_isize_assign(_2p, (unfolding acc(p_FallibleVec(_1p), wildcard) in
      p_Int_isize_snap(p_FallibleVec_field_discr(_1p))))
  label _after_0_1
  // [MIR] bb0[2]: switchInt(move _2) -> [0: bb2, 1: bb3, otherwise: bb1]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: MakePlaceOld(_2, MoveOut)
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  // var _tmp0
  _tmp0 := p_Int_isize_snap(_2p)
  exhale acc(p_Int_isize(_2p), write)
  label _after_0_2
  if (s_Int_isize_value(_tmp0) == 0) {
    _from_bb0_to_bb2 := true
    goto bb_2
  } elseif (s_Int_isize_value(_tmp0) == 1) {
    _from_bb0_to_bb3 := true
    goto bb_3
  } else {
    _from_bb0_to_bb1 := true
    goto bb_1
  }
  label bb_1
  // [MIR] bb1[0]: FakeRead(ForMatchedPlace(None), _1)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  label _after_1_0
  // [MIR] bb1[1]: unreachable
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  exhale false
  label _after_1_1
  inhale false
  label bb_2
  // [MIR] bb2[0]: falseEdge -> [real: bb4, imaginary: bb3]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb2_to_bb4 := true
  label _after_2_0
  goto bb_4
  label bb_3
  // [MIR] bb3[0]: _0 = unreachable_vec() -> [return: bb5, unwind: bb6]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: SetLatest(_0, bb3[0])
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  goto bb_term_3
  label bb_term_3
  p_Vector_assign(_0p, f_unreachable_vec())
  _from_bb3_to_bb5 := true
  label _after_3_0
  goto bb_5
  label bb_4
  // [MIR] bb4[0]: StorageLive(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb4[1]: _3 = move ((_1 as Ok).0: Vector)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: MakePlaceOld((_1@Ok).0, MoveOut)
  // (ignoring)
  // pcs_action: SetLatest(_3, bb4[1])
  // (ignoring)
  // pcs_action: RenamePlace { old: OldPlace(PlaceSnapshot { place: (_1@Ok).0, at: After(bb0[0]) }), new: Current { place: _3 } }
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, (_1@Ok), E)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_FallibleVec(_1p), write)
  // pcs_repack: Expand((_1@Ok), (_1@Ok).0, E)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_FallibleVec_0_owned(_1p), write)
  // PCG repacks_middle
  // var _tmp1
  _tmp1 := p_Vector_snap(p_FallibleVec_0_field_0(_1p))
  exhale acc(p_Vector(p_FallibleVec_0_field_0(_1p)), write)
  p_Vector_assign(_3p, _tmp1)
  label _after_4_1
  // [MIR] bb4[2]: _0 = move _3
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: MakePlaceOld(_3, MoveOut)
  // (ignoring)
  // pcs_action: SetLatest(_0, bb4[2])
  // (ignoring)
  // pcs_action: RenamePlace { old: OldPlace(PlaceSnapshot { place: _3, at: After(bb4[1]) }), new: Current { place: _0 } }
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Collapse((_1@Ok), (_1@Ok).0, W)
  // PCG repacks_middle
  // var _tmp2
  _tmp2 := p_Vector_snap(_3p)
  exhale acc(p_Vector(_3p), write)
  p_Vector_assign(_0p, _tmp2)
  label _after_4_2
  // [MIR] bb4[3]: StorageDead(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_3, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb4[4]: goto -> bb5
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb4_to_bb5 := true
  label _after_4_4
  goto bb_5
  label bb_5
  // [MIR] bb5[0]: return
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  label package_post0
  label _after_5_0
  goto end
  label bb_6
  // cleanup block
  assert false
  label end
  // return
}

method m_ClampTransform$colon$$colon$make_clamp(_0p: Ref, _1p: Ref)
  requires acc(p_Bounds(_1p), write)
  ensures acc(p_ClampTransform(_0p), write)
  ensures s_Bool_value(s_Bool_cons(s_Ref_immutable_cons(null, make_generic_s_Bounds(s_ClampTransform_read_0(p_ClampTransform_snap(_0p)))) ==
    s_Ref_immutable_cons(null, make_generic_s_Bounds(make_concrete_s_Bounds(s_Ref_immutable_value(s_Ref_immutable_cons(null,
    make_generic_s_Bounds(p_Bounds_snap(_1p)))))))))


method m_ClampTransform$colon$$colon$do_transform(_0p: Ref, _1p: Ref, _2p: Ref)
  requires acc(p_ClampTransform(_1p), write)
  requires acc(p_Int_i32(_2p), write)
  requires s_Bool_value(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
    s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p)))))
  ensures acc(p_Int_i32(_0p), write)
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ge_i32_i32(p_Int_i32_snap(_0p),
    s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
      s_Bool_cons(false) :
      mir_binop_Le_i32_i32(p_Int_i32_snap(_0p), s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Lt_i32_i32(p_Int_i32_snap(_2p),
    s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
      s_Bool_cons(true) :
      mir_binop_Eq_i32_i32(p_Int_i32_snap(_0p), s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Gt_i32_i32(p_Int_i32_snap(_2p),
    s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
      s_Bool_cons(true) :
      mir_binop_Eq_i32_i32(p_Int_i32_snap(_0p), s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))))))
  ensures s_Bool_value(make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Ge_i32_i32(p_Int_i32_snap(_2p),
    s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
      s_Bool_cons(true) :
      make_concrete_s_Bool(make_generic_s_Bool((!s_Bool_value(mir_binop_Le_i32_i32(p_Int_i32_snap(_2p),
      s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
        s_Bool_cons(true) :
        mir_binop_Eq_i32_i32(p_Int_i32_snap(_0p), p_Int_i32_snap(_2p)))))))))
{
  var _3p: Ref
  var _4p: Ref
  var _5p: Ref
  var _6p: Ref
  var _7p: Ref
  var _8p: Ref
  var _from_bb0_to_bb2: Bool
  var _from_bb0_to_bb1: Bool
  var _from_bb1_to_bb6: Bool
  var _from_bb3_to_bb5: Bool
  var _from_bb5_to_bb6: Bool
  var _from_bb4_to_bb5: Bool
  var _from_bb2_to_bb4: Bool
  var _from_bb2_to_bb3: Bool
  var _tmp0: s_Int_i32
  var _tmp1: s_Int_i32
  var _tmp2: s_Bool
  var _tmp3: s_Int_i32
  var _tmp4: s_Int_i32
  var _tmp5: s_Bool
  label start
  // var _3p
  // var _4p
  // var _5p
  // var _6p
  // var _7p
  // var _8p
  _from_bb0_to_bb2 := false
  _from_bb0_to_bb1 := false
  _from_bb1_to_bb6 := false
  _from_bb3_to_bb5 := false
  _from_bb5_to_bb6 := false
  _from_bb4_to_bb5 := false
  _from_bb2_to_bb4 := false
  _from_bb2_to_bb3 := false
  goto bb_0
  label bb_0
  // [MIR] bb0[0]: StorageLive(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb0[1]: StorageLive(_4)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb0[2]: _4 = copy _2
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_4, bb0[2])
  // (ignoring)
  // PCG repacks_start
  // PCG repacks_middle
  p_Int_i32_assign(_4p, p_Int_i32_snap(_2p))
  label _after_0_2
  // [MIR] bb0[3]: StorageLive(_5)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb0[4]: _5 = copy ((_1.0: Bounds).1: i32)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_5, bb0[4])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, _1.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_ClampTransform(_1p), write)
  // pcs_repack: Expand(_1.0, _1.0.1, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // PCG repacks_middle
  p_Int_i32_assign(_5p, p_Int_i32_snap(p_Bounds_field_1(p_ClampTransform_field_0(_1p))))
  label _after_0_4
  // [MIR] bb0[5]: _3 = Lt(move _4, move _5)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: MakePlaceOld(_4, MoveOut)
  // (ignoring)
  // pcs_action: MakePlaceOld(_5, MoveOut)
  // (ignoring)
  // pcs_action: SetLatest(_3, bb0[5])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Collapse(_1.0, _1.0.0, E)
  fold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // pcs_repack: Collapse(_1, _1.0, E)
  fold acc(p_ClampTransform(_1p), write)
  // PCG repacks_middle
  // var _tmp0
  _tmp0 := p_Int_i32_snap(_4p)
  exhale acc(p_Int_i32(_4p), write)
  // var _tmp1
  _tmp1 := p_Int_i32_snap(_5p)
  exhale acc(p_Int_i32(_5p), write)
  p_Bool_assign(_3p, mir_binop_Lt_i32_i32(_tmp0, _tmp1))
  label _after_0_5
  // [MIR] bb0[6]: switchInt(move _3) -> [0: bb2, otherwise: bb1]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: MakePlaceOld(_3, MoveOut)
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  // var _tmp2
  _tmp2 := p_Bool_snap(_3p)
  exhale acc(p_Bool(_3p), write)
  label _after_0_6
  if (s_Bool_value(_tmp2) == false) {
    _from_bb0_to_bb2 := true
    goto bb_2
  } else {
    _from_bb0_to_bb1 := true
    goto bb_1
  }
  label bb_1
  // [MIR] bb1[0]: StorageDead(_5)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_5, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb1[1]: StorageDead(_4)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_4, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb1[2]: _0 = copy ((_1.0: Bounds).1: i32)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_0, bb1[2])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, _1.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_ClampTransform(_1p), write)
  // pcs_repack: Expand(_1.0, _1.0.1, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // PCG repacks_middle
  p_Int_i32_assign(_0p, p_Int_i32_snap(p_Bounds_field_1(p_ClampTransform_field_0(_1p))))
  label _after_1_2
  // [MIR] bb1[3]: goto -> bb6
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // pcs_repack: Collapse(_1.0, _1.0.0, E)
  fold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // pcs_repack: Collapse(_1, _1.0, E)
  fold acc(p_ClampTransform(_1p), write)
  // PCG (T) repacks_middle
  _from_bb1_to_bb6 := true
  label _after_1_3
  goto bb_6
  label bb_2
  // [MIR] bb2[0]: StorageDead(_5)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_5, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb2[1]: StorageDead(_4)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_4, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb2[2]: StorageLive(_6)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb2[3]: StorageLive(_7)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb2[4]: _7 = copy _2
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_7, bb2[4])
  // (ignoring)
  // PCG repacks_start
  // PCG repacks_middle
  p_Int_i32_assign(_7p, p_Int_i32_snap(_2p))
  label _after_2_4
  // [MIR] bb2[5]: StorageLive(_8)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb2[6]: _8 = copy ((_1.0: Bounds).0: i32)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_8, bb2[6])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, _1.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_ClampTransform(_1p), write)
  // pcs_repack: Expand(_1.0, _1.0.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // PCG repacks_middle
  p_Int_i32_assign(_8p, p_Int_i32_snap(p_Bounds_field_0(p_ClampTransform_field_0(_1p))))
  label _after_2_6
  // [MIR] bb2[7]: _6 = Gt(move _7, move _8)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: MakePlaceOld(_7, MoveOut)
  // (ignoring)
  // pcs_action: MakePlaceOld(_8, MoveOut)
  // (ignoring)
  // pcs_action: SetLatest(_6, bb2[7])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Collapse(_1.0, _1.0.0, E)
  fold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // pcs_repack: Collapse(_1, _1.0, E)
  fold acc(p_ClampTransform(_1p), write)
  // PCG repacks_middle
  // var _tmp3
  _tmp3 := p_Int_i32_snap(_7p)
  exhale acc(p_Int_i32(_7p), write)
  // var _tmp4
  _tmp4 := p_Int_i32_snap(_8p)
  exhale acc(p_Int_i32(_8p), write)
  p_Bool_assign(_6p, mir_binop_Gt_i32_i32(_tmp3, _tmp4))
  label _after_2_7
  // [MIR] bb2[8]: switchInt(move _6) -> [0: bb4, otherwise: bb3]
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // pcs_action: MakePlaceOld(_6, MoveOut)
  // (ignoring)
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  // var _tmp5
  _tmp5 := p_Bool_snap(_6p)
  exhale acc(p_Bool(_6p), write)
  label _after_2_8
  if (s_Bool_value(_tmp5) == false) {
    _from_bb2_to_bb4 := true
    goto bb_4
  } else {
    _from_bb2_to_bb3 := true
    goto bb_3
  }
  label bb_3
  // [MIR] bb3[0]: StorageDead(_8)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_8, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb3[1]: StorageDead(_7)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_7, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb3[2]: _0 = copy ((_1.0: Bounds).0: i32)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_0, bb3[2])
  // (ignoring)
  // PCG repacks_start
  // pcs_repack: Expand(_1, _1.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_ClampTransform(_1p), write)
  // pcs_repack: Expand(_1.0, _1.0.0, R)
  // unfolding because of RepackOp::Expand in pcs_repacks
  unfold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // PCG repacks_middle
  p_Int_i32_assign(_0p, p_Int_i32_snap(p_Bounds_field_0(p_ClampTransform_field_0(_1p))))
  label _after_3_2
  // [MIR] bb3[3]: goto -> bb5
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // pcs_repack: Collapse(_1.0, _1.0.0, E)
  fold acc(p_Bounds(p_ClampTransform_field_0(_1p)), write)
  // pcs_repack: Collapse(_1, _1.0, E)
  fold acc(p_ClampTransform(_1p), write)
  // PCG (T) repacks_middle
  _from_bb3_to_bb5 := true
  label _after_3_3
  goto bb_5
  label bb_4
  // [MIR] bb4[0]: StorageDead(_8)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_8, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb4[1]: StorageDead(_7)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_7, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb4[2]: _0 = copy _2
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // PCG PostMain
  // pcs_action: SetLatest(_0, bb4[2])
  // (ignoring)
  // PCG repacks_start
  // PCG repacks_middle
  p_Int_i32_assign(_0p, p_Int_i32_snap(_2p))
  label _after_4_2
  // [MIR] bb4[3]: goto -> bb5
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb4_to_bb5 := true
  label _after_4_3
  goto bb_5
  label bb_5
  // [MIR] bb5[0]: StorageDead(_6)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_6, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb5[1]: goto -> bb6
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  _from_bb5_to_bb6 := true
  label _after_5_1
  goto bb_6
  label bb_6
  // [MIR] bb6[0]: StorageDead(_3)
  // PCG PreOperands
  // PCG PostOperands
  // PCG PreMain
  // pcs_action: MakePlaceOld(_3, StorageDead)
  // (ignoring)
  // PCG PostMain
  // PCG repacks_start
  // PCG repacks_middle
  // [MIR] bb6[1]: return
  // PCG (T) PreOperands
  // PCG (T) PostOperands
  // PCG (T) PreMain
  // PCG (T) PostMain
  // PCG (T) repacks_start
  // PCG (T) repacks_middle
  label package_post0
  label _after_6_1
  goto end
  label end
  // return
}

method m_ClampTransform$colon$$colon$do_transform_impure(_0p: Ref, _1p: Ref,
  _2p: Ref)
  requires acc(p_ClampTransform(_1p), write)
  requires acc(p_Int_i32(_2p), write)
  ensures acc(p_ImpureOutput(_0p), write)
  ensures s_Bool_value(mir_binop_Eq_bool_bool(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
    s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p)))), make_concrete_s_Bool(make_generic_s_Bool((s_Int_isize_value(s_FallibleI32_discr(s_ImpureOutput_read_0(p_ImpureOutput_snap(_0p)))) ==
    0 ?
      s_Bool_cons(true) :
      s_Bool_cons(false))))))
  ensures s_Bool_value(make_concrete_s_Bool(s_2_Tuple_read_0((!s_Bool_value(mir_binop_Le_i32_i32(s_Bounds_read_1(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))),
    s_Bounds_read_0(s_ClampTransform_read_0(p_ClampTransform_snap(_1p))))) ?
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), make_generic_s_Bool(s_Bool_cons(true))) :
      s_2_Tuple_cons(make_generic_s_Bool(s_Bool_cons(s_Ref_immutable_cons(null,
      make_generic_s_Int_i32(f_FallibleI32$colon$$colon$unwrap_i32(s_ImpureOutput_read_0(p_ImpureOutput_snap(_0p))))) ==
      s_Ref_immutable_cons(null, make_generic_s_Int_i32(make_concrete_s_Int_i32(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_Int_i32(f_ClampTransform$colon$$colon$do_transform(p_ClampTransform_snap(_1p),
      p_Int_i32_snap(_2p)))))))))), make_generic_s_Bool(s_Bool_cons(s_Ref_immutable_cons(null,
      make_generic_s_Int_i32(f_FallibleI32$colon$$colon$unwrap_i32(s_ImpureOutput_read_0(p_ImpureOutput_snap(_0p))))) ==
      s_Ref_immutable_cons(null, make_generic_s_Int_i32(make_concrete_s_Int_i32(s_Ref_immutable_value(s_Ref_immutable_cons(null,
      make_generic_s_Int_i32(f_ClampTransform$colon$$colon$do_transform(p_ClampTransform_snap(_1p),
      p_Int_i32_snap(_2p)))))))))))))))
  ensures s_Bool_value(s_Bool_cons(s_Ref_immutable_cons(null, make_generic_s_ClampTransform(s_ImpureOutput_read_1(p_ImpureOutput_snap(_0p)))) ==
    s_Ref_immutable_cons(null, make_generic_s_ClampTransform(make_concrete_s_ClampTransform(s_Ref_immutable_value(s_Ref_immutable_cons(null,
    make_generic_s_ClampTransform(p_ClampTransform_snap(_1p)))))))))


method assign_p_Param(self: Ref, t: Type, self_new: s_Param)
  ensures acc(p_Param(self, t), write)
  ensures p_Param_snap(self, t) == self_new


method p_2_Tuple_assign(self: Ref, T0: Type, T1: Type, value: s_2_Tuple)
  ensures acc(p_2_Tuple(self, T0, T1), write)
  ensures p_2_Tuple_snap(self, T0, T1) == value


method p_Int_i32_assign(self: Ref, value: s_Int_i32)
  ensures acc(p_Int_i32(self), write)
  ensures p_Int_i32_snap(self) == value


method p_UInt_usize_assign(self: Ref, value: s_UInt_usize)
  ensures acc(p_UInt_usize(self), write)
  ensures p_UInt_usize_snap(self) == value


method p_Vector_assign(self: Ref, value: s_Vector)
  ensures acc(p_Vector(self), write)
  ensures p_Vector_snap(self) == value


method p_Never_assign(self: Ref, value: s_Never)
  ensures acc(p_Never(self), write)
  ensures p_Never_snap(self) == value


method p_Bool_assign(self: Ref, value: s_Bool)
  ensures acc(p_Bool(self), write)
  ensures p_Bool_snap(self) == value


method p_0_Tuple_assign(self: Ref, value: s_0_Tuple)
  ensures acc(p_0_Tuple(self), write)
  ensures p_0_Tuple_snap(self) == value


method p_Ref_immutable_assign(self: Ref, T: Type, value: s_Ref_immutable)
  ensures acc(p_Ref_immutable(self, T), write)
  ensures p_Ref_immutable_snap(self, T) == value


method p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_assign(self: Ref,
  value: s_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0)
  ensures acc(p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0(self), write)
  ensures p_prusti_post_item_set_b252ac599e2f4105ba519b0020c5520c_Closure_0_snap(self) ==
    value


method p_Int_isize_assign(self: Ref, value: s_Int_isize)
  ensures acc(p_Int_isize(self), write)
  ensures p_Int_isize_snap(self) == value


method p_FallibleVec_assign(self: Ref, value: s_FallibleVec)
  ensures acc(p_FallibleVec(self), write)
  ensures p_FallibleVec_snap(self) == value


method p_Bounds_assign(self: Ref, value: s_Bounds)
  ensures acc(p_Bounds(self), write)
  ensures p_Bounds_snap(self) == value


method p_ClampTransform_assign(self: Ref, value: s_ClampTransform)
  ensures acc(p_ClampTransform(self), write)
  ensures p_ClampTransform_snap(self) == value


method p_Output_assign(self: Ref, value: s_Output)
  ensures acc(p_Output(self), write)
  ensures p_Output_snap(self) == value


method p_FallibleI32_assign(self: Ref, value: s_FallibleI32)
  ensures acc(p_FallibleI32(self), write)
  ensures p_FallibleI32_snap(self) == value


method p_ImpureOutput_assign(self: Ref, value: s_ImpureOutput)
  ensures acc(p_ImpureOutput(self), write)
  ensures p_ImpureOutput_snap(self) == value


method p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_assign(self: Ref,
  value: s_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0)
  ensures acc(p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0(self), write)
  ensures p_prusti_post_item_apply_row_by_row_rec_25476a38a3704f1498f00036802a2851_Closure_0_snap(self) ==
    value


method p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_assign(self: Ref,
  value: s_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0)
  ensures acc(p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0(self), write)
  ensures p_prusti_post_item_apply_row_by_row_rec_6dfcf4781ca94d2d9de41f29d09aaa3c_Closure_0_snap(self) ==
    value


method p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_assign(self: Ref,
  value: s_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0)
  ensures acc(p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0(self), write)
  ensures p_prusti_post_item_apply_row_by_row_rec_ba67dc7492fe4a0480f90271a7a79f6d_Closure_0_snap(self) ==
    value