```
(def-theorem copy-definedness
"forall(phi:[place -> word], h:[place -> place], #(copy(phi,h)))"
(theory places)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally copy)
simplify-insistently)))
```

```
(def-theorem a%copy-definedness
"forall(phi:[place -> word], h:[place -> place], copy%fn(phi,h) implies #(a%copy(phi,h)))"
(theory places)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally a%copy)
simplify)))
```

```
(def-theorem user%eq-transitivity
"forall(gamma_0, gamma_1, gamma_2:[place -> word], v:sets[place],
user%eq(gamma_0,gamma_1, v)  and user%eq(gamma_1,gamma_2, v)
implies user%eq(gamma_0,gamma_2, v))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally user%eq)
direct-and-antecedent-inference-strategy)))
```

```
(def-theorem user%eq-abstr
"forall (sigma_1, sigma_2:istate, v:sets[place],
user%eq(abstr(sigma_1), abstr(sigma_2), v)
iff
restrict{lambda(p:place, promote(sigma_1, p)),v}
=restrict{lambda(p:place, promote(sigma_2, p)),v})"
(theory places)
(proof
(
(unfold-single-defined-constant-globally abstr)
(unfold-single-defined-constant-globally user%eq))))
```

```
"forall(sigma:istate, f:[place -> place], copy%fn(abstr(sigma),f) implies
(theory places)
(usages d-r-convergence)
(proof
(
simplify
(apply-macete-with-minor-premises copy-liveness-corollary)
simplify)))
```

```
(def-theorem lower-definedness
"forall(sigma:istate, h:[place -> place],
#(lower(sigma,h)))"
(theory places)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally lower)
simplify-insistently)))
```

```
(def-theorem c%copy-definedness
"forall(sigma:istate, h:[place -> place],
copy%fn(abstr(sigma),h) implies
#(c%copy(sigma,lower(sigma,h))))"
(theory places)
(proof
(
(apply-macete-with-minor-premises copy-liveness-corollary)
simplify)))
```

```
(def-theorem lower-is-c%copy%fn
"forall(sigma:istate,h:[place,place],p:place,
c%copy%fn(sigma,lower(sigma,h)))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally c%copy%fn)
(unfold-single-defined-constant-globally lower)
simplify)))
```

```
(def-theorem default-c%copy-bound%place
"forall(sigma:istate, h:[place -> place], p:place,
p in bound%place(sigma) implies
default(c%copy(sigma,lower(sigma,h)))(p)==default(sigma)(p))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
simplify
(unfold-single-defined-constant-globally lower)
simplify)))
```

```
(def-theorem default-c%copy-un-bound%place
"forall(sigma:istate, h:[place -> place], p:place,
not(p in bound%place(sigma)) implies
default(c%copy(sigma,lower(sigma,h)))(p)==h(p))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
simplify
(unfold-single-defined-constant-globally lower)
simplify)))
```

```
(def-theorem gamma-c%copy-unchanged
"forall(sigma:istate, h:[place -> place],
gamma(c%copy(sigma,lower(sigma,h)))=gamma(sigma))"
(theory places)
(usages rewrite)
(proof
(
(unfold-single-defined-constant-globally c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
simplify)))
```

```
"forall(sigma:istate, f:[place -> place],
(theory places)
(proof
(
simplify)))
```

```
(def-theorem in-range-condition
"forall(y:ind_1,h:[ind_1 -> ind_2], h(y) in ran{h} iff #(h(y)))"
(theory generic-theory-2)
(usages transportable-macete transportable-rewrite)
(proof
(
direct-and-antecedent-inference-strategy
beta-reduce-insistently
simplify
(instantiate-existential ("y_\$0")))))
```

