Proofs for file C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd

Generated by Perfect Developer at 11:15:33 UTC on Tuesday January 17th 2006

Tool file versions: PDTool 3.03.03, builtin 3.03, rubric 3.03.03

Proved 30 of 30 verification conditions.

Proof of verification condition: Type constraint for 'nat' satisfied
In the context of class: AbPurse, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (9,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (27,14)
To prove: 0 ≤ (self.balance + (amt as int))
Given: 0 ≤ amt
Proof:
[Take goal term]
[1.0] 0 ≤ (self.balance + (amt as int))
→ [simplify]
[1.3] -1 < (self.balance + amt)
→ [negate goal and search for contradiction]
[1.4] ~(-1 < (self.balance + amt))
→ [simplify]
[1.7] 0 < (-self.balance + -amt)
[Take given term]
[2.0] 0 ≤ amt
→ [simplify]
[2.2] -1 < amt
[Assume known post-assertion, class invariant or type constraint for term 1.7]
[3.0] 0 ≤ self.balance
→ [simplify]
[3.2] -1 < self.balance
[Create new term from terms 1.7, 3.2 using rule: transitivity 2]
[4.0] (-1 + 0 + 1) < -amt
→ [simplify]
[4.1] 0 < -amt
→ [from term 2.2, literala < -amt is false whenever -2 < (-1 + literala)]

Proof of rule precondition:
[4.1.0] -2 < (-1 + 0)
→ [simplify]
[4.1.2] true

[4.2] false
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Type constraint for 'nat' satisfied
In the context of class: AbPurse, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (9,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (18,29)
To prove: 0 ≤ (self.lost + (amt as int))
Given: 0 ≤ amt, amt ≤ self.balance, (self.balance - (amt as int)) = self′.balance
Proof:
[Take goal term]
[1.0] 0 ≤ (self.lost + (amt as int))
→ [simplify]
[1.3] -1 < (self.lost + amt)
→ [negate goal and search for contradiction]
[1.4] ~(-1 < (self.lost + amt))
→ [simplify]
[1.7] 0 < (-self.lost + -amt)
[Take given term]
[2.0] 0 ≤ amt
→ [simplify]
[2.2] -1 < amt
[Assume known post-assertion, class invariant or type constraint for term 1.7]
[7.0] 0 ≤ self.lost
→ [simplify]
[7.2] -1 < self.lost
[Create new term from terms 1.7, 7.2 using rule: transitivity 2]
[8.0] (-1 + 0 + 1) < -amt
→ [simplify]
[8.1] 0 < -amt
→ [from term 2.2, literala < -amt is false whenever -2 < (-1 + literala)]

Proof of rule precondition:
[8.1.0] -2 < (-1 + 0)
→ [simplify]
[8.1.2] true

[8.2] false
(Rewriter time: 0.0s, Prover time: 0.1s)

Proof of verification condition: Type constraint for 'nat' satisfied
In the context of class: AbPurse, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (9,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (18,14)
To prove: 0 ≤ (self.balance - (amt as int))
Given: 0 ≤ amt, amt ≤ self.balance
Proof:
[Take given term]
[3.0] amt ≤ self.balance
→ [simplify]
[3.7] -1 < (-amt + self.balance)
[Take goal term]
[1.0] 0 ≤ (self.balance - (amt as int))
→ [simplify]
[1.4] -1 < (-amt + self.balance)
→ [from term 3.7, literala < (-amt + self.balance) is true whenever -1 < (-1 + -literala)]

Proof of rule precondition:
[1.4.0] -1 < (-1 + --1)
→ [simplify]
[1.4.3] true

[1.5] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Type constraint for 'nat' satisfied
In the context of class: AbPurse, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (9,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (23,14)
To prove: 0 ≤ (self.balance - (amt as int))
Given: 0 ≤ amt, amt ≤ self.balance
Proof:
[Take given term]
[3.0] amt ≤ self.balance
→ [simplify]
[3.7] -1 < (-amt + self.balance)
[Take goal term]
[1.0] 0 ≤ (self.balance - (amt as int))
→ [simplify]
[1.4] -1 < (-amt + self.balance)
→ [from term 3.7, literala < (-amt + self.balance) is true whenever -1 < (-1 + -literala)]

Proof of rule precondition:
[1.4.0] -1 < (-1 + --1)
→ [simplify]
[1.4.3] true

[1.5] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Type constraint satisfied
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (31,36)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (83,18)
To prove: 0 ≤ 0
Given: self ≈ (anything{} to AbPurse), self′.balance = (0 as nat)
Proof:
[Take goal term]
[1.0] 0 ≤ 0
→ [simplify]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Type constraint satisfied
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (31,25)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (83,18)
To prove: 0 ≤ 0
Given: self ≈ (anything{} to AbPurse)
Proof:
[Take goal term]
[1.0] 0 ≤ 0
→ [simplify]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'lose' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (80,105)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (17,17)
To prove: details.val ≤ it.balance
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to), self.SufficientFundsProperty(details), it = self.AbAuthPurse[details.frm]
Proof:
[Take given term]
[5.0] self.SufficientFundsProperty(details)
[Take given term]
[7.0] self.AbAuthPurse[details.frm] = it
[Take goal term]
[1.0] details.val ≤ it.balance
→ [from term 7.0, it is equal to self.AbAuthPurse[details.frm]]
[1.1] details.val ≤ self.AbAuthPurse[details.frm].balance
→ [simplify]
[1.8] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)
→ [negate goal and search for contradiction]
[1.9] ~(-1 < (-details.val + self.AbAuthPurse[details.frm].balance))
→ [simplify]
[1.13] 0 < (details.val + -self.AbAuthPurse[details.frm].balance)
[Copy term 5.0]
[15.0] self.SufficientFundsProperty(details)
→ [expand function]

Expansion detail:
[15.0.0] self.SufficientFundsProperty(details)
→ [expand function 'SufficientFundsProperty']
[15.0.1] details.val ≤ self.AbAuthPurse[details.frm].balance
→ [simplify]
[15.0.8] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)

[15.1] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)
→ [from term 1.13, literala < (-details.val + self.AbAuthPurse[details.frm].balance) is false whenever -2 < (0 + literala)]

