domain Array  {
  
  function loc(a: Array, i: Int): Ref 
  
  function len(a: Array): Int 
  
  function first(r: Ref): Array 
  
  function second(r: Ref): Int 
  
  axiom all_diff {
    (forall a: Array, i: Int ::
      { loc(a, i) }
      first(loc(a, i)) == a && second(loc(a, i)) == i)
  }
  
  axiom len_nonneg {
    (forall a: Array :: { len(a) } len(a) >= 0)
  }
}

domain Fold[A, V, B]  {
  
  function hfold(r: Receiver[A], m: Mapping[V, B], op: Operator[B]): Fold[A, V, B] 
  
  function hfoldApply(c: Fold[A, V, B], snap: Map[A,B]): B 
  
  function hfoldApply1(c: Fold[A, V, B], snap: Map[A,B]): B 
  
  function getreceiver(c: Fold[A, V, B]): Receiver[A] 
  
  function getoperator(c: Fold[A, V, B]): Operator[B] 
  
  function getmapping(c: Fold[A, V, B]): Mapping[V, B] 
  
  function dummy1(a: B): Bool 
  
  function _triggerDeleteBlock(applyC: B, block: Set[A]): Bool 
  
  function _triggerDeleteKey1(applyC: B, key: A): Bool 
  
  function exhaleCompMap(c: Fold[A, V, B], m: Map[A,B], fieldID: Int): Bool 
  
  function getSnapFieldID(m: Map[A,B]): Int 
  
  axiom applyComp1Eq {
    (forall __fold_c: Fold[A, V, B], __fold_snap: Map[A,B] ::
      { (hfoldApply(__fold_c, __fold_snap): B) }
      (hfoldApply(__fold_c, __fold_snap): B) ==
      (hfoldApply1(__fold_c, __fold_snap): B))
  }
  
  axiom _invAxFold {
    (forall __fold_r: Receiver[A], __fold_m: Mapping[V, B], __fold_o: Operator[B] ::
      { (hfold(__fold_r, __fold_m, __fold_o): Fold[A, V, B]) }
      (getreceiver((hfold(__fold_r, __fold_m, __fold_o): Fold[A, V, B])): Receiver[A]) ==
      __fold_r &&
      ((getmapping((hfold(__fold_r, __fold_m, __fold_o): Fold[A, V, B])): Mapping[V, B]) ==
      __fold_m &&
      (getoperator((hfold(__fold_r, __fold_m, __fold_o): Fold[A, V, B])): Operator[B]) ==
      __fold_o))
  }
  
  axiom _emptyFold {
    (forall __fold_c: Fold[A, V, B], __fold_snap: Map[A,B] ::
      { (hfoldApply(__fold_c, __fold_snap): B) }
      domain(__fold_snap) == Set[A]() ==>
      domain(__fold_snap) == Set[A]() &&
      (hfoldApply(__fold_c, __fold_snap): B) ==
      (opGetIden((getoperator(__fold_c): Operator[B])): B))
  }
  
  axiom _singleton {
    (forall __fold_c: Fold[A, V, B], __fold_snap: Map[A,B], __fold_elem: A ::
      { (hfoldApply(__fold_c, __fold_snap): B), Set(__fold_elem) }
      domain(__fold_snap) == Set(__fold_elem) ==>
      domain(__fold_snap) == Set(__fold_elem) &&
      (hfoldApply(__fold_c, __fold_snap): B) == __fold_snap[__fold_elem])
  }
  
  axiom _dropOne1 {
    (forall __fold_c: Fold[A, V, B], __fold_snap1: Map[A,B], __fold_key: A ::
      { (_triggerDeleteKey1((hfoldApply(__fold_c, __fold_snap1): B), __fold_key): Bool) }
      (__fold_key in domain(__fold_snap1)) ==>
      (__fold_key in domain(__fold_snap1)) &&
      (hfoldApply(__fold_c, __fold_snap1): B) ==
      (opApply((getoperator(__fold_c): Operator[B]), (hfoldApply1(__fold_c,
      (mapDelete(__fold_snap1, Set(__fold_key)): Map[A,B])): B), __fold_snap1[__fold_key]): B))
  }
  
  axiom loseMany {
    (forall __fold_c: Fold[A, V, B], __fold_snap1: Map[A,B], __fold_keys: Set[A] ::
      { (_triggerDeleteBlock((hfoldApply(__fold_c, __fold_snap1): B), __fold_keys): Bool) }
      (__fold_keys subset domain(__fold_snap1)) ==>
      (__fold_keys subset domain(__fold_snap1)) &&
      (hfoldApply(__fold_c, __fold_snap1): B) ==
      (opApply((getoperator(__fold_c): Operator[B]), (hfoldApply1(__fold_c,
      (mapDelete(__fold_snap1, __fold_keys): Map[A,B])): B), (hfoldApply1(__fold_c,
      (mapSubmap(__fold_snap1, __fold_keys): Map[A,B])): B)): B))
  }
}