```
(def-theorem dom-ran-disjointness-lemma
"forall(h,g:[ind_1->ind_1], dom{h} disj dom{g} implies
dom{(inverse{g}) oo h} disj ran{(inverse{g}) oo h})"
(theory generic-theory-1)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
(case-split ("#(h(x_\$5))"))
(move-to-sibling 2)
simplify
(block
(script-comment "`case-split' at (1)")
beta-reduce
(eliminate-iota 0)
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(contrapose "with(p:prop,forall(x_\$0:ind_1,p or p));")
(instantiate-existential ("x_\$0"))
simplify))))
```

```
"forall(sigma:istate,g,h,f,h%plus:[place,place],v:sets[place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma),h%plus)
and
ran{h} subseteq bound%place(sigma)
and
dom{h} disj bound%place(sigma)
and
ran{h} disj ran{default(sigma)}
and
bijective_on_q{g,dom{g},ran{h}}
and
dom{g} disj bound%place(sigma)
and
dom{g} disj dom{h}
and
dom{g} disj ran{h}
and
dom{g} disj v
and
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))),
p,
#(g(p)),
g(p),
?place))
implies
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises c%copy-definedness)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(raise-conditional (0))
direct-inference
(apply-macete-with-minor-premises copy-liveness-corollary)
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises a%copy-definedness)
(unfold-single-defined-constant-globally copy%fn)
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
(apply-macete-with-minor-premises rev%bound%place-abstr-definedness)
(backchain "with(f:[place,place],f)
=with(f:sets[place],
lambda(p:place,
with(p:prop,
if(with(p:place,p in f),
with(p:place,p),
with(p:prop,p),
with(p:place,p),
with(p:place,p)))));")
beta-reduce
simplify)
(block
(script-comment "`direct-inference' at (1)")
(backchain "with(f:[place,place],f)
=with(f:sets[place],
lambda(p:place,
with(p:prop,
if(with(p:place,p in f),
with(p:place,p),
with(p:prop,p),
with(p:place,p),
with(p:place,p)))));")
beta-reduce-insistently
(raise-conditional (0))
(raise-conditional (2))
direct-and-antecedent-inference-strategy
(contrapose "with(w:word,not(#(w)));")
(apply-macete-with-minor-premises rev%bound%place-abstr-definedness)
(backchain "with(p,x_\$0:place,x_\$0=p);")
(raise-conditional (0))
(raise-conditional (0))
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(contrapose "with(p,x_\$0:place,x_\$0=p);")
(raise-conditional (0))
(raise-conditional (0))
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(cut-with-single-formula "forsome(y:place, g(x)=h(y))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference-strategy (0))
(backchain "with(y:place,h:[place,place],x:place,g:[place,place],
g(x)=h(y));")
(apply-macete-with-minor-premises bound%place-abstr-definedness)
(apply-macete-with-minor-premises copy-liveness)
(unfold-single-defined-constant-globally a%copy)
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally copy)
(backchain "with(h:[place,place],f:sets[place],h%plus:[place,place],
h%plus=lambda(p:place,if(p in f, p, h(p))));")
beta-reduce
(raise-conditional (0))
(apply-macete-with-minor-premises rev%bound%place-abstr-definedness)
direct-and-antecedent-inference-strategy
(contrapose "with(y:place,h:[place,place],sigma:istate,
not(h(y) in bound%place(sigma)));")
(backchain "with(f:sets[place],f subseteq f);")
(apply-macete-with-minor-premises tr%in-range-condition))
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(h,g:[place,place],ran{g}=ran{h});")
extensionality
simplify-insistently
(instantiate-existential ("g(x)"))
(contrapose "with(x:place,g:[place,place],
forall(x_\$1:place,not(g(x)=g(x_\$1))));")
(instantiate-existential ("x"))))))))))
```

```
(def-theorem default-in-bound-place-implies-bound
"forall(p:place,sigma:istate,
default(sigma)(p) in bound%place(sigma)
implies
p in bound%place(sigma));"
(theory places)
(proof
(
(apply-macete-with-minor-premises bound%place-characterization)
(apply-macete-with-minor-premises tr%meaning-of-indic-from-pred-element)
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%first%entry-equation)
simplify)))
```

```
(def-theorem copy-fn-dom-bound
"forall(h:[place,place],sigma:istate,
#(c%copy(sigma,h)) and ran{h} subseteq bound%place(sigma)
implies
dom{h} subseteq bound%place(c%copy(sigma,h)));"
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "default(c%copy(sigma,h))= h")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(incorporate-antecedent "with(f:istate,#(f));")
(unfold-single-defined-constant-globally c%copy)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
simplify-insistently
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises default-in-bound-place-implies-bound)
simplify
(instantiate-universal-antecedent "with(f:sets[place],f subseteq f);"
("h(x_\$0)"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%in-range-condition))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(apply-macete-with-minor-premises bound%place%stability)
direct-and-antecedent-inference-strategy)))))
```

```
"
forall(sigma:istate,g,h,f,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma),h%plus)
and
ran{h} subseteq bound%place(sigma)
and
ran{g}=ran{h}
and
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))),
p,
#(g(p)),
g(p),
?place))
implies
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally copy%fn)
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises c%copy-definedness)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(force-substitution "dom{abstr(c%copy(sigma,lower(sigma,h%plus)))}"
"bound%place(c%copy(sigma,lower(sigma,h%plus)))"
(0 1))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
extensionality
simplify
(apply-macete-with-minor-premises bound%place-abstr-definedness)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%value-of-a-defined-indicator-application)
(apply-macete-with-minor-premises bound%place-abstr-definedness))
(block
(script-comment "`force-substitution' at (0)")
(backchain-repeatedly ("with(g,h%plus:[place,place],sigma:istate,f:[place,place],
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))),
p,
#(g(p)),
g(p),
?place)));"))
beta-reduce
direct-and-antecedent-inference-strategy
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
beta-reduce-insistently
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(p,x_\$0:place,x_\$0=p);")
(case-split-on-conditionals (0))
direct-inference
(cut-with-single-formula "forsome(y:place, x_\$0=h(y))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(y:place,p));")
(backchain "with(p,x_\$0:place,x_\$0=p);")
(instantiate-universal-antecedent "with(f:sets[place],f subseteq f);"
("h(y)"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(y:place,h:[place,place],not(h(y) in ran{h}));")
(apply-macete-with-minor-premises tr%in-range-condition))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(apply-macete-with-minor-premises bound%place%stability)
(apply-macete-with-minor-premises c%copy-definedness)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(f:sets[place],f=f);")
extensionality
beta-reduce-insistently
simplify
(instantiate-existential ("g(x)"))
simplify
(block
(script-comment "`instantiate-existential' at (0 1)")
(contrapose "with(p:prop,not(forsome(x_\$0:place,p)));")
(instantiate-existential ("x"))))))))))
```

```
"forall(sigma:istate, f:[place->place],
(theory places)
(proof
(
direct-inference
(case-split-on-conditionals (0))
(unfold-single-defined-constant-globally c%copy)
(case-split-on-conditionals (0)))))
```

```
"forall(sigma:istate, g, h, f, h%plus:[place -> place], v:sets[place],
h%plus=lambda (p:place, if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma), h%plus)
and
ran(h) subseteq bound%place(sigma)
and
dom(h) disj bound%place(sigma)
and
ran(h) disj ran(default(sigma))
and
bijective_on_q{g,dom{g},ran{h}}
and
dom(g) disj bound%place(sigma)
and
dom(g) disj dom(h)
and
dom(g) disj ran(h)
and
dom(g) disj v
and
f=lambda(p:place, if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p, #(g(p)), g(p),  ?place))
implies
(inverse{g}) oo h)))"
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally c%redirect)
beta-reduce-with-minor-premises
(raise-conditional (0))
direct-inference
simplify
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(p:prop,not(p));")
(unfold-single-defined-constant-globally c%redirect%fn)
beta-reduce-with-minor-premises
(apply-macete-with-minor-premises gamma-c%copy-unchanged)
(apply-macete-with-minor-premises tr%range-composition)
(apply-macete-with-minor-premises tr%ran-of-inverse)
(move-to-sibling 2)
(apply-macete-with-minor-premises tr%injective-iff-injective-on-domain)
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%injective-iff-injective-on-domain)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises tr%domain-composition)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
extensionality
simplify
(instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"
("x_0"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 0)")
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
direct-inference)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 1)")
direct-inference
(contrapose "with(x_0:place,f:sets[place],not(x_0 in f));")
(apply-macete-with-minor-premises bound%place-characterization)
(apply-macete-with-minor-premises tr%first%entry-identity-in-set)
(move-to-ancestor 1)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%first%entry-identity-in-set)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
extensionality
beta-reduce-insistently
(raise-conditional (0 1 2))
(move-to-ancestor 1)
simplify
(instantiate-universal-antecedent "with(h,g:[place,place],dom{g} disj dom{h});"
("x_0"))
(move-to-ancestor 1)
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
direct-inference
(backchain "with(p:prop,p or p);"))
(move-to-ancestor 4)
(move-to-descendent (2))
(block
(script-comment "`apply-macete-with-minor-premises' at (1 0)")
(apply-macete-with-minor-premises tr%dom-of-inverse)
(backchain "with(h,g:[place,place],ran{g}=ran{h});"))
(move-to-ancestor 4)
(move-to-descendent (1))
(weaken (1))
(move-to-ancestor 6)
(move-to-descendent (2))
(block
(script-comment "`apply-macete-with-minor-premises' at (1 0)")
(apply-macete-with-minor-premises tr%dom-of-inverse)
(backchain "with(h,g:[place,place],ran{g}=ran{h});"))
(move-to-ancestor 6)
(move-to-descendent (1))
(weaken (0 1))
(move-to-ancestor 8)
(move-to-descendent (1))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
auto-instantiate-existential)
(move-to-ancestor 8)
(move-to-descendent (2))
(apply-macete-with-minor-premises c%copy-definedness)
(move-to-ancestor 9)
(move-to-descendent (1))
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
auto-instantiate-existential)
(move-to-ancestor 14)
(move-to-descendent (1))
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0)")
beta-reduce-insistently
simplify-insistently
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(cut-with-single-formula "#(h(x_\$3))")
(cut-with-single-formula "#(iota(y:place,g(y)=h(x_\$3)))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(eliminate-iota 0)
(contrapose "with(h,g:[place,place],ran{g}=ran{h});")
extensionality
beta-reduce-insistently
(weaken (17 16 15 14 13 12 11 10 9 8 6 3 2 1))
simplify
(instantiate-existential ("h(x_\$3)"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(contrapose "with(p:prop,forall(y%iota:place,p));")
(antecedent-inference "with(p:prop,forsome(x_\$1:place,p));")
(instantiate-existential ("x_\$1"))
(backchain "with(g:[place,place],f:sets[place],injective_on_q{g,f});")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`instantiate-existential' at (0 1)")
simplify
(instantiate-existential ("x_\$3"))))
(block
(script-comment "`cut-with-single-formula' at (0)")
(unfold-single-defined-constant (0 2) lower)
(cut-with-single-formula "x_\$3 in bound%place(c%copy(sigma,lower(sigma,h%plus)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "not((inverse{g}(h(x_\$3))) in bound%place(c%copy(sigma,lower(sigma,h%plus))))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(raise-conditional (0))
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(contrapose "with(p:place,f:sets[place],not(p in f));")
beta-reduce-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(apply-macete-with-minor-premises default-c%copy-un-bound%place)
(backchain "with(f:[place,place],f)
=with(f:sets[place],
lambda(p:place,
with(p:prop,
if(with(p:place,p in f),
with(p:place,p),
with(p:prop,p),
with(p:place,p),
with(p:place,p)))));")
beta-reduce
(backchain "with(h:[place,place],f:sets[place],h%plus:[place,place],
h%plus=lambda(p:place,if(p in f, p, h(p))));")
beta-reduce
(raise-conditional (0))
direct-inference
(raise-conditional (0))
direct-inference
(raise-conditional (0))
direct-inference
(move-to-sibling 1)
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(p:place,not(#(p)));")
(eliminate-defined-iota-expression 0

a))
(eliminate-defined-iota-expression 0

b)))
(block
(script-comment "`cut-with-single-formula' at (1)")
beta-reduce-insistently
(cut-with-single-formula "iota(y:place,g(y)=h(x_\$3)) in dom{g}")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
simplify
(eliminate-defined-iota-expression 0

a))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "dom{g} disj bound%place(c%copy(sigma,lower(sigma,h%plus)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(f:[place,place],sigma:istate,g:[place,place],
dom{g} disj bound%place(c%copy(sigma,f)));")
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (1)")
insistent-direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises bound%place-characterization)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals)
(apply-macete-with-minor-premises gamma-c%copy-unchanged)
(unfold-single-defined-constant-globally c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
(raise-conditional (0))
direct-inference
(contrapose "with(x_\$0:place,g:[place,place],x_\$0 in dom{g});")
(antecedent-inference "with(p:prop,if_form(p, p, p));")
(contrapose "with(x_\$0:place,
#(first%entry(with(f:[place,place],f),
with(f:sets[place],f),
x_\$0)));")
(apply-macete-with-minor-premises tr%first%entry-equation)
beta-reduce-insistently
(apply-macete-with-minor-premises default%make-istate)
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals)
(contrapose "with(x_\$0:place,g:[place,place],x_\$0 in dom{g});")
(move-to-ancestor 1)
(raise-conditional (0))
(contrapose "with(x_\$0:place,g:[place,place],x_\$0 in dom{g});")
(antecedent-inference "with(p:prop,if_form(p, p, p));")
(block
(script-comment "`antecedent-inference' at (0)")

(contrapose "with(w:word,#(w));")

(move-to-ancestor 1)

(contrapose "with(f:[place,word],g:[place,place],
dom{g} inters dom{f}=empty_indic{place});")

extensionality

beta-reduce

(instantiate-existential ("x_\$0"))

beta-reduce

simplify)
(block
(script-comment "`antecedent-inference' at (1)")

(contrapose "with(p:place,
#(first%entry(with(f:[place,place],f),
with(f:sets[place],f),
p)));")