Proof of rule precondition:
[15.1.0] -2 < (-1 + 0)
→ [simplify]
[15.1.2] true

Expansion detail:
[15.0.0] self.SufficientFundsProperty(details)
→ [expand function 'SufficientFundsProperty']
[15.0.1] details.val ≤ self.AbAuthPurse[details.frm].balance
→ [simplify]
[15.0.8] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)

[15.1] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)
→ [from term 1.13, literala < (-details.val + self.AbAuthPurse[details.frm].balance) is false whenever -2 < (0 + literala)]

Proof of rule precondition:
[15.1.0] -2 < (-1 + 0)
→ [simplify]
[15.1.2] true

[15.2] false
(Rewriter time: 0.0s, Prover time: 0.4s)

Proof of verification condition: Precondition of '[]' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (89,82)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (760,15)
To prove: details.frm in self.AbAuthPurse.dom
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to), self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[2.1] details.frm in self.AbAuthPurse
→ [simplify]
[2.2] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] details.frm in self.AbAuthPurse.dom
→ [from term 2.2, details.frm in self.AbAuthPurse.dom is true]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'replace' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (89,48)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (802,15)
To prove: details.frm in self.AbAuthPurse
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to), self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[2.1] details.frm in self.AbAuthPurse
→ [simplify]
[2.2] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] details.frm in self.AbAuthPurse
→ [simplify]
[1.1] details.frm in self.AbAuthPurse.dom
→ [from term 2.2, details.frm in self.AbAuthPurse.dom is true]
[1.2] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of '[]' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (90,81)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (760,15)
To prove: details.to in self.AbAuthPurse.dom
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to), self.SufficientFundsProperty(details)
Proof:
[Take given term]
[3.0] self.Authentic(details.to)
→ [expand function 'Authentic']
[3.1] details.to in self.AbAuthPurse
→ [simplify]
[3.2] details.to in self.AbAuthPurse.dom
[Take goal term]
[1.0] details.to in self.AbAuthPurse.dom
→ [from term 3.2, details.to in self.AbAuthPurse.dom is true]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'replace' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (90,48)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (802,15)
To prove: details.to in self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val))
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to), self.SufficientFundsProperty(details)
Proof:
[Take given term]
[3.0] self.Authentic(details.to)
→ [expand function 'Authentic']
[3.1] details.to in self.AbAuthPurse
→ [simplify]
[3.2] details.to in self.AbAuthPurse.dom
[Take goal term]
[1.0] details.to in self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val))
→ [simplify]
[1.2] details.to in self.AbAuthPurse.dom
→ [from term 3.2, details.to in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of '[]' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (66,38)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Bin\builtin.pd (760,15)
To prove: details.frm in self.AbAuthPurse.dom
Given: self.Authentic(details.frm)
Proof:
[Take given term]
[2.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[2.1] details.frm in self.AbAuthPurse
→ [simplify]
[2.2] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] details.frm in self.AbAuthPurse.dom
→ [from term 2.2, details.frm in self.AbAuthPurse.dom is true]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Post-assertion valid
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (94,14)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (103,37)
To prove: self′.totalAbBalance ≤ self.totalAbBalance
Given: (opaque [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details)), forall $x::$attributeNames(AbWorld) • different(self′.$x; [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: self′, [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: self′, [true]: self′) ==> self.$x=self′.$x
Proof:
[Take goal term]
[1.0] self′.totalAbBalance ≤ self.totalAbBalance
→ [simplify]
[1.7] -1 < (-self′.totalAbBalance + self.totalAbBalance)
→ [negate goal and search for contradiction]
[1.8] ~(-1 < (-self′.totalAbBalance + self.totalAbBalance))
→ [simplify]
[1.12] 0 < (self′.totalAbBalance + -self.totalAbBalance)
[Take given term]
[2.0] (opaque [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.1] (opaque [(((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.2] (opaque [(((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.3] (opaque [(((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.9] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.10] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.11] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.12] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.18] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
[Copy term 1.12]
[18.0] 0 < (-self.totalAbBalance + self′.totalAbBalance)
→ [expand function]

Expansion detail 1:
[18.0.0.0] self.totalAbBalance
→ [expand function 'totalAbBalance']
[18.0.0.1] + over (for x::self.AbAuthPurse.ranb yield x.balance)
Expansion detail 2:
[18.0.1.0] self′.totalAbBalance
→ [expand function 'totalAbBalance']
[18.0.1.1] + over (for x::self′.AbAuthPurse.ranb yield x.balance)

[18.1] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self′.AbAuthPurse.ranb yield x.balance)))
[From definition temp_g_2 = self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)]
[31.0] {self.AbAuthPurse[details.frm]→temp_g_2}!lose(details.val)
[Copy term 31.0]
[32.0] {self.AbAuthPurse[details.frm]→temp_g_2}!lose(details.val)
→ [expand schema 'lose']
[32.1] ((self.AbAuthPurse[details.frm].lost + (details.val as int)) = temp_g_2.lost) .& ((self.AbAuthPurse[details.frm].balance - (details.val as int)) = temp_g_2.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_g_2.$x; self′.balance, self′.lost) ==> self.AbAuthPurse[details.frm].$x=temp_g_2.$x)
→ [simplify]
[32.8] (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val)) .& (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (forall $x::$attributeNames(AbPurse) • different(temp_g_2.$x; self′.balance, self′.lost) ==> self.AbAuthPurse[details.frm].$x=temp_g_2.$x)
→ [expand all members]
[32.9] (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val)) .& (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& ((forall $x::$attributeNames(int) • different(temp_g_2.lost.$x; lost) ==> self.AbAuthPurse[details.frm].lost.$x=temp_g_2.lost.$x) .& (forall $x::$attributeNames(int) • different(temp_g_2.balance.$x; balance) ==> self.AbAuthPurse[details.frm].balance.$x=temp_g_2.balance.$x))
→ [simplify]
[32.13] (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val))
→ [separate conjunction and work on first sub-term]
[32.14] 0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)
[From definition temp_l_1_2 = self.AbAuthPurse[details.to] after {it→it′}!add(details.val)]
[64.0] {self.AbAuthPurse[details.to]→temp_l_1_2}!add(details.val)
[From definition temp_l_1_3 = self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)]
[65.0] {self.AbAuthPurse[details.frm]→temp_l_1_3}!remove(details.val)
[Copy term 64.0]
[66.0] {self.AbAuthPurse[details.to]→temp_l_1_2}!add(details.val)
→ [expand schema 'add']
[66.1] ((self.AbAuthPurse[details.to].balance + (details.val as int)) = temp_l_1_2.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_2.$x; self′.balance) ==> self.AbAuthPurse[details.to].$x=temp_l_1_2.$x)
→ [simplify]
[66.4] (0 = (-temp_l_1_2.balance + self.AbAuthPurse[details.to].balance + details.val)) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_2.$x; self′.balance) ==> self.AbAuthPurse[details.to].$x=temp_l_1_2.$x)
→ [expand all members]
[66.5] (0 = (-temp_l_1_2.balance + self.AbAuthPurse[details.to].balance + details.val)) .& ((self.AbAuthPurse[details.to].lost = temp_l_1_2.lost) .& (forall $x::$attributeNames(int) • different(temp_l_1_2.balance.$x; balance) ==> self.AbAuthPurse[details.to].balance.$x=temp_l_1_2.balance.$x))
→ [simplify]
[66.8] (0 = (-temp_l_1_2.balance + self.AbAuthPurse[details.to].balance + details.val)) .& (0 = (-temp_l_1_2.lost + self.AbAuthPurse[details.to].lost))
→ [separate conjunction and work on first sub-term]
[66.9] 0 = (-temp_l_1_2.balance + self.AbAuthPurse[details.to].balance + details.val)
[Copy term 65.0]
[70.0] {self.AbAuthPurse[details.frm]→temp_l_1_3}!remove(details.val)
→ [expand schema 'remove']
[70.1] ((self.AbAuthPurse[details.frm].balance - (details.val as int)) = temp_l_1_3.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_3.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_3.$x)
→ [simplify]
[70.5] (0 = (-temp_l_1_3.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_3.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_3.$x)
Proof branches here giving 3 sub-goals:

Proof of sub-goal 1:
[Branch on disjunction or conditional in term 2.18 and work on branch 1]
[4.0] {self→self′}!AbTransferLost(details)
[Branch on disjunction or conditional in term 2.18 and work on branch 1]
[5.0] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 4 of conjunction in term 5.0]
[8.0] self.SufficientFundsProperty(details)
[Copy term 4.0]
[9.0] {self→self′}!AbTransferLost(details)
→ [expand schema 'AbTransferLost']
[9.1] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))) .& (forall $x::$attributeNames(AbWorld) • different(self′.$x; self′.AbAuthPurse) ==> self.$x=self′.$x)
→ [expand all members]
[9.2] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))) .& (forall $x::$attributeNames(map of (NAME → AbPurse)) • different(self′.AbAuthPurse.$x; AbAuthPurse) ==> self.AbAuthPurse.$x=self′.AbAuthPurse.$x)
→ [simplify]
[9.4] self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))
[Copy term 8.0]
[23.0] self.SufficientFundsProperty(details)
→ [expand function]
- Expansion detail:
  [23.0.0] self.SufficientFundsProperty(details)
  → [expand function 'SufficientFundsProperty']
  [23.0.1] details.val ≤ self.AbAuthPurse[details.frm].balance
  → [simplify]
  [23.0.8] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)