domain Receiver[A]  {
  
  function recApply(r: Receiver[A], a: A): Ref 
  
  function recInv(rec: Receiver[A], ref: Ref): A 
  
  function filterReceiverGood(f: Set[A], r: Receiver[A]): Bool 
  
  function filterNotLost(f1: Set[A], r: Receiver[A], lostR: Set[Ref]): Set[A] 
  
  axiom _inverse_receiver {
    (forall __fold_a: A, __fold_f: Set[A], __fold_r: Receiver[A] ::
      { (recApply(__fold_r, __fold_a): Ref), (filterReceiverGood(__fold_f, __fold_r): Bool) }
      { (filterReceiverGood(__fold_f, __fold_r): Bool), (__fold_a in
      __fold_f) }
      (filterReceiverGood(__fold_f, __fold_r): Bool) &&
      (__fold_a in __fold_f) ==>
      (filterReceiverGood(__fold_f, __fold_r): Bool) &&
      ((__fold_a in __fold_f) &&
      (recInv(__fold_r, (recApply(__fold_r, __fold_a): Ref)): A) ==
      __fold_a))
  }
  
  axiom _inverse_receiver1 {
    (forall __fold_ref: Ref, __fold_f: Set[A], __fold_r: Receiver[A] ::
      { (filterReceiverGood(__fold_f, __fold_r): Bool), (recInv(__fold_r, __fold_ref): A) }
      (filterReceiverGood(__fold_f, __fold_r): Bool) &&
      ((recInv(__fold_r, __fold_ref): A) in __fold_f) ==>
      (filterReceiverGood(__fold_f, __fold_r): Bool) &&
      (((recInv(__fold_r, __fold_ref): A) in __fold_f) &&
      (recApply(__fold_r, (recInv(__fold_r, __fold_ref): A)): Ref) ==
      __fold_ref))
  }
  
  axiom smallerF {
    (forall __fold_f1: Set[A], __fold_f2: Set[A], __fold_r: Receiver[A] ::
      { (__fold_f2 subset __fold_f1), (filterReceiverGood(__fold_f1, __fold_r): Bool) }
      (filterReceiverGood(__fold_f1, __fold_r): Bool) &&
      (__fold_f2 subset __fold_f1) ==>
      (filterReceiverGood(__fold_f1, __fold_r): Bool) &&
      ((__fold_f2 subset __fold_f1) &&
      (filterReceiverGood(__fold_f2, __fold_r): Bool)))
  }
  
  axiom smallerFDelete {
    (forall __fold_f1: Set[A], __fold_f2: Set[A], __fold_r: Receiver[A] ::
      { (filterReceiverGood(__fold_f1, __fold_r): Bool), (__fold_f1 setminus
      __fold_f2) }
      (filterReceiverGood(__fold_f1, __fold_r): Bool) ==>
      (filterReceiverGood(__fold_f1, __fold_r): Bool) &&
      (filterReceiverGood((__fold_f1 setminus __fold_f2), __fold_r): Bool))
  }
  
  axiom unionF {
    (forall __fold_f1: Set[A], __fold_f2: Set[A], __fold_r: Receiver[A] ::
      { (filterReceiverGood((__fold_f1 union __fold_f2), __fold_r): Bool) }
      (filterReceiverGood((__fold_f1 union __fold_f2), __fold_r): Bool) ==>
      (filterReceiverGood((__fold_f1 union __fold_f2), __fold_r): Bool) &&
      ((filterReceiverGood(__fold_f1, __fold_r): Bool) &&
      (filterReceiverGood(__fold_f2, __fold_r): Bool)))
  }
  
  axiom _filterNotLostAxiom {
    (forall __fold_a: A, __fold_fs: Set[A], __fold_r: Receiver[A], __fold_lostR: Set[Ref] ::
      { (__fold_a in
      (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set[A])) }
      (__fold_a in
      (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set[A])) ==
      ((__fold_a in __fold_fs) &&
      !(((recApply(__fold_r, __fold_a): Ref) in __fold_lostR))))
  }
  
  axiom _filterNotLostSubset {
    (forall __fold_fs: Set[A], __fold_r: Receiver[A], __fold_lostR: Set[Ref] ::
      { (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set[A]) }
      ((filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set[A]) subset
      __fold_fs))
  }
}

domain Operator[B]  {
  
  function _noTrigOp(out: B): Bool 
  
  function opApply(op: Operator[B], val1: B, val2: B): B 
  
  function opGetIden(op: Operator[B]): B 
}