(unfold-single-defined-constant (1) lower)

(backchain "with(h:[place,place],f:sets[place],h%plus:[place,place],
h%plus=lambda(p:place,if(p in f, p, h(p))));")

(backchain "with(h:[place,place],f:sets[place],h%plus:[place,place],
h%plus=lambda(p:place,if(p in f, p, h(p))));")

beta-reduce

(force-substitution "if(x_\$0 in bound%place(sigma),
default(sigma)(x_\$0),
x_\$0 in bound%place(sigma),
x_\$0,
h(x_\$0))"
"h(x_\$0)"
(0))

(move-to-sibling 1)

(block
(script-comment "`force-substitution' at (1)")
(instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"
("x_\$0"))
(weaken (15 14 13 12 11 10 9 8 6 5 4 3))
simplify)

(block
(script-comment "`force-substitution' at (0)")
(cut-with-single-formula "not(#(h(x_\$0)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(weaken (14 13 12 11 10 9 8 6 5 4 3))
simplify)
(block
(script-comment "`cut-with-single-formula' at (1)")
(instantiate-universal-antecedent "with(h,g:[place,place],dom{g} disj dom{h});"
("x_\$0"))
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined))))))))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises default-in-bound-place-implies-bound)
(unfold-single-defined-constant (0)

c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
(raise-conditional (0))
(apply-macete-with-minor-premises default%make-istate)
(unfold-single-defined-constant (0)

lower)
(backchain "with(h:[place,place],f:sets[place],h%plus:[place,place],
h%plus=lambda(p:place,if(p in f, p, h(p))));")
beta-reduce
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(contrapose "with(x_\$3:place,sigma:istate,x_\$3 in bound%place(sigma));")
(instantiate-universal-antecedent "with(sigma:istate,h:[place,place],
dom{h} disj bound%place(sigma));"

("x_\$3")))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(raise-conditional (0))
direct-inference
(apply-macete-with-minor-premises bound%place%stability)
(apply-macete-with-minor-premises c%copy-definedness)
direct-inference
(instantiate-universal-antecedent "with(f:sets[place],f subseteq f);"

("(h(x_\$3))"))
(contrapose "with(x_\$3:place,h:[place,place],not(h(x_\$3) in ran{h}));")
(apply-macete-with-minor-premises tr%in-range-condition)))))))))))
```

```
(def-theorem case-1-mach-copy
"forall(sigma:istate, g, h, f, h%plus:[place -> place], v:sets[place],
h%plus=lambda (p:place, if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma), h%plus)
and
ran(h) subseteq bound%place(sigma)
and
dom(h) disj bound%place(sigma)
and
ran(h) disj ran(default(sigma))
and
bijective_on_q{g,dom{g},ran{h}}
and
dom(g) disj bound%place(sigma)
and
dom(g) disj dom(h)
and
dom(g) disj ran(h)
and
dom(g) disj v
and
f=lambda(p:place, if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p, #(g(p)), g(p),  ?place))
implies
user%eq(
a%copy(abstr(sigma), h%plus),
abstr(c%redirect(
(inverse{g} oo h))),
v))"
(theory places)
(proof
(
(apply-macete-with-minor-premises c%redirect-no-op)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
auto-instantiate-existential)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises rev%copy-liveness)
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises c%copy-definedness)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
insistent-direct-and-antecedent-inference-strategy
simplify-insistently
(backchain "with(f:[place,place],f)
=with(f:sets[place],
lambda(p:place,
with(p:prop,
if(with(p:place,p in f),
with(p:place,p),
with(p:prop,p),
with(p:place,p),
with(p:place,p)))));")
beta-reduce
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(contrapose "with(p:place,#(p));")
(move-to-ancestor 1)
(instantiate-universal-antecedent "with(v:sets[place],g:[place,place],dom{g} disj v);"
("x"))
(contrapose "with(x:place,g:[place,place],not(x in dom{g}));")
simplify)))))
```

```
(def-constant h%ok
"lambda(h:[place->place], sigma:istate,
ran(h) subseteq bound%place(sigma)
and
dom(h) disj bound%place(sigma))"
(theory places))
```

```
(def-constant g%h%ok
"lambda(g,h:[place->place], sigma:istate,
bijective_on_q{g,dom{g},ran{h}}
and
dom(g) disj bound%place(sigma)
and
dom(g) disj dom{default(sigma)}
and
dom(g) disj dom(h))"
(theory places))
```

```
(def-theorem g%h%ok-corollary
"forall(g,h:[place->place], sigma:istate,
h%ok(h, sigma) and g%h%ok(g,h, sigma)
implies dom(g) disj ran(h))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally h%ok)
(unfold-single-defined-constant-globally g%h%ok)
insistent-direct-and-antecedent-inference-strategy
(backchain "with(f:sets[place],f subseteq f);")
(backchain "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"))))
```

```
(def-constant snapshot%not%visible
"lambda(g:[place->place], v:sets[place], dom(g) disj v)"
(theory places))
```

```
(def-theorem silly-conditional-simplification
"forall(sigma:istate, g, h, f, h%plus:[place -> place], v:sets[place],
lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p,
#(g(p)), g(p),  ?place))
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p,  g(p))))"
(theory places)
(proof ((prove-by-logic-and-simplification 0))))
```

```
(def-theorem case-1-mach-copy-thm
"forall(sigma:istate, g, h, f, h%plus:[place -> place], v:sets[place],
h%ok(h,sigma)
and
ran(h) disj ran(default(sigma))
and
g%h%ok(g,h,sigma)
and
snapshot%not%visible(g,v)
and
h%plus=lambda (p:place, if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma), h%plus)
and
f=lambda(p:place, if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p, g(p)))
implies
user%eq(
a%copy(abstr(sigma), h%plus),
abstr(c%redirect(
(inverse{g} oo h))),
v))"
(theory places)
(proof
(
(apply-macete-with-minor-premises case-1-mach-copy)
(apply-macete-with-minor-premises g%h%ok-corollary)
(apply-macete-with-minor-premises silly-conditional-simplification)
(unfold-single-defined-constant-globally g%h%ok)
(unfold-single-defined-constant-globally h%ok)
(unfold-single-defined-constant-globally snapshot%not%visible)
insistent-direct-and-antecedent-inference-strategy
auto-instantiate-existential
insistent-direct-and-antecedent-inference-strategy)))
```

```
(def-theorem g%h%ok-dom-g-unbound
"forall(sigma:istate, g,h:[place -> place], p:place,
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and
p in dom{g}
implies
not p in bound%place(sigma))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally h%ok)
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
simplify)))
```

```
(def-theorem g%h%ok-dom-g-disj-dom-h
"forall(sigma:istate, g,h:[place -> place], p:place,
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and
p in dom{g}
implies
not p in dom{h})"
(theory places)
(proof
(
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(backchain "with(h,g:[place,place],dom{g} disj dom{h});"))))
```

```
(def-theorem g%h%ok-dom-h-disj-dom-g
"forall(sigma:istate, g,h:[place -> place], p:place,
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and p in dom{h}
implies
not p in dom{g})"
(theory places)
(proof
(
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(backchain "with(h,g:[place,place],dom{g} disj dom{h});"))))
```

```
(def-theorem default-c%copy-lower
"forall(sigma:istate,h%plus:[place,place],
default(c%copy(sigma,lower(sigma,h%plus)))
=lower(sigma,h%plus))"
(theory places)
(usages rewrite)
(proof
(
(unfold-single-defined-constant-globally c%copy)
(apply-macete-with-minor-premises lower-is-c%copy%fn)
simplify)))
```

```
(def-theorem lower-for-bound-place
"forall(sigma:istate, f:[place -> place], p:place,
p in bound%place(sigma) implies lower(sigma,f)(p)==default(sigma)(p))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally lower)
simplify)))
```

```
(def-theorem lower-for-unbound-place
"forall(sigma:istate, f:[place -> place], p:place,
not(p in bound%place(sigma)) implies lower(sigma,f)(p)==f(p))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally lower)
simplify)))
```

```
"forall(f,h%plus:[place,place],g:[place,place],sigma:istate,h:[place,place],
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma),h%plus)
and
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))),
p,
g(p)))
implies
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises silly-conditional-simplification)
(instantiate-existential ("g" "h"))
(block
(script-comment "`instantiate-existential' at (0 2)")
(incorporate-antecedent "with(sigma:istate,h:[place,place],h%ok(h,sigma));")
(unfold-single-defined-constant-globally h%ok)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`instantiate-existential' at (0 3)")
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy))))
```

```
"forall(sigma:istate, g,h,f,h%plus,h_delta:[place -> place], v:sets[place],
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and
snapshot%not%visible(g,v)
and
h%plus=lambda (p:place, if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma), h%plus)
and
f=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p, g(p)))
implies
(inverse{g}) oo (lower(sigma,h%plus)))))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally c%redirect)
beta-reduce-with-minor-premises
(move-to-sibling 1)
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
auto-instantiate-existential)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
simplify
(unfold-single-defined-constant-globally c%redirect%fn)
beta-reduce-with-minor-premises
(move-to-sibling 1)
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
(instantiate-existential ("g" "h")))
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(apply-macete-with-minor-premises gamma-c%copy-unchanged)
(apply-macete-with-minor-premises tr%range-composition)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(weaken (0 1))
(apply-macete-with-minor-premises tr%dom-of-inverse)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises tr%subseteq-transitivity)
(instantiate-existential ("ran{h}"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(antecedent-inference "with(p:prop,p);")
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(backchain "with(h,g:[place,place],ran{g}=ran{h});"))
(block
(script-comment "`instantiate-existential' at (0 0 1)")
(unfold-single-defined-constant-globally lower)
(backchain "with(p:prop,p and p and p and p and p and p);")
beta-reduce-insistently
simplify
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(antecedent-inference "with(p:prop,p and p and p and p and p and p);")
(contrapose "with(sigma:istate,h:[place,place],h%ok(h,sigma));")
(unfold-single-defined-constant-globally h%ok)
(contrapose "with(p,x_\$3:place,x_\$3=p);")
(auto-instantiate-universal-antecedent "with(h,g:[place,place],ran{g} subseteq ran{h});")
(antecedent-inference "with(p:prop,p and p);")
(auto-instantiate-universal-antecedent "with(sigma:istate,h:[place,place],
dom{h} disj bound%place(sigma));")
(contrapose "with(x:place,f:sets[place],not(x in f));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(antecedent-inference-strategy (0))
(apply-macete-with-minor-premises tr%injective-iff-injective-on-domain)
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy))
(move-to-ancestor 2)
(move-to-descendent (1))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(instantiate-existential ("g" "h")))
(move-to-ancestor 4)
(move-to-descendent (1))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(instantiate-existential ("g" "h")))
(move-to-ancestor 4)
(move-to-descendent (2))
(block
(script-comment "`apply-macete-with-minor-premises' at (2)")
(apply-macete-with-minor-premises c%copy-definedness)
(antecedent-inference-strategy (1)))
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises tr%ran-of-inverse)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(antecedent-inference-strategy (2))
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%injective-iff-injective-on-domain))
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0)")
extensionality
simplify-insistently
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"