[23.1] -1 < (-details.val + self.AbAuthPurse[details.frm].balance)
[Assume known post-assertion, class invariant or type constraint for term 23.1]
[24.0] 0 ≤ details.val
→ [simplify]
[24.2] -1 < details.val
[Copy term 18.1]
[19.0] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self′.AbAuthPurse.ranb yield x.balance)))
→ [from term 9.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))]
[19.1] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).ranb yield x.balance)))
→ [+ over for..yield of replace]
[19.2] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (((self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - self.AbAuthPurse[details.frm].balance))
→ [simplify]
[19.7] 0 < (-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance)
→ [introduce variable 'temp_g_2' defined as self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)]
[19.8] 0 < (-self.AbAuthPurse[details.frm].balance + temp_g_2.balance)
→ [from term 32.14, temp_g_2.balance is equal to -details.val + self.AbAuthPurse[details.frm].balance]
[19.9] 0 < (-self.AbAuthPurse[details.frm].balance + (-details.val + self.AbAuthPurse[details.frm].balance))
→ [simplify]
[19.12] 0 < -details.val
→ [from term 24.2, literala < -details.val is false whenever -2 < (-1 + literala)]
- Proof of rule precondition:
  [19.12.0] -2 < (-1 + 0)
  → [simplify]
  [19.12.2] true
