domain Equality[T]  {
  
  function eq(l: T, r: T): Bool 
  
  axiom {
    (forall l: T, r: T ::
      { (eq(l, r): Bool) }
      (eq(l, r): Bool) == (l == r))
  }
}

domain IntWellFoundedOrder  {
  
  axiom integer_ax_bound {
    (forall int1: Int ::
      { (bounded(int1): Bool) }
      int1 >= 0 ==> (bounded(int1): Bool))
  }
  
  axiom integer_ax_dec {
    (forall int1: Int, int2: Int ::
      { (decreasing(int1, int2): Bool) }
      int1 < int2 ==> (decreasing(int1, int2): Bool))
  }
}

domain PredicateInstance  {
  
  
}

domain PredicateInstancesNestedRelation  {
  
  function nestedPredicates(l1: PredicateInstance, l2: PredicateInstance): Bool 
  
  axiom nestedReflex {
    (forall l1: PredicateInstance ::!nestedPredicates(l1, l1))
  }
  
  axiom nestedTrans {
    (forall l1: PredicateInstance, l2: PredicateInstance, l3: PredicateInstance ::
      { nestedPredicates(l1, l2), nestedPredicates(l2, l3) }
      nestedPredicates(l1, l2) && nestedPredicates(l2, l3) ==>
      nestedPredicates(l1, l3))
  }
}

domain PredicateInstancesWellFoundedOrder  {
  
  axiom predicate_instances_ax_bound {
    (forall l1: PredicateInstance ::
      { (bounded(l1): Bool) }
      (bounded(l1): Bool))
  }
  
  axiom predicate_instances_ax_dec {
    (forall l1: PredicateInstance, l2: PredicateInstance ::
      { nestedPredicates(l1, l2) }
      (decreasing(l1, l2): Bool) == nestedPredicates(l1, l2))
  }
}

domain ShArray[T]  {
  
  function ShArrayfirst(r: T): ShArray[T] 
  
  function ShArraylen(a: ShArray[T]): Int 
  
  function ShArrayloc(a: ShArray[T], i: Int): T 
  
  function ShArraysecond(r: T): Int 
  
  axiom {
    (forall a: ShArray[T] ::
      { (ShArraylen(a): Int) }
      (ShArraylen(a): Int) >= 0)
  }
  
  axiom {
    (forall a: ShArray[T], i: Int ::
      { (ShArrayloc(a, i): T) }
      0 <= i && i < (ShArraylen(a): Int) ==>
      (ShArrayfirst((ShArrayloc(a, i): T)): ShArray[T]) == a &&
      (ShArraysecond((ShArrayloc(a, i): T)): Int) == i)
  }
}

domain ShStruct4[T0, T1, T2, T3]  {
  
  function ShStructget0of4(x: ShStruct4[T0, T1, T2, T3]): T0 
  
  function ShStructget1of4(x: ShStruct4[T0, T1, T2, T3]): T1 
  
  function ShStructget2of4(x: ShStruct4[T0, T1, T2, T3]): T2 
  
  function ShStructget3of4(x: ShStruct4[T0, T1, T2, T3]): T3 
  
  function ShStructrev0of4(v0: T0): ShStruct4[T0, T1, T2, T3] 
  
  function ShStructrev1of4(v1: T1): ShStruct4[T0, T1, T2, T3] 
  
  function ShStructrev2of4(v2: T2): ShStruct4[T0, T1, T2, T3] 
  
  function ShStructrev3of4(v3: T3): ShStruct4[T0, T1, T2, T3] 
  
  axiom {
    (forall x: ShStruct4[T0, T1, T2, T3] ::
      { (ShStructget0of4(x): T0) }
      (ShStructrev0of4((ShStructget0of4(x): T0)): ShStruct4[T0, T1, T2, T3]) ==
      x)
  }
  
  axiom {
    (forall x: ShStruct4[T0, T1, T2, T3] ::
      { (ShStructget1of4(x): T1) }
      (ShStructrev1of4((ShStructget1of4(x): T1)): ShStruct4[T0, T1, T2, T3]) ==
      x)
  }
  
  axiom {
    (forall x: ShStruct4[T0, T1, T2, T3] ::
      { (ShStructget2of4(x): T2) }
      (ShStructrev2of4((ShStructget2of4(x): T2)): ShStruct4[T0, T1, T2, T3]) ==
      x)
  }
  
  axiom {
    (forall x: ShStruct4[T0, T1, T2, T3] ::
      { (ShStructget3of4(x): T3) }
      (ShStructrev3of4((ShStructget3of4(x): T3)): ShStruct4[T0, T1, T2, T3]) ==
      x)
  }
  
  axiom {
    (forall x: ShStruct4[T0, T1, T2, T3], y: ShStruct4[T0, T1, T2, T3] ::
      { (eq(x, y): Bool) }
      (eq(x, y): Bool) ==
      ((ShStructget0of4(x): T0) == (ShStructget0of4(y): T0) &&
      (ShStructget1of4(x): T1) == (ShStructget1of4(y): T1) &&
      (ShStructget2of4(x): T2) == (ShStructget2of4(y): T2) &&
      (ShStructget3of4(x): T3) == (ShStructget3of4(y): T3)))
  }
}