("x_0"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises bound%place-characterization)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%first%entry-identity-in-set)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0 0)")
extensionality
simplify-insistently
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(lower(sigma,h%plus)(x_0))")
(contrapose "with(x_0:place,h%plus:[place,place],sigma:istate,
#(lower(sigma,h%plus)(x_0)));")
(unfold-single-defined-constant-globally lower)
(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")
beta-reduce
(raise-conditional (0))
(raise-conditional (0))
(contrapose "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
(antecedent-inference-strategy (0))
(block
(script-comment "`antecedent-inference-strategy' at (0)")
(contrapose "with(x_0:place,f:sets[place],x_0 in f);")
(backchain "with(p:prop,p and p and p and p);")
(move-to-ancestor 1)
(antecedent-inference-strategy (0))
(auto-instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));")
(instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"

("x_0"))
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`antecedent-inference-strategy' at (1 1)")
(contrapose "with(x_0:place,h:[place,place],#(h(x_0)));")
(antecedent-inference-strategy (0))
(instantiate-universal-antecedent "with(h,g:[place,place],dom{g} disj dom{h});"

("x_0"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(x_0:place,g:[place,place],not(x_0 in dom{g}));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(contrapose "with(x_0:place,h:[place,place],not(x_0 in dom{h}));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0 0 0 0 0)")
(cut-with-single-formula "x_\$3 in bound%place(c%copy(sigma,lower(sigma,h%plus)))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "#(lower(sigma,h%plus)(x_\$3))")
(move-to-sibling 1)
simplify
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(x_\$3:place,h%plus:[place,place],sigma:istate,
#(lower(sigma,h%plus)(x_\$3)));")
(unfold-single-defined-constant (0)

lower)
(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")
beta-reduce
(raise-conditional (0))
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(apply-macete-with-minor-premises bound%place%stability)
(apply-macete-with-minor-premises c%copy-definedness)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 1)")
(apply-macete-with-minor-premises bound%place-characterization)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
beta-reduce-insistently
(apply-macete-with-minor-premises gamma-c%copy-unchanged)
(move-to-ancestor 1)
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals)
(apply-macete-with-minor-premises tr%first%entry-equation)
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(apply-macete-locally-with-minor-premises default-c%copy-lower

(0)

"default(c%copy(sigma,lower(sigma,h%plus)))
(x_\$3)")
(apply-macete-with-minor-premises lower-for-unbound-place)
(force-substitution "h%plus(x_\$3)"

"if(x_\$3 in bound%place(sigma), x_\$3, h(x_\$3))"

(0))
(block
(script-comment "`force-substitution' at (0)")

simplify

(move-to-ancestor 1)

(raise-conditional (1))

direct-and-antecedent-inference-strategy

(cut-with-single-formula "h(x_\$3) in bound%place(c%copy(sigma,lower(sigma,h%plus)))")

(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(p:place,f:sets[place],p in f);")
(apply-macete-with-minor-premises bound%place-characterization)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals))

(block
(script-comment "`cut-with-single-formula' at (1)")
(incorporate-antecedent "with(sigma:istate,h:[place,place],h%ok(h,sigma));")
(unfold-single-defined-constant-globally h%ok)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(f:sets[place],f subseteq f);"
("h(x_\$3)"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(x_\$3:place,h:[place,place],not(h(x_\$3) in ran{h}));")
(apply-macete-with-minor-premises tr%in-range-condition))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(apply-macete-with-minor-premises bound%place%stability)
(apply-macete-with-minor-premises c%copy-definedness)
direct-and-antecedent-inference-strategy)))
(block
(script-comment "`force-substitution' at (1)")

(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")

beta-reduce))
(apply-macete-with-minor-premises c%copy-definedness))))
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-locally-with-minor-premises lower-for-bound-place