[19.13] false
Proof of sub-goal 2:
[Work on branch 2 from term 2.18]
[36.0] {self→self′}!AbTransferOkay(details)
[Work on branch 2 from term 2.18]
[37.0] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
→ [separate conjunction and work on first sub-term]
[37.1] ~(details.frm = details.to)
[Copy term 36.0]
[41.0] {self→self′}!AbTransferOkay(details)
→ [expand schema 'AbTransferOkay']
[41.1] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))) .& (forall $x::$attributeNames(AbWorld) • different(self′.$x; self′.AbAuthPurse) ==> self.$x=self′.$x)
→ [expand all members]
[41.2] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))) .& (forall $x::$attributeNames(map of (NAME → AbPurse)) • different(self′.AbAuthPurse.$x; AbAuthPurse) ==> self.AbAuthPurse.$x=self′.AbAuthPurse.$x)
→ [simplify]
[41.4] self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))
[Copy term 18.1]
[44.0] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self′.AbAuthPurse.ranb yield x.balance)))
→ [from term 41.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))]
[44.1] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).ranb yield x.balance)))
→ [+ over for..yield of replace]
[44.3] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (((self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (((self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - self.AbAuthPurse[details.frm].balance)) - self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val))[details.to].balance))
→ [simplify]
[44.7] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + ((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), []: self.AbAuthPurse[details.to]).balance))
→ [explicitly assert falsehood of skipped guards in subsequent guards]
[44.8] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + ((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~(details.frm ≈ details.to)]: self.AbAuthPurse[details.to]).balance))
→ [from term 37.1, details.frm = details.to is false]
[44.10] 0 < (-(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + ((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([false]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~false]: self.AbAuthPurse[details.to]).balance))
→ [simplify]
[44.17] 0 < (-self.AbAuthPurse[details.frm].balance + -self.AbAuthPurse[details.to].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance)
→ [introduce variable 'temp_l_1_2' defined as self.AbAuthPurse[details.to] after {it→it′}!add(details.val)]
[44.18] 0 < (-self.AbAuthPurse[details.frm].balance + -self.AbAuthPurse[details.to].balance + temp_l_1_2.balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance)
→ [introduce variable 'temp_l_1_3' defined as self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)]
[44.19] 0 < (-self.AbAuthPurse[details.frm].balance + -self.AbAuthPurse[details.to].balance + temp_l_1_2.balance + temp_l_1_3.balance)
→ [from term 66.9, temp_l_1_2.balance is equal to self.AbAuthPurse[details.to].balance + details.val]
[44.20] 0 < (-self.AbAuthPurse[details.frm].balance + -self.AbAuthPurse[details.to].balance + (self.AbAuthPurse[details.to].balance + details.val) + temp_l_1_3.balance)
→ [simplify]
[44.23] 0 < (-self.AbAuthPurse[details.frm].balance + temp_l_1_3.balance + details.val)
[Retrieve term developed earlier]
[70.5] (0 = (-temp_l_1_3.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_3.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_3.$x)
→ [from term 44.23, (-temp_l_1_3.balance + -details.val + self.AbAuthPurse[details.frm].balance) = literala is false whenever -1 < (0 + literala)]
- Proof of rule precondition:
  [70.5.0] -1 < (0 + 0)
  → [simplify]
  [70.5.2] true
[70.6] false .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_3.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_3.$x)
→ [simplify]
[70.7] false
Proof of sub-goal 3:
[Work on branch 3 from term 2.18]
[71.0] {self→self′}!AbIgnore(details)
[Copy term 71.0]
[89.0] {self→self′}!AbIgnore(details)
→ [expand schema 'AbIgnore']
[89.1] (self′ as from AbWorld) = (self as from AbWorld)
→ [simplify]
[89.2] self = self′
[Copy term 1.12]
[90.0] 0 < (-self.totalAbBalance + self′.totalAbBalance)
→ [from term 89.2, self′ is equal to self]
[90.1] 0 < (-self.totalAbBalance + self.totalAbBalance)
→ [simplify]
[90.3] false

(Rewriter time: 0.0s, Prover time: 14.7s)