domain Slice[T]  {
  
  function sarray(s: Slice[T]): ShArray[T] 
  
  function scap(s: Slice[T]): Int 
  
  function slen(s: Slice[T]): Int 
  
  function smake(a: ShArray[T], o: Int, l: Int, c: Int): Slice[T] 
  
  function soffset(s: Slice[T]): Int 
  
  axiom deconstructor_over_constructor_array {
    (forall a: ShArray[T], o: Int, l: Int, c: Int ::
      { (sarray((smake(a, o, l, c): Slice[T])): ShArray[T]) }
      0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
      (sarray((smake(a, o, l, c): Slice[T])): ShArray[T]) == a)
  }
  
  axiom deconstructor_over_constructor_cap {
    (forall a: ShArray[T], o: Int, l: Int, c: Int ::
      { (scap((smake(a, o, l, c): Slice[T])): Int) }
      0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
      (scap((smake(a, o, l, c): Slice[T])): Int) == c)
  }
  
  axiom deconstructor_over_constructor_len {
    (forall a: ShArray[T], o: Int, l: Int, c: Int ::
      { (slen((smake(a, o, l, c): Slice[T])): Int) }
      0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
      (slen((smake(a, o, l, c): Slice[T])): Int) == l)
  }
  
  axiom deconstructor_over_constructor_offset {
    (forall a: ShArray[T], o: Int, l: Int, c: Int ::
      { (soffset((smake(a, o, l, c): Slice[T])): Int) }
      0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
      (soffset((smake(a, o, l, c): Slice[T])): Int) == o)
  }
  
  axiom {
    (forall s: Slice[T] ::
      { (sarray(s): ShArray[T]) }
      { (soffset(s): Int) }
      { (slen(s): Int) }
      { (scap(s): Int) }
      s ==
      (smake((sarray(s): ShArray[T]), (soffset(s): Int), (slen(s): Int), (scap(s): Int)): Slice[T]))
  }
  
  axiom {
    (forall s: Slice[T] ::
      { (slen(s): Int) }
      { (scap(s): Int) }
      (slen(s): Int) <= (scap(s): Int))
  }
  
  axiom {
    (forall s: Slice[T] ::
      { (soffset(s): Int), (scap(s): Int) }
      { (ShArraylen((sarray(s): ShArray[T])): Int) }
      (soffset(s): Int) + (scap(s): Int) <=
      (ShArraylen((sarray(s): ShArray[T])): Int))
  }
  
  axiom {
    (forall s: Slice[T] :: { (slen(s): Int) } 0 <= (slen(s): Int))
  }
  
  axiom {
    (forall s: Slice[T] :: { (soffset(s): Int) } 0 <= (soffset(s): Int))
  }
}

domain String  {
  
  function strConcat(l: Int, r: Int): Int 
  
  function strLen(id: Int): Int 
  
  unique function stringLit(): Int 
  
  axiom {
    (forall l: Int, r: Int ::
      { strLen(strConcat(l, r)) }
      strLen(strConcat(l, r)) == strLen(l) + strLen(r))
  }
  
  axiom {
    (forall str: Int :: { strLen(str) } 0 <= strLen(str))
  }
  
  axiom {
    strLen(stringLit()) == 0
  }
}

domain Tuple2[T0, T1]  {
  
  function get0of2(p: Tuple2[T0, T1]): T0 
  
  function get1of2(p: Tuple2[T0, T1]): T1 
  
  function tuple2(t0: T0, t1: T1): Tuple2[T0, T1] 
  
  axiom getter_over_tuple2 {
    (forall t0: T0, t1: T1 ::
      { (tuple2(t0, t1): Tuple2[T0, T1]) }
      (get0of2((tuple2(t0, t1): Tuple2[T0, T1])): T0) == t0 &&
      (get1of2((tuple2(t0, t1): Tuple2[T0, T1])): T1) == t1)
  }
  
  axiom tuple2_over_getter {
    (forall p: Tuple2[T0, T1] ::
      { (get0of2(p): T0) }
      { (get1of2(p): T1) }
      (tuple2((get0of2(p): T0), (get1of2(p): T1)): Tuple2[T0, T1]) == p)
  }
}