(0)

"lower(c%copy(sigma,lower(sigma,h%plus)),f)(x_\$3)")
(apply-macete-with-minor-premises default-c%copy-lower)
(cut-with-single-formula "not((iota(y:place,g(y)=lower(sigma,h%plus)(x_\$3))) in bound%place(c%copy(sigma,lower(sigma,h%plus))))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-locally-with-minor-premises lower-for-unbound-place

(0)

"lower(c%copy(sigma,lower(sigma,h%plus)),f)
(iota(y:place,g(y)=lower(sigma,h%plus)(x_\$3)))")
(backchain "with(g:[place,place],sigma:istate,f:[place,place],
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,f)), p, g(p))));")
beta-reduce-with-minor-premises
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(iota(y:place,g(y)=lower(sigma,h%plus)(x_\$3)))")
(eliminate-defined-iota-expression 0

a)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0 0 1 1)")
(cut-with-single-formula "#(lower(sigma,h%plus)(x_\$3))")
(incorporate-antecedent "with(x_\$3:place,f,g:[place,place],#(inverse{g}(f(x_\$3))));")
simplify-insistently))
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "#(lower(sigma,h%plus)(x_\$3))")
(incorporate-antecedent "with(x_\$3:place,f,g:[place,place],#(inverse{g}(f(x_\$3))));")
simplify
direct-inference
(eliminate-defined-iota-expression 0

a)
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(sigma:istate,g:[place,place],
dom{g} disj bound%place(sigma));"