domain Mapping[V, B]  {
  
  function mapApply(m: Mapping[V, B], _mInput: V): B 
  
  function mapIdentity(): Mapping[V, V] 
  
  axiom {
    (forall __v: V ::
      { (mapApply((mapIdentity(): Mapping[V, V]), __v): V) }
      (mapApply((mapIdentity(): Mapping[V, V]), __v): V) == __v)
  }
}

domain MapEdit[A, B]  {
  
  function mapDelete(m: Map[A,B], e: Set[A]): Map[A,B] 
  
  function mapSubmap(m: Map[A,B], es: Set[A]): Map[A,B] 
  
  function disjUnionEq(s1: Set[A], s2: Set[A], s3: Set[A]): Bool 
  
  axiom disjUnionEqDef {
    (forall __fold_s1: Set[A], __fold_s2: Set[A], __fold_s3: Set[A] ::
      { (disjUnionEq(__fold_s1, __fold_s2, __fold_s3): Bool) }
      (disjUnionEq(__fold_s1, __fold_s2, __fold_s3): Bool) ==
      ((__fold_s1 intersection __fold_s2) == Set[A]() &&
      (__fold_s1 union __fold_s2) == __fold_s3))
  }
}

domain setFunc[A]  {
  
  axiom setminusAssoc {
    (forall __fold_s1: Set[A], __fold_s2: Set[A], __fold_s3: Set[A] ::
      { ((__fold_s1 setminus __fold_s2) setminus __fold_s3) }
      ((__fold_s1 setminus __fold_s2) setminus __fold_s3) ==
      ((__fold_s1 setminus __fold_s3) setminus __fold_s2))
  }
  
  axiom setminusRepeated {
    (forall __fold_s1: Set[A], __fold_s2: Set[A] ::
      { ((__fold_s1 setminus __fold_s2) setminus __fold_s2) }
      ((__fold_s1 setminus __fold_s2) setminus __fold_s2) ==
      (__fold_s1 setminus __fold_s2))
  }
  
  axiom _emptySubset {
    (forall __fold_s1: Set[A], __fold_s2: Set[A] ::
      { (__fold_s2 subset __fold_s1) }
      __fold_s1 == Set[A]() ==>
      (__fold_s2 subset __fold_s1) == (__fold_s2 == Set[A]()))
  }
}

domain ___arrayRec_Receiver_Domain  {
  
  function arrayRec(a: Array): Receiver[Int] 
  
  axiom {
    (forall a: Array, i: Int ::
      { (recApply(arrayRec(a), i): Ref) }
      { loc(a, i) }
      (recApply(arrayRec(a), i): Ref) == loc(a, i))
  }
}

domain ___allInt_Filter_Domain  {
  
  function allInt(start: Int, end: Int): Set[Int] 
  
  axiom {
    (forall start: Int, end: Int, i: Int ::
      { (i in allInt(start, end)) }
      (i in allInt(start, end)) == (i >= start && i < end))
  }
}

domain ___add_Operator_Domain  {
  
  function add(): Operator[Int] 
  
  axiom {
    (forall a: Int, b: Int ::
      { (opApply(add(), a, b): Int) }
      (opApply(add(), a, b): Int) == a + b)
  }
  
  axiom {
    (opGetIden(add()): Int) == 0
  }
}

field val: Int

function __snap_Int_Int_Int_val(c: Fold[Int, Int, Int], f: Set[Int]): Map[Int,Int]
  requires [(filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool),
    (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool) ||
    (forall __ind1: Int, __ind2: Int ::
      { (__ind1 in f), (__ind2 in f) }
      (__ind1 in f) && ((__ind2 in f) && __ind1 != __ind2) ==>
      (recApply((getreceiver(c): Receiver[Int]), __ind1): Ref) !=
      (recApply((getreceiver(c): Receiver[Int]), __ind2): Ref))]
  requires (forall __ind: Int ::
      { (__ind in f) }
      (__ind in f) ==>
      acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 /
      10))
  ensures (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool)
  ensures domain(result) == f
  ensures (forall __ind: Int ::
      { result[__ind] }
      (__ind in f) ==>
      result[__ind] ==
      (mapApply((getmapping(c): Mapping[Int, Int]), (recApply((getreceiver(c): Receiver[Int]),
      __ind): Ref).val): Int))
  ensures (forall __s: Set[Int] ::
      { (mapDelete(result, __s): Map[Int,Int]) }
      __s != Set[Int]() ==>
      __snap_Int_Int_Int_val_prime(c, (f setminus __s)) ==
      (mapDelete(result, __s): Map[Int,Int]))
  ensures (forall __s: Set[Int] ::
      { (mapSubmap(result, __s): Map[Int,Int]) }
      (__s subset f) && __s != f ==>
      (__s subset f) &&
      (__s != f &&
      __snap_Int_Int_Int_val_prime(c, __s) ==
      (mapSubmap(result, __s): Map[Int,Int])))
  ensures (forall __s1: Set[Int], __s2: Set[Int] ::
      { (disjUnionEq(__s1, __s2, f): Bool) }
      (disjUnionEq(__s1, __s2, f): Bool) ==>
      (disjUnionEq(__s1, __s2, f): Bool) &&
      (hfoldApply1(c, result): Int) ==
      (opApply((getoperator(c): Operator[Int]), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c,
      __s1)): Int), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s2)): Int)): Int))
  ensures (forall __s: Set[Int] ::
      { (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s)): Int) }
      (dummy1(__s == f): Bool))
  ensures result == __snap_Int_Int_Int_val_prime(c, f)
  ensures (getSnapFieldID(result): Int) == 0


