diff --git a/genericmonomap/monomap.gobra b/genericmonomap/monomap.gobra
index a8ec218..1cdd029 100644
--- a/genericmonomap/monomap.gobra
+++ b/genericmonomap/monomap.gobra
@@ -66,6 +66,21 @@ pure func (m MonoMap) ToDict() dict[Key]Val {
 		(m.inUse ? (let smallMap := MonoMap(m.next).ToDict() in smallMap[m.k = m.v]) : dict[Key]Val{})
 }
 
+ghost
+requires  m.Inv()
+decreases m.Inv()
+pure func (m MonoMap) KeySet() set[Key] {
+	return domain(m.ToDict())
+}
+
+ghost
+requires  m.Inv()
+requires  k elem domain(m.ToDict())
+decreases m.Inv()
+pure func (m MonoMap) Get(k Key) Val {
+	return let d := m.ToDict() in Val(d[k])
+}
+
 pred (m MonoMap) Witness(k Key, v Val) {
 	acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) &&
 	isComparable(k)                  &&
diff --git a/resalgebraNoAxioms/auth.gobra b/resalgebraNoAxioms/auth.gobra
new file mode 100644
index 0000000..8c68e36
--- /dev/null
+++ b/resalgebraNoAxioms/auth.gobra
@@ -0,0 +1,140 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+var _ RA = TypeAuthRA{}
+var AuthRA TypeAuthRA = TypeAuthRA{}
+
+type IntWithTopBot interface {}
+type Top struct{}
+type Bottom struct{}
+type Int struct {
+	V int
+}
+
+type AuthCarrier struct {
+	Fst IntWithTopBot
+	Snd int
+}
+
+type TypeAuthRA struct{}
+
+ghost
+decreases
+pure func AuthView(m int) Elem {
+	return AuthCarrier{Int{m}, 0}
+}
+
+ghost
+decreases
+pure func FragView(m int) Elem {
+	return AuthCarrier{Bottom{}, m}
+}
+
+
+ghost
+decreases
+pure func (ra TypeAuthRA) IsElem(e Elem) (res bool) {
+	return typeOf(e) == type[AuthCarrier] &&
+		let c := e.(AuthCarrier) in
+		c.Fst === Bottom{} ||
+		c.Fst === Top{}    ||
+		typeOf(c.Fst) == type[Int]
+}
+
+ghost
+requires ra.IsElem(e)
+decreases
+pure func (ra TypeAuthRA) IsValid(e Elem) bool {
+	return let x := e.(AuthCarrier) in
+		x.Fst === Bottom{} ||
+		(typeOf(x.Fst) == type[Int] && x.Fst.(Int).V >= x.Snd)
+}
+
+ghost
+requires ra.IsElem(e)
+ensures  res !== none[Elem] ==> ra.IsElem(get(res))
+decreases
+pure func (ra TypeAuthRA) Core(e Elem) (ghost res option[Elem]) {
+	return let x := e.(AuthCarrier) in
+		some(Elem(AuthCarrier{Bottom{}, x.Snd}))
+}
+
+ghost
+requires ra.IsElem(e1) && ra.IsElem(e2)
+ensures  ra.IsElem(res)
+decreases
+pure func (ra TypeAuthRA) Compose(e1 Elem, e2 Elem) (res Elem) {
+	return let c1 := e1.(AuthCarrier) in
+		let c2 := e2.(AuthCarrier)    in
+		(c1.Fst === Bottom{} ?
+			AuthCarrier{c2.Fst, max(c1.Snd, c2.Snd)} :
+			(c2.Fst === Bottom{} ?
+				AuthCarrier{c1.Fst, max(c1.Snd, c2.Snd)} :
+				AuthCarrier{Top{}, max(c1.Snd, c2.Snd)}))
+}
+
+ghost
+decreases
+pure func max(a int, b int) int {
+	return a > b ? a : b
+}
+
+// all lemmas proven automatically
+
+
+ghost
+decreases
+pure func (ra TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeAuthRA) ComposeComm(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeAuthRA) CoreId(e Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeAuthRA) CoreIdem(e Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeAuthRA) CoreMono(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeAuthRA) ValidOp(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
\ No newline at end of file
diff --git a/resalgebraNoAxioms/cooliomapio.gobra b/resalgebraNoAxioms/cooliomapio.gobra
new file mode 100644
index 0000000..becca86
--- /dev/null
+++ b/resalgebraNoAxioms/cooliomapio.gobra
@@ -0,0 +1,144 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+// map that can only grow monotically. adding a new element to the map
+// requires and ensures the map invariant, but checking that a key-pair value (or a key is in the map) is in the map
+// should not require the map inv
+
+ghost type key = LocName
+ghost type val = cooliosetio
+
+ghost type node ghost struct {
+	inUse bool
+	next gpointer[node]
+	k key
+	v val
+	p perm
+}
+
+// todo: change
+ghost type cooliomapio gpointer[node]
+
+pred inv(m cooliomapio) {
+	acc(m, 1/2) &&
+	(m.next == nil ==> !m.inUse && acc(m, 1/2)) &&
+	(m.next != nil ==> 
+		m.inUse &&
+		acc(&m.p, 1/2) &&
+		inv(m.next)    &&
+		m.p > 0        &&
+		acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.k, m.p) && acc(&m.v, m.p))
+}
+
+ghost
+mayInit
+ensures inv(m)
+ensures toDict(m) == dict[key]val{}
+decreases
+func allocMap() (m cooliomapio) {
+	var g@ node
+	fold inv(&g)
+	return &g
+}
+
+ghost
+requires inv(m)
+decreases inv(m)
+pure func toDict(m cooliomapio) dict[key]val {
+	return unfolding inv(m) in (m.inUse ? (let smallMap := toDict(m.next) in smallMap[m.k = m.v]) : dict[key]val{})
+}
+
+// ghost
+// requires witness(m, k)
+// decreases
+// pure func getVal(m cooliomapio, k key) val
+
+pred witness(m cooliomapio, k key, v val) {
+	acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) &&
+	(!m.inUse ==> false) &&
+	(m.k == k && m.v != v ==> false) &&
+	(m.k != k ==> witness(m.next, k, v))
+}
+
+ghost
+requires inv(m)
+requires !(k elem domain(toDict(m)))
+ensures  inv(m)
+ensures  witness(m, k, v)
+// ensures  getVal(m, k) === v
+ensures  toDict(m) === old(toDict(m))[k = v]
+decreases inv(m)
+func add(m cooliomapio, k key, v val) {
+	unfold inv(m)
+	if !m.inUse {
+		next@ := node{}
+		assert acc(m)
+		m.inUse = true
+		m.p = 1/4
+		m.next = &next
+		m.k = k
+		m.v = v
+		fold inv(m.next)
+		fold inv(m)
+		assert toDict(m) === unfolding inv(m) in toDict(m.next)[m.k = m.v]
+		assert toDict(m) === dict[key]val{k : v}
+		fold witness(m, k, v)
+	} else {
+		add(m.next, k, v)
+		assert witness(m.next, k, v)
+		m.p = m.p/2
+		fold inv(m)
+		fold witness(m, k, v)
+	}
+}
+
+ghost
+requires 0 < p
+requires acc(inv(m), p)
+//requires witness(m, k)
+requires witness(m, k, v)
+ensures  acc(inv(m), p)
+ensures  witness(m, k, v)
+ensures  k elem domain(toDict(m))
+ensures  toDict(m)[k] === v // v may not be comparable
+decreases acc(inv(m), p)
+func lemmaWitness(m cooliomapio, k key, v val, p perm) {
+	d := toDict(m)
+	unfold acc(inv(m), p)
+	unfold witness(m, k, v)
+	if m.k == k {
+		assert k elem domain(d)
+	} else {
+		lemmaWitness(m.next, k, v, p)
+	}
+	fold acc(inv(m), p)
+	fold witness(m, k, v)
+}
+
+ghost
+requires witness(m, k, v)
+ensures  witness(m, k, v) && witness(m, k, v)
+decreases witness(m, k, v)
+func dupWitness(m cooliomapio, k key, v val) {
+	unfold witness(m, k, v)
+	if m.k != k {
+		dupWitness(m.next, k, v)
+	}
+	fold witness(m, k, v)
+	fold witness(m, k, v)
+}
\ No newline at end of file
diff --git a/resalgebraNoAxioms/cooliosetio.gobra b/resalgebraNoAxioms/cooliosetio.gobra
new file mode 100644
index 0000000..4270bb2
--- /dev/null
+++ b/resalgebraNoAxioms/cooliosetio.gobra
@@ -0,0 +1,130 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+// sets that can only grow monotically. adding a new element to the set
+// requires and ensures the set invariant, but checking that a value is in the set
+// should not require the set inv
+
+ghost type valSet = idx
+
+ghost type nodeSet ghost struct {
+	inUse bool
+	next gpointer[nodeSet]
+	v valSet
+	p perm
+}
+
+// todo: change
+ghost type cooliosetio gpointer[nodeSet]
+
+pred (m cooliosetio) Inv() {
+	acc(m, 1/2) &&
+	(m.next == nil ==> !m.inUse && acc(m, 1/2)) &&
+	(m.next != nil ==> 
+		m.inUse &&
+		acc(&m.p, 1/2) &&
+		cooliosetio(m.next).Inv() &&
+		m.p > 0                   &&
+		acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.v, m.p))
+}
+
+ghost
+ensures m.Inv()
+ensures toCoolSet(m) == set[valSet]{}
+decreases
+func allocSet() (m cooliosetio) {
+	var g@ nodeSet
+	var c cooliosetio = &g
+	fold c.Inv()
+	return c
+}
+
+ghost
+requires m.Inv()
+decreases m.Inv()
+pure func toCoolSet(m cooliosetio) set[valSet] {
+	return unfolding m.Inv() in (m.inUse ? (toCoolSet(m.next) union set[valSet]{m.v}) : set[valSet]{})
+}
+
+pred (m cooliosetio) witness(v valSet) {
+	acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.v, _) &&
+	(!m.inUse ==> false) &&
+	(m.v != v ==> cooliosetio(m.next).witness(v))
+}
+
+ghost
+requires m.Inv()
+ensures  m.Inv()
+ensures  m.witness(v)
+ensures  toCoolSet(m) === old(toCoolSet(m)) union set[valSet]{v}
+decreases m.Inv()
+func (m cooliosetio) add(v valSet) {
+	unfold m.Inv()
+	if !m.inUse {
+		next@ := nodeSet{}
+		assert acc(m)
+		m.inUse = true
+		m.p = 1/4
+		m.next = &next
+		m.v = v
+		fold cooliosetio(m.next).Inv()
+		fold m.Inv()
+		fold m.witness(v)
+	} else {
+		cooliosetio(m.next).add(v)
+		assert cooliosetio(m.next).witness(v)
+		m.p = m.p/2
+		fold m.Inv()
+		fold m.witness(v)
+	}
+}
+
+ghost
+requires 0 < p
+requires acc(m.Inv(), p)
+requires m.witness(v)
+ensures  acc(m.Inv(), p)
+ensures  m.witness(v)
+ensures  v elem toCoolSet(m)
+decreases acc(m.Inv(), p)
+func (m cooliosetio) lemmaWitness(v valSet, p perm) {
+	d := toCoolSet(m)
+	// here
+	unfold acc(m.Inv(), p)
+	unfold m.witness(v)
+	if m.v == v {
+		assert v elem d
+	} else {
+		cooliosetio(m.next).lemmaWitness(v, p)
+	}
+	fold acc(m.Inv(), p)
+	fold m.witness(v)
+}
+
+ghost
+requires m.witness(v)
+ensures  m.witness(v) && m.witness(v)
+decreases m.witness(v)
+func (m cooliosetio) dupWitness(v valSet) {
+	unfold m.witness(v)
+	if m.v != v {
+		cooliosetio(m.next).dupWitness(v)
+	}
+	fold m.witness(v)
+	fold m.witness(v)
+}
\ No newline at end of file
diff --git a/resalgebraNoAxioms/doc.gobra b/resalgebraNoAxioms/doc.gobra
new file mode 100644
index 0000000..72564c7
--- /dev/null
+++ b/resalgebraNoAxioms/doc.gobra
@@ -0,0 +1,53 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+// This package shows that we can provide a model for ghost locations, similar to
+// those of Iris entirely in Gobra. The public API of this package is very similar to
+//  that of `resalgebra` except that (1) we made some tweaks to the definition of RA that
+// should be logically equivalent to those of the RA defined in `resalgebra`
+// but which are easier to work with in Gobra (e.g., all lemmas in the
+// interface RA are universally quantified, rather than requiring the user
+// to provide the instantiations of the quantified variables), (2) all
+// lemmas for ghost locations require a Witness value to be passed.
+// This is due to a technicality in Gobra (we cannot existentially quantify
+// over resources).
+
+// For the time being, to keep the same API for GhostLocations
+// as the one found in `resalgebra/loc.gobra`, we axiomatize
+// the introduction and elimination rules for existential QPs:
+
+// Same as `exists w s.t. GhostLocationW(l, ra, e, w)`
+pred GhostLocation(l LocName, ra RA, e Elem)
+
+// Converting between GhostLocationW and GhostLocation by
+// introducing the existential quantifier.
+ghost
+trusted
+requires GhostLocationW(l, ra, e, w)
+ensures  GhostLocation(l, ra, e)
+decreases
+func IntroExists(l LocName, ra RA, e Elem, w Witness)
+
+// Converting between GhostLocation and GhostLocationW by
+// eliminating the existential quantifier.
+ghost
+trusted
+requires GhostLocation(l, ra, e)
+ensures  GhostLocationW(l, ra, e, w)
+decreases
+func ElimExists(l LocName, ra RA, e Elem) (w Witness)
\ No newline at end of file
diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra
new file mode 100644
index 0000000..2100d72
--- /dev/null
+++ b/resalgebraNoAxioms/loc.gobra
@@ -0,0 +1,634 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+dup pkgInvariant Invariant(GlobalMem!<!>)
+package resalgebraNoAxioms
+
+// At the moment, all of these definitions are trusted, and this,
+// prone to mistakes. If possible, we should find a model for the
+// predicate GhostLocation and for all lemmas.
+
+ghost type LocName gpointer[int]
+
+/***** GhostLocation *****/
+
+ghost
+requires ra != nil
+requires ra.IsElem(e) && ra.IsValid(e)
+ensures  l != nil
+ensures  GhostLocation(l, ra, e)
+decreases
+func Alloc(ra RA, e Elem) (l LocName) {
+	l, w := AllocW(ra, e)
+	assert GhostLocationW(l, ra, e, w)
+	IntroExists(l, ra, e, w)
+}
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocation(l, ra, ra.Compose(e1, e2))
+ensures  GhostLocation(l, ra, e1) && GhostLocation(l, ra, e2)
+decreases
+func GhostOp1(l LocName, ra RA, e1 Elem, e2 Elem) {
+	w := ElimExists(l, ra, ra.Compose(e1, e2))
+	w1, w2 := GhostOp1W(l, ra, e1, e2, w)
+	IntroExists(l, ra, e1, w1)
+	IntroExists(l, ra, e2, w2)
+}
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocation(l, ra, e1) && GhostLocation(l, ra, e2)
+ensures  GhostLocation(l, ra, ra.Compose(e1, e2))
+decreases
+func GhostOp2(l LocName, ra RA, e1 Elem, e2 Elem) {
+	w1 := ElimExists(l, ra, e1)
+	w2 := ElimExists(l, ra, e2)
+	GhostOp2W(l, ra, e1, e2, w1, w2)
+	IntroExists(l, ra, ra.Compose(e1, e2), w1)
+}
+
+ghost
+requires ra != nil
+requires GhostLocation(l, ra, e)
+ensures  GhostLocation(l, ra, e)
+ensures  ra.IsElem(e) && ra.IsValid(e)
+decreases
+func GhostValid(l LocName, ra RA, e Elem) {
+	w := ElimExists(l, ra, e)
+	GhostValidW(l, ra, e, w)
+	IntroExists(l, ra, e, w)
+}
+
+// Slightly different from paper, only captures a deterministic update.
+// Non-deterministic update can be easily supported too.
+ghost
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocation(l, ra, e1)
+requires IsFramePreservingUpdate(ra, e1, e2)
+ensures  GhostLocation(l, ra, e2)
+decreases
+func GhostUpdate(l LocName, ra RA, e1 Elem, e2 Elem) {
+	w := ElimExists(l, ra, e1)
+	GhostUpdateW(l, ra, e1, e2, w)
+	IntroExists(l, ra, e2, w)
+}
+
+/***** Frame-Preserving Updates *****/
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+decreases
+pure func IsFramePreservingUpdate(ra RA, e1 Elem, e2 Elem) bool {
+	return forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] ==> ra.IsElem(get(c))) ==>
+		(LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) ==> LiftedIsValid(ra, LiftedCompose(ra, some(e2), c)))
+}
+
+ghost
+requires ra != nil
+requires e1 !== none[Elem] ==> ra.IsElem(get(e1))
+requires e2 !== none[Elem] ==> ra.IsElem(get(e2))
+decreases
+pure func LiftedCompose(ra RA, e1 option[Elem], e2 option[Elem]) option[Elem] {
+	return e1 === none[Elem] ?
+		e2 :
+		(e2 === none[Elem] ?
+			e1 :
+			some(ra.Compose(get(e1), get(e2))))
+}
+
+ghost
+requires ra != nil
+requires e !== none[Elem] ==> ra.IsElem(get(e))
+decreases
+pure func LiftedIsValid(ra RA, e option[Elem]) bool {
+	return e !== none[Elem] ?
+		ra.IsValid(get(e)) :
+		true
+}
+
+/***** Model: Global State *****/
+
+pred GlobalMem() {
+	inv(model) &&
+	ras.Inv()  &&
+	// necessary for proving key freshness
+	(forall k LocName :: { k elem domain(toDict(model)) } k elem domain(toDict(model)) ==> acc(k, 1/2)) &&
+	// complicated way of saying that the domains of model and ras are the same:
+	(forall k LocName :: { k elem domain(toDict(model)) } { ras.ToDict()[k] } k elem domain(toDict(model)) ==>
+		k elem domain(ras.ToDict())) &&
+	(forall k LocName :: { k elem domain(toDict(model)) } k elem domain(ras.ToDict()) ==>
+		k elem domain(toDict(model))) &&
+	(forall k LocName :: { k elem domain(ras.ToDict()) }{ ras.ToDict()[k] } k elem domain(ras.ToDict()) ==>
+		ras.ToDict()[k] != RA(nil)) &&
+	// injectivity
+	(forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		toDict(model)[k1] != toDict(model)[k2]) &&
+	(forall k LocName :: k elem domain(toDict(model)) ==> toDict(model)[k].Inv()) &&
+	// injectivity
+	(forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))) &&
+	(forall k LocName :: k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2))) &&
+	(forall k LocName :: { k elem domain(toDict(model)) }{ toDict(model)[k] } k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==>
+			i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))) &&
+	(forall k LocName :: { k elem domain(toDict(model)) } { toDict(model)[k] }{ ras.ToDict()[k] } k elem domain(toDict(model)) ==>
+		(forall i idx :: { i elem toCoolSet(toDict(model)[k]) } { i.inUse } i elem toCoolSet(toDict(model)[k]) ==>
+			i.inUse ==> (
+				forall i2 idx :: { ras.ToDict()[k].Compose(i.val, i2.val) } i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==>
+					ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) &&
+					ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))))
+	// MISSING: the product of all inUse elements is valid. requires proving all kinds of facts
+	//          about the updates to the set of values inUse and the order in which the multiplication is performed.
+	//          this is easy to show ghostOp1 and ghostOp2 and frame-preserving updates
+}
+
+// TODO: use MonoSet and MonoMap for the model; delete cooliosetio and mapio
+ghost var model cooliomapio = allocMap()
+ghost var ras rasMap = rasMapAlloc()
+
+func init() {
+	fold GlobalMem!<!>()
+	EstablishInvariant(GlobalMem!<!>)
+}
+
+/***** Model *****/
+
+ghost type idx gpointer[meta]
+
+ghost type Witness ghost struct {
+	i idx
+	c cooliosetio
+}
+
+ghost type meta ghost struct {
+	inUse bool
+	val Elem
+}
+
+pred GhostLocationW(l LocName, ra RA, e Elem, w Witness) {
+	acc(w.i, 1/2)          &&
+	w.i.inUse              &&
+	witness(model, l, w.c) &&
+	w.c.witness(w.i)       &&
+	ra != nil              &&
+	w.i.val === e          &&
+	ra.IsElem(w.i.val)     &&
+	ra.IsValid(w.i.val)    &&
+	ras.Witness(l, ra)
+}
+
+/***** Model: functions that do not acquire global invariant; these functions may be called from critical regions *****/
+
+ghost
+requires GlobalMem()
+requires ra != nil
+requires ra.IsElem(e) && ra.IsValid(e)
+ensures  GlobalMem()
+ensures  l != nil
+ensures  GhostLocationW(l, ra, e, w)
+decreases
+func AllocWI(ra RA, e Elem) (l LocName, w Witness) {
+	unfold GlobalMem()
+
+	newl := new(int)
+	var cs cooliosetio = allocSet()
+	iii := &meta{true, e}
+	cs.add(iii)
+	if (newl elem domain(toDict(model))) {
+		assert acc(newl, 3/2)
+	}
+	assert !(newl elem domain(toDict(model)))
+	rasDict := ras.ToDict()
+	assert !(newl elem domain(rasDict))
+	ras.Insert(newl, ra)
+	add(model, newl, cs)
+	assert witness(model, newl, cs)
+	newi := Witness{iii, cs}
+
+	assert forall k LocName :: k elem domain(toDict(model)) && k != newl ==>
+		!(iii elem toCoolSet(toDict(model)[k]))
+	assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))
+
+	fold GhostLocationW(newl, ra, e, newi)
+
+	assert acc(newl, 1/2)
+	assert forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2)
+	assert forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict())
+	assert forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil)
+
+	assert forall k LocName :: k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2))
+	assert forall k LocName :: k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==>
+			i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))
+	fold GlobalMem()
+
+	return newl, newi
+}
+
+ghost
+requires GlobalMem()
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, ra.Compose(e1, e2), w)
+ensures  GlobalMem()
+ensures  GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2)
+decreases
+func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) {
+	i := w
+	unfold GlobalMem()
+	unfold GhostLocationW(l, ra, ra.Compose(e1, e2), i)
+
+	ras.DupWitness(l, ra)
+	ras.WitnessInMap(l, ra, 1/10)
+	assert witness(model, l, i.c)
+	lemmaWitness(model, l, i.c, 1/3)
+	assert toDict(model)[l] === i.c
+	assert i.c.witness(i.i)
+	i.c.lemmaWitness(i.i, 1/3)
+	assert i.i elem toCoolSet(i.c)
+	ra.ValidOp(e1, e2)
+	assert ra.IsValid(e1)
+	ra.ComposeComm(e1, e2)
+	ra.ValidOp(e2, e1)
+	assert ra.IsValid(e2)
+
+	i.i.inUse = false
+	iii1 := &meta{true, e1}
+	dupWitness(model, l, i.c)
+	i.c.add(iii1)
+	i1 := Witness{iii1, i.c}
+	ras.DupWitness(l, ra)
+	assert forall k LocName :: k elem domain(toDict(model)) && k != l ==>
+		!(iii1 elem toCoolSet(toDict(model)[k]))
+	assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))
+	fold GhostLocationW(l, ra, e1, i1)
+
+	iii2 := &meta{true, e2}
+	i.c.add(iii2)
+	assert witness(model, l, i.c)
+	i2 := Witness{iii2, i.c}
+	assert forall k LocName :: k elem domain(toDict(model)) && k != l ==>
+		!(iii2 elem toCoolSet(toDict(model)[k]))
+	assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))
+	fold GhostLocationW(l, ra, e2, i2)
+
+	assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))
+
+	assert ras.ToDict()[l] === ra
+
+	// not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid
+
+	ghostOp1WIAux(ra, iii1.val, iii2.val)
+	
+	assert forall k LocName :: k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==>
+			i.inUse ==> (
+				forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==>
+					ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) &&
+					ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val))))
+
+	fold GlobalMem()
+	return i1, i2
+}
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1) && ra.IsElem(e2)
+requires ra.IsValid(ra.Compose(e1, e2))
+ensures  forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e1, e))
+ensures  forall e Elem :: { ra.Compose(e2, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e2, e))
+ensures  forall e Elem :: { ra.Compose(e, e1) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e, e1))
+ensures  forall e Elem :: { ra.Compose(e, e2) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e, e2))
+decreases
+func ghostOp1WIAux(ra RA, e1 Elem, e2 Elem) {
+	ghostOp1WIAux1(ra, e1, e2)
+	ghostOp1WIAux2(ra, e1, e2)
+	ComposeCommQ(ra)
+}
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1) && ra.IsElem(e2)
+requires ra.IsValid(ra.Compose(e1, e2))
+ensures  forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e1, e))
+decreases
+func ghostOp1WIAux1(ra RA, e1 Elem, e2 Elem) {
+	assert forall e Elem :: ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+		let _ := ra.ComposeAssoc(e1, e2, e) in
+		ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) &&
+		let _ := ra.ComposeComm(e2, e) in
+		ra.Compose(e, e2) === ra.Compose(e2, e) &&
+		ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) &&
+		let _ := ra.ComposeAssoc(e1, e, e2) in
+		ra.Compose(e1, ra.Compose(e, e2)) === ra.Compose(ra.Compose(e1, e), e2) &&
+		ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) &&
+		let _ := ra.ValidOp(ra.Compose(e1, e), e2) in
+		ra.IsValid(ra.Compose(e1, e))
+}
+
+ghost
+requires ra != nil
+requires ra.IsElem(e1) && ra.IsElem(e2)
+requires ra.IsValid(ra.Compose(e1, e2))
+ensures  forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+	ra.IsValid(ra.Compose(e2, e))
+decreases
+func ghostOp1WIAux2(ra RA, e1 Elem, e2 Elem) {
+	assert forall e Elem :: ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==>
+		let _ := ra.ComposeAssoc(e1, e2, e) in
+		ra.IsValid(ra.Compose(e1, ra.Compose(e2, e)))  &&
+		let _ := ra.ComposeComm(e1, ra.Compose(e2, e)) in
+		ra.IsValid(ra.Compose(ra.Compose(e2, e), e1))  &&
+		let _ := ra.ValidOp(ra.Compose(e2, e), e1) in
+		ra.IsValid(ra.Compose(e2, e))
+}
+
+ghost
+requires GlobalMem()
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2)
+ensures  GlobalMem()
+ensures  GhostLocationW(l, ra, ra.Compose(e1, e2), w1)
+decreases
+func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) {
+	i1 := w1
+	i2 := w2
+
+	unfold GlobalMem()
+	unfold GhostLocationW(l, ra, e1, i1)
+
+	ras.DupWitness(l, ra)
+	ras.WitnessInMap(l, ra, 1/10)
+	assert ra === ras.ToDict()[l]
+
+	unfold GhostLocationW(l, ra, e2, i2)
+	lemmaWitness(model, l, i2.c, 1/3)
+	assert forall i idx :: { i elem toCoolSet(toDict(model)[l]) } { i.inUse } i elem toCoolSet(toDict(model)[l]) ==>
+		i.inUse ==> (
+			forall i2 idx :: { ras.ToDict()[l].Compose(i.val, i2.val) } i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i ==>
+				ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) &&
+				ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val)))
+	assert i2.c === toDict(model)[l]
+	i2.c.lemmaWitness(i2.i, 1/3)
+	assert i2.i elem toCoolSet(i2.c)
+	lemmaWitness(model, l, i1.c, 1/3)
+	i1.c.lemmaWitness(i1.i, 1/3)
+
+	assert i1.i elem toCoolSet(toDict(model)[l]) && i1.i.inUse
+	assert i2.i elem toCoolSet(toDict(model)[l]) && i2.i.inUse
+	assert ra.IsElem(ra.Compose(i1.i.val, i2.i.val))
+	assert ra.IsValid(ra.Compose(i1.i.val, i2.i.val))
+
+	// TODO: this is where the invariant of Validity of the product of all elements comes in handy
+	//       to prove this assumption
+	assume forall ii idx :: ii elem toCoolSet(toDict(model)[l]) && ii.inUse && ii !== i1.i && ii != i2.i ==>
+		// let _ := ghostOp2WIaux(ra, e1, e2, ii.val) in
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ra.Compose(e1, e2), ii.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ra.Compose(e1, e2), ii.val))
+
+	assert ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2))
+	i1.i.val = ra.Compose(e1, e2)
+	i2.i.inUse = false
+	fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1)
+
+	assert forall k LocName :: k elem domain(toDict(model)) ==>
+		(forall i idx :: i elem toCoolSet(toDict(model)[k]) ==>
+			i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))
+
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i1.i ==>
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i1.i.val, i2.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i1.i.val, i2.val))
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i1.i ==>
+		let _ := ra.ComposeComm(i2.val, i1.i.val) in
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i2.val, i1.i.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i2.val, i1.i.val))
+	fold GlobalMem()
+}
+
+ghost
+requires GlobalMem()
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, e1, w)
+requires IsFramePreservingUpdate(ra, e1, e2)
+ensures  GlobalMem()
+ensures  GhostLocationW(l, ra, e2, w)
+decreases
+func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) {
+	i := w
+	unfold GlobalMem()
+
+	unfold GhostLocationW(l, ra, e1, i)
+	lemmaWitness(model, l, i.c, 1/3)
+	i.c.lemmaWitness(i.i, 1/3)
+
+	ras.DupWitness(l, ra)
+	ras.WitnessInMap(l, ra, 1/10)
+
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==>
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.i.val, i2.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.i.val, i2.val))
+
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==>
+		let _ := updateFrameLemma(ra, i.i.val, i2.val, e2) in
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(e2, i2.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(e2, i2.val))
+
+	i.i.val = e2
+
+	if forall e Elem :: ra.IsElem(e) ==> LiftedCompose(ra, some(e1), some(e)) === none[Elem] {
+		assert ra.IsValid(e2)
+	} else if forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) ==> !ra.IsValid(ra.Compose(e1, e)) {
+		assert IsFramePreservingUpdate(ra, e1, e2)
+		assert forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] ==> ra.IsElem(get(c))) ==>
+			(LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) ==> LiftedIsValid(ra, LiftedCompose(ra, some(e2), c)))
+		assert forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] ==> ra.IsElem(get(c))) ==>
+			(LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) ==> c === none[Elem])
+		assert LiftedIsValid(ra, LiftedCompose(ra, some(e2), none[Elem]))
+		assert ra.IsValid(e2)
+	} else {
+		assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) &&
+			LiftedCompose(ra, some(e1), some(e)) !== none[Elem]
+		ValidOpQ(ra)
+		assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) &&
+			LiftedIsValid(ra, LiftedCompose(ra, some(e1), some(e))) &&
+			ra.IsValid(ra.Compose(e1, e)) &&
+			ra.IsValid(ra.Compose(e2, e)) &&
+			ra.IsValid(e2)
+	}
+
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==>
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.i.val, i2.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.i.val, i2.val))
+	assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==>
+		let _ := ra.ComposeComm(i2.val, i.i.val) in
+		ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i2.val, i.i.val)) &&
+		ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i2.val, i.i.val))
+
+	fold GhostLocationW(l, ra, e2, i)
+	fold GlobalMem()
+}
+
+ghost
+opaque
+requires ra != nil
+requires ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3)
+requires ra.IsElem(ra.Compose(e1, e2))
+requires ra.IsValid(ra.Compose(e1, e2))
+requires IsFramePreservingUpdate(ra, e1, e3)
+ensures  ra.IsElem(ra.Compose(e3, e2))
+ensures  ra.IsValid(ra.Compose(e3, e2))
+decreases
+pure func updateFrameLemma(ra RA, e1 Elem, e2 Elem, e3 Elem) Unit {
+	return let _ := asserting(ra.IsValid(ra.Compose(e1, e2)))   in
+		let _ := asserting(IsFramePreservingUpdate(ra, e1, e3)) in
+		let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] ==> ra.IsElem(get(c))) ==>
+			(LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) ==> LiftedIsValid(ra, LiftedCompose(ra, some(e3), c)))) in
+		let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] && ra.IsElem(get(c))) ==>
+			LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) === ra.IsValid(ra.Compose(e1, get(c)))) in
+		let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { ra.Compose(e3, get(c)) } (c !== none[Elem] && ra.IsElem(get(c))) ==>
+			LiftedIsValid(ra, LiftedCompose(ra, some(e3), c)) === ra.IsValid(ra.Compose(e3, get(c)))) in
+		let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { ra.Compose(e3, get(c)) } (c !== none[Elem] && ra.IsElem(get(c))) ==>
+			ra.IsValid(ra.Compose(e1, get(c))) ==> ra.IsValid(ra.Compose(e3, get(c)))) in
+		// the term `get(some(e2))` is used to trigger the previous quantifier
+		let _ := asserting(ra.IsElem(ra.Compose(e3, get(some(e2))))) in
+		Unit{}
+}
+
+/***** Model: functions that do not depend on the global invariant *****/
+
+ghost
+requires ra != nil
+requires GhostLocationW(l, ra, e, w)
+ensures  GhostLocationW(l, ra, e, w)
+ensures  ra.IsElem(e) && ra.IsValid(e)
+decreases
+func GhostValidW(l LocName, ra RA, e Elem, w Witness) {
+	unfold GhostLocationW(l, ra, e, w)
+	fold GhostLocationW(l, ra, e, w)
+}
+
+/***** Model: wrappers that acquire the global invariant; these functions may not be called from critical regions *****/
+
+ghost
+opensInvariants
+requires ra != nil
+requires ra.IsElem(e) && ra.IsValid(e)
+ensures  l != nil
+ensures  GhostLocationW(l, ra, e, w)
+decreases
+func AllocW(ra RA, e Elem) (l LocName, w Witness) {
+	openDupPkgInv
+	critical GlobalMem!<!> (
+	changeView1()
+	l, w = AllocWI(ra, e)
+	changeView2()
+	)
+}
+
+ghost
+opensInvariants
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, ra.Compose(e1, e2), w)
+ensures  GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2)
+decreases
+func GhostOp1W(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) {
+	openDupPkgInv
+	critical GlobalMem!<!> (
+	changeView1()
+	w1, w2 = GhostOp1WI(l, ra, e1, e2, w)
+	changeView2()
+	)
+}
+
+ghost
+opensInvariants
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2)
+ensures  GhostLocationW(l, ra, ra.Compose(e1, e2), w1)
+decreases
+func GhostOp2W(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) {
+	openDupPkgInv
+	critical GlobalMem!<!> (
+	changeView1()
+	GhostOp2WI(l, ra, e1, e2, w1, w2)
+	changeView2()
+	)
+}
+
+ghost
+opensInvariants
+requires ra != nil
+requires ra.IsElem(e1)
+requires ra.IsElem(e2)
+requires GhostLocationW(l, ra, e1, w)
+requires IsFramePreservingUpdate(ra, e1, e2)
+ensures  GhostLocationW(l, ra, e2, w)
+decreases
+func GhostUpdateW(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) {
+	openDupPkgInv
+	critical GlobalMem!<!> (
+	changeView1()
+	GhostUpdateWI(l, ra, e1, e2, w)
+	changeView2()
+	)
+}
+
+ghost
+requires GlobalMem!<!>()
+ensures  GlobalMem()
+decreases
+func changeView1() {
+	unfold GlobalMem!<!>()
+	fold GlobalMem()
+}
+
+ghost
+requires GlobalMem()
+ensures  GlobalMem!<!>()
+decreases
+func changeView2() {
+	unfold GlobalMem()
+	fold GlobalMem!<!>()
+}
\ No newline at end of file
diff --git a/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra
new file mode 100644
index 0000000..7765c23
--- /dev/null
+++ b/resalgebraNoAxioms/oneshot.gobra
@@ -0,0 +1,119 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+type Pending struct{}
+
+type Shot struct {
+	N int
+}
+
+type Fail struct{}
+
+type TypeOneShotRA struct{}
+
+TypeOneShotRA implements RA
+
+var OneShotRA TypeOneShotRA = TypeOneShotRA{}
+
+ghost
+decreases
+pure
+func (ra TypeOneShotRA) IsElem(e Elem) (res bool) {
+	return e != nil &&
+		// using typeOf here leads to unexpected incompletnesses
+		(e === Elem(Pending{})) ||
+		typeOf(e) == type[Shot] ||
+		// using typeOf here leads to unexpected incompletnesses
+		(e === Fail{})
+}
+
+ghost
+requires ra.IsElem(e)
+decreases
+pure
+func (ra TypeOneShotRA) IsValid(e Elem) bool {
+	return e != nil &&
+		(typeOf(e) == type[Pending] || typeOf(e) == type[Shot])
+}
+
+ghost
+requires ra.IsElem(e)
+ensures  res !== none[Elem] ==> ra.IsElem(get(res))
+decreases
+pure
+func (ra TypeOneShotRA) Core(e Elem) (ghost res option[Elem]) {
+	return typeOf(e) == type[Pending] ?
+		none[Elem] :
+		some(e)
+}
+
+
+ghost
+requires ra.IsElem(e1) && ra.IsElem(e2)
+ensures  ra.IsElem(res)
+decreases
+pure
+func (ra TypeOneShotRA) Compose(e1 Elem, e2 Elem) (res Elem) {
+	return typeOf(e1) == type[Shot] && typeOf(e2) == type[Shot] && e1 === e2 ?
+		e1 :
+		Elem(Fail{})
+}
+
+// all of the following properties are proven automatically
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) ComposeComm(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) CoreId(e Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) CoreIdem(e Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) CoreMono(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
+
+ghost
+decreases
+pure func (ra TypeOneShotRA) ValidOp(e1 Elem, e2 Elem) Unit {
+	// proved
+	return Unit{}
+}
\ No newline at end of file
diff --git a/resalgebraNoAxioms/ra.gobra b/resalgebraNoAxioms/ra.gobra
new file mode 100644
index 0000000..8c15f8d
--- /dev/null
+++ b/resalgebraNoAxioms/ra.gobra
@@ -0,0 +1,172 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package resalgebraNoAxioms
+
+type Elem interface{}
+
+type Unit struct{}
+
+type RA interface {
+	// defines the set of elements of the RA
+	ghost
+	decreases
+	pure IsElem(e Elem) (res bool)
+
+	ghost
+	requires IsElem(e)
+	decreases
+	pure IsValid(e Elem) bool
+
+	ghost
+	requires IsElem(e)
+	ensures  res !== none[Elem] ==> IsElem(get(res))
+	decreases
+	pure Core(e Elem) (ghost res option[Elem])
+
+	ghost
+	requires IsElem(e1) && IsElem(e2)
+	ensures  IsElem(res)
+	decreases
+	pure Compose(e1 Elem, e2 Elem) (res Elem)
+
+	// Lemmas
+
+	ghost
+	requires IsElem(e1) && IsElem(e2) && IsElem(e3)
+	ensures  Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3))
+	decreases
+	pure ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit
+
+	ghost
+	requires IsElem(e1) && IsElem(e2)
+	ensures  Compose(e1, e2) === Compose(e2, e1)
+	decreases
+	pure ComposeComm(e1 Elem, e2 Elem) Unit
+
+	ghost
+	requires IsElem(e)
+	ensures  let c := Core(e) in
+		c !== none[Elem] ==> Compose(get(c), e) === e
+	decreases
+	pure CoreId(e Elem) Unit
+
+	ghost
+	requires IsElem(e)
+	requires Core(e) !== none[Elem]
+	ensures  let c := Core(e) in
+		let cc := Core(get(c)) in
+		cc !== none[Elem] &&
+		get(cc) === get(c)
+	decreases
+	pure CoreIdem(e Elem) Unit
+
+	ghost
+	requires IsElem(e1) && IsElem(e2)
+	requires Core(e1) !== none[Elem]
+	// fully expanded version of <= due to Gobra's lack of `Self` in interface specs
+	requires exists e3 Elem :: { IsElem(e3) } IsElem(e3) && e2 === Compose(e1, e3)
+	ensures  Core(e2) !== none[Elem]
+	ensures  exists e4 Elem :: { IsElem(e4) } IsElem(e4) && get(Core(e2)) === Compose(get(Core(e1)), e4)
+	decreases
+	pure CoreMono(e1 Elem, e2 Elem) Unit
+
+	ghost
+	requires IsElem(e1) && IsElem(e2)
+	requires IsValid(Compose(e1, e2))
+	ensures  IsValid(e1)
+	decreases
+	pure ValidOp(e1 Elem, e2 Elem) Unit
+}
+
+// The following wrappers should be treated as automatically generated code, their implementation
+// is not to be read closely
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e1, e2, e3 Elem :: { ra.Compose(ra.Compose(e1, e2), e3) } { ra.Compose(e1, ra.Compose(e2, e3)) } ra.IsElem(e1) &&
+	ra.IsElem(e2) && ra.IsElem(e3) ==>
+		ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3))
+decreases
+pure func ComposeAssocQ(ra RA) Unit {
+	return asserting(forall e1, e2, e3 Elem :: { ra.Compose(ra.Compose(e1, e2), e3) } { ra.Compose(e1, ra.Compose(e2, e3)) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) ==> let _ := ra.ComposeAssoc(e1, e2, e3) in ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3)))
+}
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e1, e2 Elem :: { ra.Compose(e1, e2) } { ra.Compose(e2, e1) } ra.IsElem(e1) && ra.IsElem(e2) ==>
+	ra.Compose(e1, e2) === ra.Compose(e2, e1)
+decreases
+pure func ComposeCommQ(ra RA) Unit {
+	return asserting(forall e1, e2 Elem :: { ra.Compose(e1, e2) } { ra.Compose(e2, e1) } ra.IsElem(e1) && ra.IsElem(e2) ==> let _ := ra.ComposeComm(e1, e2) in ra.Compose(e1, e2) === ra.Compose(e2, e1))
+}
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e Elem :: { ra.Core(e) } ra.IsElem(e) ==>
+	let c := ra.Core(e) in
+		c !== none[Elem] ==> ra.Compose(get(c), e) === e
+decreases
+pure func CoreIdQ(ra RA) Unit {
+	return asserting(forall e Elem :: { ra.Core(e) } ra.IsElem(e) ==> let _ := ra.CoreId(e) in ra.Core(e) !== none[Elem] ==> ra.Compose(get(ra.Core(e)), e) === e)
+}
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e Elem :: { ra.Core(e) } ra.IsElem(e) && ra.Core(e) !== none[Elem] ==>
+	let c := ra.Core(e) in
+	let cc := ra.Core(get(c)) in
+	cc !== none[Elem] &&
+	get(cc) === get(c)
+decreases
+pure func CoreIdemQ(ra RA) Unit {
+	return asserting(forall e Elem :: { ra.Core(e) } ra.IsElem(e) && ra.Core(e) !== none[Elem] ==> let _ := ra.CoreIdem(e) in let c := ra.Core(e) in let cc := ra.Core(get(c)) in cc !== none[Elem] && get(cc) === get(c))
+}
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e1, e2 Elem ::  { ra.Core(e1), ra.Core(e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.Core(e1) !== none[Elem] &&
+	// fully expanded version of <= due to Gobra's lack of `Self` in interface specs
+	(exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3)) ==>
+	ra.Core(e2) !== none[Elem] &&
+	exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4)
+decreases
+pure func CoreMonoQ(ra RA) Unit {
+	return asserting(forall e1, e2 Elem :: { ra.Core(e1), ra.Core(e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.Core(e1) !== none[Elem] && (exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3)) ==> let _ := ra.CoreMono(e1, e2) in ra.Core(e2) !== none[Elem] &&
+	exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4))
+}
+
+ghost
+opaque
+requires ra != nil
+ensures  forall e1, e2 Elem :: { ra.Compose(e1, e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsValid(ra.Compose(e1, e2)) ==>
+	ra.IsValid(e1)
+decreases
+pure func ValidOpQ(ra RA) Unit {
+	return asserting(forall e1, e2 Elem :: { ra.Compose(e1, e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsValid(ra.Compose(e1, e2)) ==> let _ := ra.ValidOp(e1, e2) in ra.IsValid(e1))
+}
+
+ghost
+requires b
+decreases
+pure func asserting(ghost b bool) Unit {
+	return Unit{}
+}
diff --git a/resalgebraNoAxioms/ras-map.gobra b/resalgebraNoAxioms/ras-map.gobra
new file mode 100644
index 0000000..d57a360
--- /dev/null
+++ b/resalgebraNoAxioms/ras-map.gobra
@@ -0,0 +1,151 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+// Instantiation of genericmonomap for `ras` (Key is LocName and Val is RA).
+// Copying this is easier than implementing wrappers around MonoMap.
+
+package resalgebraNoAxioms
+
+ghost type keyRasMap = LocName
+type valRasMap = RA
+
+ghost type nodeRasMap ghost struct {
+	inUse bool
+	next gpointer[nodeRasMap]
+	k keyRasMap
+	v valRasMap
+	p perm
+}
+
+ghost type rasMap gpointer[nodeRasMap]
+
+pred (m rasMap) Inv() {
+	acc(m, 1/2) &&
+	(m.next == nil ==> !m.inUse && acc(m, 1/2)) &&
+	(m.next != nil ==> 
+		m.inUse &&
+		acc(&m.p, 1/2)       &&
+		rasMap(m.next).Inv() &&
+		m.p > 0              &&
+		acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.k, m.p) && acc(&m.v, m.p))
+}
+
+ghost
+mayInit
+ensures m.Inv()
+ensures m.ToDict() == dict[keyRasMap]valRasMap{}
+decreases
+func rasMapAlloc() (m rasMap) {
+	var g@ nodeRasMap
+	fold rasMap(&g).Inv()
+	return &g
+}
+
+ghost
+requires  m.Inv()
+decreases m.Inv()
+pure func (m rasMap) ToDict() dict[keyRasMap]valRasMap {
+	return unfolding m.Inv() in
+		(m.inUse ? (let smallMap := rasMap(m.next).ToDict() in smallMap[m.k = m.v]) : dict[keyRasMap]valRasMap{})
+}
+
+ghost
+requires  m.Inv()
+decreases m.Inv()
+pure func (m rasMap) KeySet() set[keyRasMap] {
+	return domain(m.ToDict())
+}
+
+ghost
+requires  m.Inv()
+requires  k elem domain(m.ToDict())
+decreases m.Inv()
+pure func (m rasMap) Get(k keyRasMap) valRasMap {
+	return let d := m.ToDict() in valRasMap(d[k])
+}
+
+pred (m rasMap) Witness(k keyRasMap, v valRasMap) {
+	acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) &&
+	(!m.inUse ==> false)               &&
+	(m.k === k && m.v !== v ==> false) &&
+	(m.k != k ==> rasMap(m.next).Witness(k, v))
+}
+
+ghost
+requires m.Inv()
+requires !(k elem domain(m.ToDict()))
+ensures  m.Inv()
+ensures  m.Witness(k, v)
+ensures  m.ToDict() === old(m.ToDict())[k = v]
+decreases m.Inv()
+func (m rasMap) Insert(k keyRasMap, v valRasMap) {
+	unfold m.Inv()
+	if !m.inUse {
+		next@ := nodeRasMap{}
+		assert acc(m)
+		m.inUse = true
+		m.p = 1/4
+		m.next = &next
+		m.k = k
+		m.v = v
+		fold rasMap(m.next).Inv()
+		fold m.Inv()
+		assert m.ToDict() === unfolding m.Inv() in rasMap(m.next).ToDict()[m.k = m.v]
+		assert m.ToDict() === dict[keyRasMap]valRasMap{k : v}
+		fold m.Witness(k, v)
+	} else {
+		rasMap(m.next).Insert(k, v)
+		assert rasMap(m.next).Witness(k, v)
+		m.p = m.p/2
+		fold m.Inv()
+		fold m.Witness(k, v)
+	}
+}
+
+ghost
+requires 0 < p
+requires acc(m.Inv(), p)
+requires m.Witness(k, v)
+ensures  acc(m.Inv(), p)
+ensures  m.Witness(k, v)
+ensures  k elem domain(m.ToDict())
+ensures  m.ToDict()[k] === v
+decreases acc(m.Inv(), p)
+func (m rasMap) WitnessInMap(k keyRasMap, v valRasMap, p perm) {
+	d := m.ToDict()
+	unfold acc(m.Inv(), p)
+	unfold m.Witness(k, v)
+	if m.k == k {
+		assert k elem domain(d)
+	} else {
+		rasMap(m.next).WitnessInMap(k, v, p)
+	}
+	fold acc(m.Inv(), p)
+	fold m.Witness(k, v)
+}
+
+ghost
+requires m.Witness(k, v)
+ensures  m.Witness(k, v) && m.Witness(k, v)
+decreases m.Witness(k, v)
+func (m rasMap) DupWitness(k keyRasMap, v valRasMap) {
+	unfold m.Witness(k, v)
+	if m.k != k {
+		rasMap(m.next).DupWitness(k, v)
+	}
+	fold m.Witness(k, v)
+	fold m.Witness(k, v)
+}
\ No newline at end of file