("a"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(apply-macete-with-minor-premises bound%place-characterization)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%definedness-of-dangling-conditionals)
(apply-macete-with-minor-premises tr%first%entry-equation)
simplify
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises bound%place-characterization)
beta-reduce-insistently
(apply-macete-with-minor-premises tr%first%entry-identity-in-set))
(block
(script-comment "`direct-inference' at (1)")
(unfold-single-defined-constant (1)

lower)
(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")
(move-to-ancestor 1)
(force-substitution "h%plus(a)"

"if(a in bound%place(sigma), a, h(a))"

(0))
(block
(script-comment "`force-substitution' at (0)")

simplify

(instantiate-universal-antecedent "with(h,g:[place,place],dom{g} disj dom{h});"
("a"))

(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(a:place,g:[place,place],not(a in dom{g}));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))

(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(contrapose "with(a:place,h:[place,place],not(a in dom{h}));")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)))
(block
(script-comment "`force-substitution' at (1)")

(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")

beta-reduce)))))))))))))
```

```
(def-theorem case-3-mach-copy-thm
"forall(sigma:istate, g,h,f,h%plus,h_delta:[place -> place], v:sets[place],
h%ok(h,sigma)
and
g%h%ok(g,h,sigma)
and
snapshot%not%visible(g,v)
and
h%plus=lambda (p:place, if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma), h%plus)
and
f=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))), p, g(p)))
implies
user%eq(
a%copy(abstr(sigma), h%plus),
abstr(c%redirect(
(inverse{g}) oo (lower(sigma,h%plus)))),
v))"
(theory places)
(proof
(
(apply-macete-with-minor-premises c%redirect-no-op)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises rev%copy-liveness)
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises c%copy-definedness)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
insistent-direct-and-antecedent-inference-strategy
(block
(script-comment "`insistent-direct-and-antecedent-inference-strategy' at (0 0 0 0 0
0)")
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises c%copy-definedness)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
simplify-insistently
(backchain "with(g:[place,place],sigma:istate,f:[place,place],
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,f)), p, g(p))));")
(backchain "with(h:[place,place],sigma:istate,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p))));")
(move-to-ancestor 1)
beta-reduce
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(contrapose "with(v:sets[place],g:[place,place],
snapshot%not%visible(g,v));")
(unfold-single-defined-constant-globally snapshot%not%visible)
simplify-insistently
auto-instantiate-existential))
(block
(script-comment "`insistent-direct-and-antecedent-inference-strategy' at (0 0 1 0)")
simplify
(apply-macete-with-minor-premises c%copy-definedness)
(apply-macete-with-minor-premises a%copy-definedness)
direct-inference
(apply-macete-with-minor-premises copy-liveness)
(unfold-single-defined-constant-globally copy%fn)
(force-substitution "dom{a%copy(abstr(sigma),h%plus)}"
"bound%place(c%copy(sigma,lower(sigma,h%plus)))"
(0 1))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(apply-macete-with-minor-premises rev%copy-liveness)
(unfold-single-defined-constant-globally bound%place)
(move-to-ancestor 1)
extensionality
(block
(script-comment "`extensionality' at (0)")
beta-reduce
simplify
(apply-macete-with-minor-premises tr%value-of-a-defined-indicator-application)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises bound%place-abstr-definedness)
direct-and-antecedent-inference-strategy)
(apply-macete-with-minor-premises bound%place-abstr-definedness))
(block
(script-comment "`extensionality' at (1)")
(apply-macete-with-minor-premises bound%place-characterization)
(apply-macete-with-minor-premises c%copy-definedness)))
(block
(script-comment "`force-substitution' at (0)")
(backchain-repeatedly ("with(g,h%plus:[place,place],sigma:istate,f:[place,place],
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,lower(sigma,h%plus))),
p,
g(p))));"))
beta-reduce
simplify
(backchain "with(g:[place,place],sigma:istate,f:[place,place],
f
=lambda(p:place,
if(p in bound%place(c%copy(sigma,f)), p, g(p))));")
beta-reduce-insistently
simplify
(raise-conditional (0))
direct-and-antecedent-inference-strategy
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 1)")
(incorporate-antecedent "with(sigma:istate,h,g:[place,place],g%h%ok(g,h,sigma));")
(unfold-single-defined-constant-globally g%h%ok)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "x_\$0 in ran{h}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(sigma:istate,h:[place,place],h%ok(h,sigma));")
(unfold-single-defined-constant-globally h%ok)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises bound%place%stability)
(apply-macete-with-minor-premises c%copy-definedness)
direct-inference
(backchain "with(f:sets[place],f subseteq f);"))
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain-backwards "with(h,g:[place,place],ran{g}=ran{h});")
(backchain "with(p,x_\$0:place,x_\$0=p);")
(apply-macete-with-minor-premises tr%in-range-condition)))))))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
auto-instantiate-existential))))
```

```
(def-constant g%h%ok_2
"lambda(g,h:[place->place], s:sets[place], sigma:istate,
bijective_on_q{g,s,ran{h}}
and
dom(g) disj dom{gamma(sigma)}
and
dom(g) disj dom(h)
and
forall(p:place, #(g(p)) implies g(p)=default(sigma)(p)))"
(theory places))
```

```
(def-theorem empty-inters-iff-disjoint
"forall(s_0,s_1:sets[ind_1],
s_0 inters s_1=empty_indic{ind_1}
iff s_0 disj s_1)"
(theory pure-generic-theory-1)
(usages transportable-rewrite transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(contrapose "with(p:prop,p);")
extensionality
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
extensionality
simplify-insistently))))
```

```
(def-theorem lower-h%plus
"forall(sigma:istate,h,h%plus:[place,place],
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p)))
implies
lower(sigma,h%plus)=lower(sigma,h))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally lower)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,p);")
extensionality
beta-reduce
direct-inference
(case-split-on-conditionals (0)))))
```

```
(def-theorem g%h%ok_2-etc-implies-bound
"forall(sigma:istate,g,h:[place,place],s:sets[place],a:place,
g%h%ok_2(g,h,s,sigma) and h%ok(h,sigma) and a in s
implies
a in bound%place(sigma))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally g%h%ok_2)
(unfold-single-defined-constant-globally h%ok)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "default(sigma)(a) in bound%place(sigma)")
(apply-macete-with-minor-premises default-in-bound-place-implies-bound)
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain-backwards "forall(p:place,#(p) implies p=p);")
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
simplify)
(block
(script-comment "`direct-inference' at (1)")
(cut-with-single-formula "g(a) in ran{g}")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%in-range-condition)
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises tr%element-of-a-subset-is-an-element)
auto-instantiate-existential
(backchain "with(h,g:[place,place],ran{g}=ran{h});")))))))
```

```
(def-theorem g%h%ok_2-disjointness
"forall(sigma:istate, g,h:[place -> place], s:sets[place],
g%h%ok_2(g,h,s,sigma) implies dom{g} disj dom{h})"
(theory places)
(proof
(
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy)))
```

```
(def-theorem h%ok-implies-dom-unbound
"forall(sigma:istate, h:[place -> place], a:place,
h%ok(h,sigma) and a in dom{h} implies not(a in bound%place(sigma)))"
(theory places)
(proof
(
(unfold-single-defined-constant-globally h%ok)
simplify
(move-to-ancestor 1)
direct-and-antecedent-inference-strategy
(backchain "with(f:sets[place],f disj f);"))))
```

```
(def-theorem g%h%ok_2-iota-definedness
"forall(sigma:istate, g,h:[place -> place], s:sets[place], x:place,
g%h%ok_2(g,h,s,sigma) and x in dom{h} implies #(iota(y:place,g(y)=h(x))))"
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(sigma:istate,s:sets[place],h,g:[place,place],
g%h%ok_2(g,h,s,sigma));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(h(x))")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(block
(script-comment "`cut-with-single-formula' at (0)")
(eliminate-iota 0)
(contrapose "with(h,g:[place,place],ran{g}=ran{h});")
extensionality
beta-reduce-insistently
(instantiate-existential ("h(x)"))
simplify
direct-inference
(move-to-sibling 1)
(instantiate-existential ("x"))
(block
(script-comment "`direct-inference' at (0)")
(contrapose "with(p:prop,forall(y%iota:place,p or p or p));")
(antecedent-inference-strategy (0 1))
(instantiate-existential ("x_\$1"))
(backchain "with(g:[place,place],s:sets[place],injective_on_q{g,s});")
(force-substitution "s" "dom{g}" (0 1))
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
simplify)))))
```

```
(def-theorem case-2-mach-copy-thm
"forall(sigma:istate,g,h,h%plus:[place,place],s,v:sets[place],
h%ok(h,sigma)
and
g%h%ok_2(g,h,s,sigma)
and
snapshot%not%visible(g,v)
and
h%plus
=lambda(p:place,if(p in bound%place(sigma), p, h(p)))
and
copy%fn(abstr(sigma),h%plus)
implies
user%eq(a%copy(abstr(sigma),h%plus),
abstr(c%redirect(c%copy(sigma,lower(sigma,h%plus)),
(inverse{g}) oo h)),
v))"
(theory places)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises c%redirect-no-op)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises copy-liveness)
(unfold-single-defined-constant-globally user%eq))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(unfold-single-defined-constant-globally c%redirect)
simplify
(unfold-single-defined-constant-globally c%redirect%fn)
(apply-macete-with-minor-premises tr%range-composition)
(apply-macete-with-minor-premises tr%ran-of-inverse)
(apply-macete-with-minor-premises gamma-c%copy-unchanged)
(apply-macete-with-minor-premises tr%domain-composition)
(move-to-ancestor 4)
(move-to-descendent (1))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(weaken (0 1))
(move-to-ancestor 2)
(move-to-descendent (0 1))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(weaken (0 1))
(move-to-ancestor 2)
(move-to-descendent (0 0 1))
(weaken (1))
(move-to-ancestor 2)
(move-to-descendent (0))
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-locally-with-minor-premises tr%intersection-commutativity