Proof of verification condition: Post-assertion valid
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (94,14)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (104,57)
To prove: (self.totalAbBalance + self.totalAbLost) = (self′.totalAbBalance + self′.totalAbLost)
Given: (opaque [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details)), forall $x::$attributeNames(AbWorld) • different(self′.$x; [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: self′, [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: self′, [true]: self′) ==> self.$x=self′.$x
Proof:
[Take goal term]
[1.0] (self.totalAbBalance + self.totalAbLost) = (self′.totalAbBalance + self′.totalAbLost)
→ [simplify]
[1.3] 0 = (-self′.totalAbBalance + -self′.totalAbLost + self.totalAbBalance + self.totalAbLost)
→ [negate goal and search for contradiction]
[1.4] ~(0 = (-self′.totalAbBalance + -self′.totalAbLost + self.totalAbBalance + self.totalAbLost))
[Take given term]
[2.0] (opaque [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.1] (opaque [(((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.2] (opaque [(((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.3] (opaque [(((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.9] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.10] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.11] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [expand function 'Authentic']
[2.12] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [(((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
→ [simplify]
[2.18] (opaque [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferLost(details), [~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)]: {self→self′}!AbTransferOkay(details), [true]: {self→self′}!AbIgnore(details))
[Copy term 1.4]
[20.0] ~(0 = (-self′.totalAbBalance + -self′.totalAbLost + self.totalAbBalance + self.totalAbLost))
→ [expand function]

Expansion detail 1:
[20.0.0.0] self′.totalAbBalance
→ [expand function 'totalAbBalance']
[20.0.0.1] + over (for x::self′.AbAuthPurse.ranb yield x.balance)
Expansion detail 2:
[20.0.1.0] self′.totalAbLost
→ [expand function 'totalAbLost']
[20.0.1.1] + over (for x::self′.AbAuthPurse.ranb yield x.lost)
Expansion detail 3:
[20.0.2.0] self.totalAbBalance
→ [expand function 'totalAbBalance']
[20.0.2.1] + over (for x::self.AbAuthPurse.ranb yield x.balance)
Expansion detail 4:
[20.0.3.0] self.totalAbLost
→ [expand function 'totalAbLost']
[20.0.3.1] + over (for x::self.AbAuthPurse.ranb yield x.lost)

[20.1] ~(0 = (-(+ over (for x::self′.AbAuthPurse.ranb yield x.balance)) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
[From definition temp_g_2 = self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)]
[35.0] {self.AbAuthPurse[details.frm]→temp_g_2}!lose(details.val)
[Copy term 35.0]
[36.0] {self.AbAuthPurse[details.frm]→temp_g_2}!lose(details.val)
→ [expand schema 'lose']
[36.1] ((self.AbAuthPurse[details.frm].lost + (details.val as int)) = temp_g_2.lost) .& ((self.AbAuthPurse[details.frm].balance - (details.val as int)) = temp_g_2.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_g_2.$x; self′.balance, self′.lost) ==> self.AbAuthPurse[details.frm].$x=temp_g_2.$x)
→ [simplify]
[36.8] (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val)) .& (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (forall $x::$attributeNames(AbPurse) • different(temp_g_2.$x; self′.balance, self′.lost) ==> self.AbAuthPurse[details.frm].$x=temp_g_2.$x)
→ [expand all members]
[36.9] (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val)) .& (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& ((forall $x::$attributeNames(int) • different(temp_g_2.lost.$x; lost) ==> self.AbAuthPurse[details.frm].lost.$x=temp_g_2.lost.$x) .& (forall $x::$attributeNames(int) • different(temp_g_2.balance.$x; balance) ==> self.AbAuthPurse[details.frm].balance.$x=temp_g_2.balance.$x))
→ [simplify]
[36.13] (0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val))
→ [separate conjunction and work on first sub-term]
[36.14] 0 = (-temp_g_2.balance + -details.val + self.AbAuthPurse[details.frm].balance)
[Work on sub-term 2 of conjunction in term 36.13]
[37.0] 0 = (-temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val)
[From definition temp_l_1_0 = self.AbAuthPurse[details.to] after {it→it′}!add(details.val)]
[67.0] {self.AbAuthPurse[details.to]→temp_l_1_0}!add(details.val)
[From definition temp_l_1_1 = self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)]
[68.0] {self.AbAuthPurse[details.frm]→temp_l_1_1}!remove(details.val)
[Copy term 67.0]
[69.0] {self.AbAuthPurse[details.to]→temp_l_1_0}!add(details.val)
→ [expand schema 'add']
[69.1] ((self.AbAuthPurse[details.to].balance + (details.val as int)) = temp_l_1_0.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_0.$x; self′.balance) ==> self.AbAuthPurse[details.to].$x=temp_l_1_0.$x)
→ [simplify]
[69.4] (0 = (-temp_l_1_0.balance + self.AbAuthPurse[details.to].balance + details.val)) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_0.$x; self′.balance) ==> self.AbAuthPurse[details.to].$x=temp_l_1_0.$x)
→ [expand all members]
[69.5] (0 = (-temp_l_1_0.balance + self.AbAuthPurse[details.to].balance + details.val)) .& ((self.AbAuthPurse[details.to].lost = temp_l_1_0.lost) .& (forall $x::$attributeNames(int) • different(temp_l_1_0.balance.$x; balance) ==> self.AbAuthPurse[details.to].balance.$x=temp_l_1_0.balance.$x))
→ [simplify]
[69.8] (0 = (-temp_l_1_0.balance + self.AbAuthPurse[details.to].balance + details.val)) .& (0 = (-temp_l_1_0.lost + self.AbAuthPurse[details.to].lost))
→ [separate conjunction and work on first sub-term]
[69.9] 0 = (-temp_l_1_0.balance + self.AbAuthPurse[details.to].balance + details.val)
[Copy term 68.0]
[71.0] {self.AbAuthPurse[details.frm]→temp_l_1_1}!remove(details.val)
→ [expand schema 'remove']
[71.1] ((self.AbAuthPurse[details.frm].balance - (details.val as int)) = temp_l_1_1.balance) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_1.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_1.$x)
→ [simplify]
[71.5] (0 = (-temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (forall $x::$attributeNames(AbPurse) • different(temp_l_1_1.$x; self′.balance) ==> self.AbAuthPurse[details.frm].$x=temp_l_1_1.$x)
→ [expand all members]
[71.6] (0 = (-temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& ((self.AbAuthPurse[details.frm].lost = temp_l_1_1.lost) .& (forall $x::$attributeNames(int) • different(temp_l_1_1.balance.$x; balance) ==> self.AbAuthPurse[details.frm].balance.$x=temp_l_1_1.balance.$x))
→ [simplify]
[71.9] (0 = (-temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (0 = (-temp_l_1_1.lost + self.AbAuthPurse[details.frm].lost))
Proof branches here giving 3 sub-goals:

Proof of sub-goal 1:
[Branch on disjunction or conditional in term 2.18 and work on branch 1]
[4.0] {self→self′}!AbTransferLost(details)
[Copy term 4.0]
[9.0] {self→self′}!AbTransferLost(details)
→ [expand schema 'AbTransferLost']
[9.1] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))) .& (forall $x::$attributeNames(AbWorld) • different(self′.$x; self′.AbAuthPurse) ==> self.$x=self′.$x)
→ [expand all members]
[9.2] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))) .& (forall $x::$attributeNames(map of (NAME → AbPurse)) • different(self′.AbAuthPurse.$x; AbAuthPurse) ==> self.AbAuthPurse.$x=self′.AbAuthPurse.$x)
→ [simplify]
[9.4] self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))
[Copy term 20.1]
[23.0] ~(0 = (-(+ over (for x::self′.AbAuthPurse.ranb yield x.balance)) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 9.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))]
[23.1] ~(0 = (-(+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).ranb yield x.balance)) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [+ over for..yield of replace]
[23.2] ~(0 = (-(((self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - self.AbAuthPurse[details.frm].balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[23.8] ~(0 = ((-(self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 9.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val))]
[23.9] ~(0 = ((-(self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance) + -(+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [+ over for..yield of replace]
[23.10] ~(0 = ((-(self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance) + -(((self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).lost + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))) - self.AbAuthPurse[details.frm].lost) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[23.21] ~(0 = (-(self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)).lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].lost))
→ [introduce variable 'temp_g_2' defined as self.AbAuthPurse[details.frm] after {it→it′}!lose(details.val)]
[23.23] ~(0 = (-temp_g_2.balance + -temp_g_2.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].lost))
→ [from term 36.14, temp_g_2.balance is equal to -details.val + self.AbAuthPurse[details.frm].balance]
[23.24] ~(0 = (-(-details.val + self.AbAuthPurse[details.frm].balance) + -temp_g_2.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].lost))
→ [simplify]
[23.27] ~(0 = (-self.AbAuthPurse[details.frm].balance + -temp_g_2.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].lost + details.val))
→ [from term 37.0, -temp_g_2.lost + self.AbAuthPurse[details.frm].lost + details.val is equal to 0]
[23.28] ~(0 = (0 + -self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].balance))
→ [simplify]
[23.32] false
Proof of sub-goal 2:
[Work on branch 2 from term 2.18]
[38.0] {self→self′}!AbTransferOkay(details)
[Work on branch 2 from term 2.18]
[39.0] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
→ [separate conjunction and work on first sub-term]
[39.1] ~(details.frm = details.to)
[Copy term 38.0]
[43.0] {self→self′}!AbTransferOkay(details)
→ [expand schema 'AbTransferOkay']
[43.1] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))) .& (forall $x::$attributeNames(AbWorld) • different(self′.$x; self′.AbAuthPurse) ==> self.$x=self′.$x)
→ [expand all members]
[43.2] (self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))) .& (forall $x::$attributeNames(map of (NAME → AbPurse)) • different(self′.AbAuthPurse.$x; AbAuthPurse) ==> self.AbAuthPurse.$x=self′.AbAuthPurse.$x)
→ [simplify]
[43.4] self′.AbAuthPurse ≈ self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))
[Copy term 20.1]
[48.0] ~(0 = (-(+ over (for x::self′.AbAuthPurse.ranb yield x.balance)) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 43.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))]
[48.1] ~(0 = (-(+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).ranb yield x.balance)) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [+ over for..yield of replace]
[48.3] ~(0 = (-(((self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (((self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - self.AbAuthPurse[details.frm].balance)) - self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val))[details.to].balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[48.7] ~(0 = (-((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), []: self.AbAuthPurse[details.to]).balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [explicitly assert falsehood of skipped guards in subsequent guards]
[48.8] ~(0 = (-((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~(details.frm ≈ details.to)]: self.AbAuthPurse[details.to]).balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 39.1, details.frm = details.to is false]
[48.10] ~(0 = (-((-self.AbAuthPurse[details.frm].balance + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + (+ over (for x::self.AbAuthPurse.ranb yield x.balance))) - ([false]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~false]: self.AbAuthPurse[details.to]).balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[48.23] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -(+ over (for x::self′.AbAuthPurse.ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 43.4, self′.AbAuthPurse is equal to self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val))]
[48.24] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -(+ over (for x::self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).replace(details.to → self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).ranb yield x.lost)) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [+ over for..yield of replace]
[48.26] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -(((self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + (((self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))) - self.AbAuthPurse[details.frm].lost)) - self.AbAuthPurse.replace(details.frm → self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val))[details.to].lost) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[48.30] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -((-self.AbAuthPurse[details.frm].lost + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), []: self.AbAuthPurse[details.to]).lost) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [explicitly assert falsehood of skipped guards in subsequent guards]
[48.31] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -((-self.AbAuthPurse[details.frm].lost + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))) - ([details.frm ≈ details.to]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~(details.frm ≈ details.to)]: self.AbAuthPurse[details.to]).lost) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [from term 39.1, details.frm = details.to is false]
[48.33] ~(0 = ((-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance) + -((-self.AbAuthPurse[details.frm].lost + (self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + (self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))) - ([false]: self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val), [~false]: self.AbAuthPurse[details.to]).lost) + (+ over (for x::self.AbAuthPurse.ranb yield x.balance)) + (+ over (for x::self.AbAuthPurse.ranb yield x.lost))))
→ [simplify]
[48.51] ~(0 = (-(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost + self.AbAuthPurse[details.to].lost))
→ [introduce variable 'temp_l_1_0' defined as self.AbAuthPurse[details.to] after {it→it′}!add(details.val)]
[48.52] ~(0 = (-temp_l_1_0.balance + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).balance + -(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost + self.AbAuthPurse[details.to].lost))
→ [introduce variable 'temp_l_1_1' defined as self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)]
[48.53] ~(0 = (-temp_l_1_0.balance + -temp_l_1_1.balance + -(self.AbAuthPurse[details.to] after {it→it′}!add(details.val)).lost + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost + self.AbAuthPurse[details.to].lost))
→ [introduce variable 'temp_l_1_0' defined as self.AbAuthPurse[details.to] after {it→it′}!add(details.val)]
[48.54] ~(0 = (-temp_l_1_0.balance + -temp_l_1_1.balance + -temp_l_1_0.lost + -(self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)).lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost + self.AbAuthPurse[details.to].lost))
→ [introduce variable 'temp_l_1_1' defined as self.AbAuthPurse[details.frm] after {it→it′}!remove(details.val)]
[48.55] ~(0 = (-temp_l_1_0.balance + -temp_l_1_1.balance + -temp_l_1_0.lost + -temp_l_1_1.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost + self.AbAuthPurse[details.to].lost))
→ [from term 69.8, -temp_l_1_0.lost + self.AbAuthPurse[details.to].lost is equal to 0]
[48.56] ~(0 = (0 + -temp_l_1_0.balance + -temp_l_1_1.balance + -temp_l_1_1.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost))
→ [simplify]
[48.58] ~((-temp_l_1_0.balance + -temp_l_1_1.balance + -temp_l_1_1.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost) = 0)
→ [from term 69.9, temp_l_1_0.balance is equal to self.AbAuthPurse[details.to].balance + details.val]
[48.59] ~(0 = (-(self.AbAuthPurse[details.to].balance + details.val) + -temp_l_1_1.balance + -temp_l_1_1.lost + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.to].balance + self.AbAuthPurse[details.frm].lost))
→ [simplify]
[48.63] ~(0 = (-temp_l_1_1.balance + -temp_l_1_1.lost + -details.val + self.AbAuthPurse[details.frm].balance + self.AbAuthPurse[details.frm].lost))
→ [from term 71.9, -temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance is equal to 0]
[48.64] ~(0 = (0 + -temp_l_1_1.lost + self.AbAuthPurse[details.frm].lost))
→ [simplify]
[48.66] ~((-temp_l_1_1.lost + self.AbAuthPurse[details.frm].lost) = 0)
[Retrieve term developed earlier]
[71.9] (0 = (-temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& (0 = (-temp_l_1_1.lost + self.AbAuthPurse[details.frm].lost))
→ [from term 48.66, 0 = (-temp_l_1_1.lost + self.AbAuthPurse[details.frm].lost) is false]
[71.10] (0 = (-temp_l_1_1.balance + -details.val + self.AbAuthPurse[details.frm].balance)) .& false
→ [simplify]
[71.11] false
Proof of sub-goal 3:
[Work on branch 3 from term 2.18]
[72.0] {self→self′}!AbIgnore(details)
[Copy term 72.0]
[73.0] {self→self′}!AbIgnore(details)
→ [expand schema 'AbIgnore']
[73.1] (self′ as from AbWorld) = (self as from AbWorld)
→ [simplify]
[73.2] self = self′
[Copy term 1.4]
[74.0] ~(0 = (-self′.totalAbBalance + -self′.totalAbLost + self.totalAbBalance + self.totalAbLost))
→ [from term 73.2, self′ is equal to self]
[74.2] ~(0 = (-self.totalAbBalance + -self.totalAbLost + self.totalAbBalance + self.totalAbLost))
→ [simplify]
[74.7] false

(Rewriter time: 0.0s, Prover time: 19.5s)

Proof of verification condition: Precondition of 'AbTransferLost' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (96,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (75,13)
To prove: self.Authentic(details.frm)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 2 of conjunction in term 2.9]
[4.0] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 4.0, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferLost' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (96,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (76,13)
To prove: self.Authentic(details.to)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 3 of conjunction in term 2.9]
[5.0] details.to in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.to)
→ [expand function 'Authentic']
[1.1] details.to in self.AbAuthPurse
→ [simplify]
[1.2] details.to in self.AbAuthPurse.dom
→ [from term 5.0, details.to in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferLost' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (96,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (77,25)
To prove: ~(details.frm = details.to)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
→ [separate conjunction and work on first sub-term]
[2.10] ~(details.frm = details.to)
[Take goal term]
[1.0] ~(details.frm = details.to)
→ [from term 2.10, details.frm = details.to is false]
[1.1] ~false
→ [simplify]
[1.2] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferLost' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (96,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (78,13)
To prove: self.SufficientFundsProperty(details)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 4 of conjunction in term 2.9]
[6.0] self.SufficientFundsProperty(details)
[Take goal term]
[1.0] self.SufficientFundsProperty(details)
→ [from term 6.0, self.SufficientFundsProperty(details) is true]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'SufficientFundsProperty' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (95,95)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (65,13)
To prove: self.Authentic(details.frm)
Given: (self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)
Proof:
[Take given term]
[2.0] (self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [expand function 'Authentic']
[2.1] ((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [simplify]
[2.2] ((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [expand function 'Authentic']
[2.3] ((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)
→ [simplify]
[2.7] (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& ~(details.frm = details.to)
[Work on sub-term 2 of conjunction in term 2.7]
[4.0] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 4.0, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferOkay' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (98,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (84,13)
To prove: self.Authentic(details.frm)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 2 of conjunction in term 2.9]
[4.0] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 4.0, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferOkay' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (98,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (85,13)
To prove: self.Authentic(details.to)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 3 of conjunction in term 2.9]
[5.0] details.to in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.to)
→ [expand function 'Authentic']
[1.1] details.to in self.AbAuthPurse
→ [simplify]
[1.2] details.to in self.AbAuthPurse.dom
→ [from term 5.0, details.to in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferOkay' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (98,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (86,25)
To prove: ~(details.frm = details.to)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
→ [separate conjunction and work on first sub-term]
[2.10] ~(details.frm = details.to)
[Take goal term]
[1.0] ~(details.frm = details.to)
→ [from term 2.10, details.frm = details.to is false]
[1.1] ~false
→ [simplify]
[1.2] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'AbTransferOkay' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (98,21)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (87,13)
To prove: self.SufficientFundsProperty(details)
Given: ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
Proof:
[Take given term]
[2.0] ((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.1] (((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.2] (((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [expand function 'Authentic']
[2.3] (((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)
→ [simplify]
[2.9] ~(details.frm = details.to) .& (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& self.SufficientFundsProperty(details)
[Work on sub-term 4 of conjunction in term 2.9]
[6.0] self.SufficientFundsProperty(details)
[Take goal term]
[1.0] self.SufficientFundsProperty(details)
→ [from term 6.0, self.SufficientFundsProperty(details) is true]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'SufficientFundsProperty' satisfied
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (97,95)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (65,13)
To prove: self.Authentic(details.frm)
Given: (self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)
Proof:
[Take given term]
[2.0] (self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [expand function 'Authentic']
[2.1] ((details.frm in self.AbAuthPurse) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [simplify]
[2.2] ((details.frm in self.AbAuthPurse.dom) & self.Authentic(details.to)) & ~(details.frm = details.to)
→ [expand function 'Authentic']
[2.3] ((details.frm in self.AbAuthPurse.dom) & (details.to in self.AbAuthPurse)) & ~(details.frm = details.to)
→ [simplify]
[2.7] (details.frm in self.AbAuthPurse.dom) .& (details.to in self.AbAuthPurse.dom) .& ~(details.frm = details.to)
[Work on sub-term 2 of conjunction in term 2.7]
[4.0] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 4.0, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: At least one guard is true
In the context of class: AbWorld, declared at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (47,1)
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (94,14)
To prove: true .| (((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)) .| (((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details))
Proof:
[Take goal term]
[1.0] true .| (((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details)) .| (((self.Authentic(details.frm) & self.Authentic(details.to)) & ~(details.frm = details.to)) & self.SufficientFundsProperty(details))
→ [simplify]
[1.1] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'SufficientFundsProperty' satisfied
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (78,13)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (65,13)
To prove: self.Authentic(details.frm)
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to)
Proof:
[Take given term]
[2.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[2.1] details.frm in self.AbAuthPurse
→ [simplify]
[2.2] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 2.2, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)

Proof of verification condition: Precondition of 'SufficientFundsProperty' satisfied
Condition generated at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (87,13)
Condition defined at: C:\Program Files\Escher Technologies\Perfect Developer\Examples\Mondex\AbWorld.pd (65,13)
To prove: self.Authentic(details.frm)
Given: self.Authentic(details.frm), self.Authentic(details.to), ~(details.frm = details.to)
Proof:
[Take given term]
[2.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[2.1] details.frm in self.AbAuthPurse
→ [simplify]
[2.2] details.frm in self.AbAuthPurse.dom
[Take goal term]
[1.0] self.Authentic(details.frm)
→ [expand function 'Authentic']
[1.1] details.frm in self.AbAuthPurse
→ [simplify]
[1.2] details.frm in self.AbAuthPurse.dom
→ [from term 2.2, details.frm in self.AbAuthPurse.dom is true]
[1.3] true
(Rewriter time: 0.0s, Prover time: 0.0s)