-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbankAccount_M1_accountCreation.bpo
117 lines (117 loc) · 22.4 KB
/
bankAccount_M1_accountCreation.bpo
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="ACCOUNT" org.eventb.core.type="ℙ(ACCOUNT)"/>
<org.eventb.core.poIdentifier name="CLIENT" org.eventb.core.type="ℙ(CLIENT)"/>
<org.eventb.core.poIdentifier name="K" org.eventb.core.type="ℤ"/>
<org.eventb.core.poPredicate name="ACCOUNU" org.eventb.core.predicate="finite(ACCOUNT)" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#)"/>
<org.eventb.core.poPredicate name="ACCOUNV" org.eventb.core.predicate="finite(CLIENT)" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#*"/>
<org.eventb.core.poPredicate name="ACCOUNW" org.eventb.core.predicate="K∈ℕ" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="balance" org.eventb.core.type="ℙ(ACCOUNT×ℤ)"/>
<org.eventb.core.poIdentifier name="owner" org.eventb.core.type="ℙ(ACCOUNT×CLIENT)"/>
<org.eventb.core.poPredicate name="balancf" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.invariant#)"/>
<org.eventb.core.poPredicate name="balancg" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.invariant#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/invBalance/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C5"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(ACCOUNT×ℤ))∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#INITIALISATION\/invBalance\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/invOwner/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C5"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(ACCOUNT×CLIENT))∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#INITIALISATION\/invOwner\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTbankAccount_C5" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="owner'" org.eventb.core.type="ℙ(ACCOUNT×CLIENT)"/>
<org.eventb.core.poIdentifier name="balance'" org.eventb.core.type="ℙ(ACCOUNT×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPbankAccount_C5" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTIDENTbankAccount_C5" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="accountCreation/invBalance/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C6"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balance∪{a ↦ 0}∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#accountCreation\/invBalance\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="accountCreation/invOwner/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C6"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="owner∪{a ↦ c}∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#accountCreation\/invOwner\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="accountCreation/setNewAccountOwnership/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C6"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="owner∪{a ↦ c}∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#.|org.eventb.core.action#act1"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#.|org.eventb.core.action#act1"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#accountCreation\/setNewAccountOwnership\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="accountCreation/setNewAccountBalance/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C6"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balance∪{a ↦ 0}∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#.|org.eventb.core.action#act2"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#.|org.eventb.core.action#act2"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#accountCreation\/setNewAccountBalance\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTbankAccount_C6" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
<org.eventb.core.poIdentifier name="owner'" org.eventb.core.type="ℙ(ACCOUNT×CLIENT)"/>
<org.eventb.core.poIdentifier name="c" org.eventb.core.type="CLIENT"/>
<org.eventb.core.poIdentifier name="balance'" org.eventb.core.type="ℙ(ACCOUNT×ℤ)"/>
<org.eventb.core.poIdentifier name="a" org.eventb.core.type="ACCOUNT"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPbankAccount_C6" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTIDENTbankAccount_C6" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="c∈CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*|org.eventb.core.guard#("/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="a∈ACCOUNT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*|org.eventb.core.guard#,"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="a∉dom(owner)" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*|org.eventb.core.guard#-"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="a∉dom(balance)" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#*|org.eventb.core.guard#."/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="operate/invBalance/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C7">
<org.eventb.core.poPredicate name="'" org.eventb.core.predicate="balance'∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#\/|org.eventb.core.action#act5"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balance'∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#\/"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#operate\/invBalance\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="operate/invOwner/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTALLHYPbankAccount_C7">
<org.eventb.core.poPredicate name="'" org.eventb.core.predicate="owner'∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#\/|org.eventb.core.action#act3"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="owner'∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.event#."/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.event#\/"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poSequent#operate\/invOwner\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTbankAccount_C7" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
<org.eventb.core.poIdentifier name="owner'" org.eventb.core.type="ℙ(ACCOUNT×CLIENT)"/>
<org.eventb.core.poIdentifier name="balance'" org.eventb.core.type="ℙ(ACCOUNT×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPbankAccount_C7" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#EVTIDENTbankAccount_C7" org.eventb.core.poStamp="3"/>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BankAccount/bankAccount_M1_accountCreation.bpo|org.eventb.core.poFile#bankAccount_M1_accountCreation|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#."/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>