domain Tuple4[T0, T1, T2, T3]  {
  
  function get0of4(p: Tuple4[T0, T1, T2, T3]): T0 
  
  function get1of4(p: Tuple4[T0, T1, T2, T3]): T1 
  
  function get2of4(p: Tuple4[T0, T1, T2, T3]): T2 
  
  function get3of4(p: Tuple4[T0, T1, T2, T3]): T3 
  
  function tuple4(t0: T0, t1: T1, t2: T2, t3: T3): Tuple4[T0, T1, T2, T3] 
  
  axiom getter_over_tuple4 {
    (forall t0: T0, t1: T1, t2: T2, t3: T3 ::
      { (tuple4(t0, t1, t2, t3): Tuple4[T0, T1, T2, T3]) }
      (get0of4((tuple4(t0, t1, t2, t3): Tuple4[T0, T1, T2, T3])): T0) == t0 &&
      (get1of4((tuple4(t0, t1, t2, t3): Tuple4[T0, T1, T2, T3])): T1) == t1 &&
      (get2of4((tuple4(t0, t1, t2, t3): Tuple4[T0, T1, T2, T3])): T2) == t2 &&
      (get3of4((tuple4(t0, t1, t2, t3): Tuple4[T0, T1, T2, T3])): T3) == t3)
  }
  
  axiom tuple4_over_getter {
    (forall p: Tuple4[T0, T1, T2, T3] ::
      { (get0of4(p): T0) }
      { (get1of4(p): T1) }
      { (get2of4(p): T2) }
      { (get3of4(p): T3) }
      (tuple4((get0of4(p): T0), (get1of4(p): T1), (get2of4(p): T2), (get3of4(p): T3)): Tuple4[T0, T1, T2, T3]) ==
      p)
  }
}

domain Types  {
  
  function behavioral_subtype_Types(l: Types, r: Types): Bool 
  
  function comparableType_Types(t: Types): Bool 
  
  function empty_interface_Types(): Types 
  
  unique function empty_interface_Types_tag(): Int 
  
  function nil_Types(): Types 
  
  unique function nil_Types_tag(): Int 
  
  function tag_Types(t: Types): Int 
  
  axiom {
    (forall a: Types ::
      { behavioral_subtype_Types(a, a) }
      behavioral_subtype_Types(a, a))
  }
  
  axiom {
    (forall a: Types ::
      { behavioral_subtype_Types(a, empty_interface_Types()) }
      behavioral_subtype_Types(a, empty_interface_Types()))
  }
  
  axiom {
    (forall a: Types, b: Types, c: Types ::
      { behavioral_subtype_Types(a, b), behavioral_subtype_Types(b, c) }
      behavioral_subtype_Types(a, b) && behavioral_subtype_Types(b, c) ==>
      behavioral_subtype_Types(a, c))
  }
  
  axiom {
    comparableType_Types(empty_interface_Types()) == false
  }
  
  axiom {
    comparableType_Types(nil_Types()) == true
  }
  
  axiom {
    tag_Types(empty_interface_Types()) == empty_interface_Types_tag()
  }
  
  axiom {
    tag_Types(nil_Types()) == nil_Types_tag()
  }
}

domain WellFoundedOrder[T]  {
  
  function bounded(arg1: T): Bool 
  
  function decreasing(arg1: T, arg2: T): Bool 
}

field PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$: ShStruct4[Ref, Ref, Ref, Ref]

field SliceString$$$_S_$$$$$$$_E_$$$: Slice[Ref]

field String$$$$_E_$$$: Int

function IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf: Tuple2[Ref, Types]): Bool
  requires !(thisItf == (tuple2(null, nil_Types()): Tuple2[Ref, Types]))
  requires acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), wildcard)
  decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf)


function sadd(left: Int, right: Int): Int
  ensures result == left + right
  decreases
{
  left + right
}

function sconstruct_Ref(a: ShArray[Ref], offset: Int, len: Int, cap: Int): Slice[Ref]
  requires 0 <= offset
  requires 0 <= len
  requires len <= cap
  requires offset + cap <= (ShArraylen(a): Int)
  ensures (sarray(result): ShArray[Ref]) == a
  ensures (soffset(result): Int) == offset
  ensures (slen(result): Int) == len
  ensures (scap(result): Int) == cap
  decreases _