(0)

"dom{h} inters dom{g}=empty_indic{place}")
(apply-macete-with-minor-premises tr%empty-inters-iff-disjoint)
(incorporate-antecedent "with(sigma:istate,s:sets[place],h,g:[place,place],
g%h%ok_2(g,h,s,sigma));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises default-c%copy-lower)
(instantiate-theorem lower-h%plus
("sigma" "h" "h%plus"))
(backchain-repeatedly ("with(h,h%plus:[place,place],sigma:istate,
lower(sigma,h%plus)=lower(sigma,h));"))
(unfold-single-defined-constant-globally lower)
(instantiate-theorem h%ok-implies-dom-unbound
("sigma" "h" "x_\$3"))
(instantiate-theorem g%h%ok_2-iota-definedness
("sigma" "g" "h" "s" "x_\$3"))
(block
(script-comment "`instantiate-theorem' at (0 0 0)")
(contrapose "with(sigma:istate,s:sets[place],h,g:[place,place],
not(g%h%ok_2(g,h,s,sigma)));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
insistent-direct-and-antecedent-inference-strategy)
(block
(script-comment "`instantiate-theorem' at (0 1)")
simplify-insistently
beta-reduce-insistently
(cut-with-single-formula "#(h(x_\$3))")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(block
(script-comment "`cut-with-single-formula' at (0)")
beta-reduce-insistently
(apply-macete-with-minor-premises g%h%ok_2-etc-implies-bound)
(instantiate-theorem g%h%ok_2-etc-implies-bound
("sigma" "g"

"h"

"s"

"iota(y:place,g(y)=h(x_\$3))"))
(block
(script-comment "`instantiate-theorem' at (0 0 0)")
(contrapose "with(sigma:istate,s:sets[place],h,g:[place,place],
not(g%h%ok_2(g,h,s,sigma)));")
(unfold-single-defined-constant-globally g%h%ok_2)
insistent-direct-and-antecedent-inference-strategy)
(block
(script-comment "`instantiate-theorem' at (0 0 2)")
(contrapose "with(p:prop,s:sets[place],not(iota(y:place,p) in s));")
(eliminate-defined-iota-expression 0

b)
(backchain-backwards "with(s:sets[place],g:[place,place],dom{g}=s);")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-theorem' at (0 1)")
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(backchain-backwards "with(p:prop,forall(p:place,with(p:prop,p implies p)));")
direct-inference
(eliminate-defined-iota-expression 0

c)
(eliminate-defined-iota-expression 0

d)))))
(block
(script-comment "`apply-macete-with-minor-premises' at (1 0)")
(apply-macete-with-minor-premises tr%dom-of-inverse)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(incorporate-antecedent "with(sigma:istate,s:sets[place],h,g:[place,place],
g%h%ok_2(g,h,s,sigma));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
(backchain "with(h,g:[place,place],ran{g}=ran{h});"))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(weaken (0 1))
(incorporate-antecedent "with(sigma:istate,s:sets[place],h,g:[place,place],
g%h%ok_2(g,h,s,sigma));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%injective-iff-injective-on-domain)
(backchain "with(s:sets[place],g:[place,place],dom{g}=s);"))))
(block
(script-comment "`apply-macete-with-minor-premises' at (1 0)")
(apply-macete-with-minor-premises tr%dom-of-inverse)
(incorporate-antecedent "with(sigma:istate,s:sets[place],h,g:[place,place],
g%h%ok_2(g,h,s,sigma));")
(unfold-single-defined-constant-globally g%h%ok_2)
direct-and-antecedent-inference-strategy
(backchain "with(h,g:[place,place],ran{g}=ran{h});")))))))
```