function __snap_Int_Int_Int_val_prime(c: Fold[Int, Int, Int], f: Set[Int]): Map[Int,Int]
  requires (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool)
  requires (forall __ind: Int ::
      { (__ind in f) }
      (__ind in f) ==>
      acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 /
      10))
  ensures (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool)


method operator_add_welldef_check()
{
  assert (forall _i1: Int, _i2: Int ::
      { (_noTrigOp((opApply((add(): Operator[Int]), _i1, _i2): Int)): Bool) }
      (opApply((add(): Operator[Int]), _i1, _i2): Int) ==
      (opApply((add(): Operator[Int]), _i2, _i1): Int))
  assert (forall _i1: Int, _i2: Int, _i3: Int ::
      { (_noTrigOp((opApply((add(): Operator[Int]), (opApply((add(): Operator[Int]),
      _i1, _i2): Int), _i3): Int)): Bool) }
      (opApply((add(): Operator[Int]), (opApply((add(): Operator[Int]), _i1,
      _i2): Int), _i3): Int) ==
      (opApply((add(): Operator[Int]), _i1, (opApply((add(): Operator[Int]),
      _i2, _i3): Int)): Int))
  assert (forall _i1: Int ::
      { (_noTrigOp((opApply((add(): Operator[Int]), _i1, (opGetIden((add(): Operator[Int])): Int)): Int)): Bool) }
      (opApply((add(): Operator[Int]), _i1, (opGetIden((add(): Operator[Int])): Int)): Int) ==
      _i1)
}

method test1(a: Array)
  requires (forall j: Int ::
      { loc(a, j) }
      0 <= j && j < len(a) ==> acc(loc(a, j).val, write))
  requires len(a) > 10
{
  var js: Set[Int]
  var is: Set[Int]
  var j1: Int
  var j2: Int
  var j3: Int
  var i1: Int
  var i2: Int
  var i3: Int
  var i4: Int
  var i5: Int
  var i6: Int
  label _compLabell0
  inhale (js subset allInt(0, len(a)))
  inhale (is subset allInt(0, len(a)))
  inhale (j1 in js)
  inhale (j2 in js)
  inhale (j3 in js)
  inhale (i1 in is)
  inhale (i2 in is)
  inhale (i3 in is)
  inhale (i4 in is)
  inhale (i5 in is)
  inhale (i6 in is)
  loc(a, i1).val := loc(a, i1).val + 1
  label _compLabell1
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool)))
  loc(a, j1).val := loc(a, j1).val + 1
  label _compLabell2
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool)))
  loc(a, i2).val := loc(a, i2).val + 1
  label _compLabell3
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool)))
  loc(a, i3).val := loc(a, i3).val + 1
  label _compLabell4
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool)))
  loc(a, j2).val := loc(a, j2).val + 1
  label _compLabell5
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool)))
  loc(a, i4).val := loc(a, i4).val + 1
  label _compLabell6
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool)))
  loc(a, i5).val := loc(a, i5).val + 1
  label _compLabell7
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool)))
  loc(a, j3).val := loc(a, j3).val + 1
  label _compLabell8
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool)))
  loc(a, i6).val := loc(a, i6).val + 1
  label _compLabell9
  inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
      { old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
      { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      (forall __ind: Int ::
        { (__ind in __f) }
        (__ind in __f) ==>
        perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
        none) ==>
      (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
      ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
      (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool) &&
      (_triggerDeleteKey1(old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
      __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool)))
  inhale (js intersection is) == Set[Int]()
  assert (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]),
    add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a),
    (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int) ==
    old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]),
    add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a),
    (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int)) +
    3
}