function sfullSliceFromArray_Ref(a: ShArray[Ref], i: Int, j: Int, k: Int): Slice[Ref]
  requires 0 <= i
  requires i <= j
  requires j <= k
  requires k <= (ShArraylen(a): Int)
  ensures (soffset(result): Int) == i
  ensures (slen(result): Int) == j - i
  ensures (scap(result): Int) == k - i
  ensures (sarray(result): ShArray[Ref]) == a
  decreases _


function sfullSliceFromSlice_Ref(s: Slice[Ref], i: Int, j: Int, k: Int): Slice[Ref]
  requires 0 <= i
  requires i <= j
  requires j <= k
  requires k <= (scap(s): Int)
  ensures (soffset(result): Int) == (soffset(s): Int) + i
  ensures (slen(result): Int) == j - i
  ensures (scap(result): Int) == k - i
  ensures (sarray(result): ShArray[Ref]) == (sarray(s): ShArray[Ref])
  decreases _


function ssliceFromSlice_Ref(s: Slice[Ref], i: Int, j: Int): Slice[Ref]
  requires 0 <= i
  requires i <= j
  requires j <= (scap(s): Int)
  ensures (soffset(result): Int) == (soffset(s): Int) + i
  ensures (slen(result): Int) == j - i
  ensures (scap(result): Int) == (scap(s): Int) - i
  ensures (sarray(result): ShArray[Ref]) == (sarray(s): ShArray[Ref])
  decreases _


function toAbstractChain2_97009f8b_F(bars_V0: Slice[Ref], perms_V0: Perm): Seq[Tuple4[Seq[Int], Seq[Int], Seq[Int], Seq[Int]]]
  requires perms_V0 > 0 / 1
  requires (forall k_V1: Int ::
      { (ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
      k_V1)): Ref) }
      0 <= k_V1 && k_V1 < (slen(bars_V0): Int) ==>
      acc((ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
      k_V1)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$, write))
  requires (forall k_V2: Int ::
      { (ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
      k_V2)): Ref) }
      0 <= k_V2 && k_V2 < (slen(bars_V0): Int) ==>
      acc(PredBar_97009f8b_F((ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
      k_V2)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$, (slen(bars_V0): Int) -
      k_V2 -
      1), perms_V0))
  ensures (slen(bars_V0): Int) == |result|
  ensures (forall k_V3: Int ::
      { (get0of4(result[k_V3]): Seq[Int]) }
      0 <= k_V3 && k_V3 < (slen(bars_V0): Int) ==>
      (unfolding acc(PredBar_97009f8b_F((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
        sadd((soffset(bars_V0): Int), k_V3)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$,
        (slen(bars_V0): Int) - k_V3 - 1), perms_V0) in
        (unfolding acc(acc_strs_97009f8b_F((ShStructget0of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V3)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$), perms_V0) in
          toSeq2_97009f8b_F((ShStructget0of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V3)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$)) ==
        (get0of4(result[k_V3]): Seq[Int])))
  ensures (forall k_V4: Int ::
      { (get1of4(result[k_V4]): Seq[Int]) }
      0 <= k_V4 && k_V4 < (slen(bars_V0): Int) ==>
      (unfolding acc(PredBar_97009f8b_F((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
        sadd((soffset(bars_V0): Int), k_V4)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$,
        (slen(bars_V0): Int) - k_V4 - 1), perms_V0) in
        (unfolding acc(acc_strs_97009f8b_F((ShStructget1of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V4)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$), perms_V0) in
          toSeq2_97009f8b_F((ShStructget1of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V4)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$)) ==
        (get1of4(result[k_V4]): Seq[Int])))
  ensures (forall k_V5: Int ::
      { (get2of4(result[k_V5]): Seq[Int]) }
      0 <= k_V5 && k_V5 < (slen(bars_V0): Int) ==>
      (unfolding acc(PredBar_97009f8b_F((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
        sadd((soffset(bars_V0): Int), k_V5)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$,
        (slen(bars_V0): Int) - k_V5 - 1), perms_V0) in
        (unfolding acc(acc_strs_97009f8b_F((ShStructget2of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V5)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$), perms_V0) in
          toSeq2_97009f8b_F((ShStructget2of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V5)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$)) ==
        (get2of4(result[k_V5]): Seq[Int])))
  ensures (forall k_V6: Int ::
      { (get3of4(result[k_V6]): Seq[Int]) }
      0 <= k_V6 && k_V6 < (slen(bars_V0): Int) ==>
      (unfolding acc(PredBar_97009f8b_F((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
        sadd((soffset(bars_V0): Int), k_V6)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$,
        (slen(bars_V0): Int) - k_V6 - 1), perms_V0) in
        (unfolding acc(acc_strs_97009f8b_F((ShStructget3of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V6)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$), perms_V0) in
          toSeq2_97009f8b_F((ShStructget3of4((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
          sadd((soffset(bars_V0): Int), k_V6)): Ref).PointerDefinedBar_97009f8b_T$$$_S_$$$$$$$_E_$$$): Ref).SliceString$$$_S_$$$$$$$_E_$$$)) ==
        (get3of4(result[k_V6]): Seq[Int])))
  decreases


function toSeq2_97009f8b_F(s_V0: Slice[Ref]): Seq[Int]
  requires (forall j_V1: Int ::
      { (ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
      j_V1)): Ref) }
      0 <= j_V1 && j_V1 < (slen(s_V0): Int) ==>
      acc((ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
      j_V1)): Ref).String$$$$_E_$$$, write))
  ensures |result| == (slen(s_V0): Int)
  ensures (forall j_V2: Int ::
      { (ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
      j_V2)): Ref).String$$$$_E_$$$ }
      { result[j_V2] }
      0 <= j_V2 && j_V2 < (slen(s_V0): Int) ==>
      (ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int), j_V2)): Ref).String$$$$_E_$$$ ==
      result[j_V2])
  decreases (slen(s_V0): Int)
{
  ((slen(s_V0): Int) == 0 ?
    Seq[Int]() :
    toSeq2_97009f8b_F(ssliceFromSlice_Ref(s_V0, 0, (slen(s_V0): Int) - 1)) ++
    Seq((ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
    (slen(s_V0): Int) - 1)): Ref).String$$$$_E_$$$))
}

predicate ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf: Tuple2[Ref, Types]) 

predicate PredBar_97009f8b_F(bar_V0: ShStruct4[Ref, Ref, Ref, Ref], k_V0: Int) {
  (let fn$$0 ==
    (bar_V0) in
    acc((ShStructget0of4(fn$$0): Ref).SliceString$$$_S_$$$$$$$_E_$$$, write) &&
    acc((ShStructget1of4(fn$$0): Ref).SliceString$$$_S_$$$$$$$_E_$$$, write) &&
    acc((ShStructget2of4(fn$$0): Ref).SliceString$$$_S_$$$$$$$_E_$$$, write) &&
    acc((ShStructget3of4(fn$$0): Ref).SliceString$$$_S_$$$$$$$_E_$$$, write)) &&
  acc(acc_strs_97009f8b_F((ShStructget0of4(bar_V0): Ref).SliceString$$$_S_$$$$$$$_E_$$$), write) &&
  acc(acc_strs_97009f8b_F((ShStructget1of4(bar_V0): Ref).SliceString$$$_S_$$$$$$$_E_$$$), write) &&
  acc(acc_strs_97009f8b_F((ShStructget2of4(bar_V0): Ref).SliceString$$$_S_$$$$$$$_E_$$$), write) &&
  acc(acc_strs_97009f8b_F((ShStructget3of4(bar_V0): Ref).SliceString$$$_S_$$$$$$$_E_$$$), write)
}

predicate acc_strs_97009f8b_F(arr_V0: Slice[Ref]) {
  (forall k_V1: Int ::
    { (ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
    k_V1)): Ref) }
    0 <= k_V1 && k_V1 < (slen(arr_V0): Int) ==>
    acc((ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
    k_V1)): Ref).String$$$$_E_$$$, write))
}

method $INIT_97009f8b_ef412b23()
  decreases
{
  
  // decl 
  {
    
    
    label returnLabel
  }
}

method Duplicate_ad177c4e_SY$db8f20c_ad177c4e_(thisItf: Tuple2[Ref, Types])
  requires !(thisItf == (tuple2(null, nil_Types()): Tuple2[Ref, Types]))
  requires acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), write)
  ensures acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), write)
  ensures IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) ==
    old(IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf))
  ensures IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) ==>
    acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), write)
  decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf)


method Error_ad177c4e_SY$db8f20c_ad177c4e_(thisItf: Tuple2[Ref, Types])
  returns (P0_PO0: Int)
  requires !(thisItf == (tuple2(null, nil_Types()): Tuple2[Ref, Types]))
  requires acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), write)
  ensures acc(ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf), write)
  ensures IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) ==
    old(IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf))
  decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf)


method panic_ad177c4e_F(v_V0: Tuple2[Ref, Types])
  requires false