1case \x of 0 -> 1 -> _ ->  ---> if \x = 0
2 then ->1 else if \x = 1 then ->2 else ->3
3
4case \x of nodeCap@(CNodeCap {}) -> _ ->  ---> let nodeCap = \x in
5 if isCNodeCap nodeCap
6 then ->1 else ->2
7
8case \x of root@(CNodeCap {}) -> _ ->  ---> let root = \x in
9 if isCNodeCap root
10 then ->1 else ->2
11
12case \x of rt@(CNodeCap {}) -> _ ->  ---> let rt = \x in
13 if isCNodeCap rt
14 then ->1 else ->2
15
16case \x of cap@(EndpointCap { capEPCanSend = True }) -> cap@(NotificationCap { capNtfnCanSend = True }) -> cap ->  ---> let cap = \x in
17 if isEndpointCap cap \<and> capEPCanSend cap
18 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
19 then ->2 else ->3
20
21case \x of EndpointCap { \v0\EPCanReceive = True } -> NotificationCap { \v0\NtfnCanReceive = True } -> _ ->  ---> let \v0\ = \x in
22 if isEndpointCap \v0\ \<and> \v0\EPCanReceive \v0
23 then ->1 else if isNotificationCap \v0\ \<and> \v0\NtfnCanReceive \v0
24 then ->2 else ->3
25
26case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) ->  ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \<and> capTCBCanWrite cap
27 then ->1 else if isCNodeCap cap
28 then ->2 else if isUntypedCap cap
29 then ->3 else if isArchObjectCap cap
30 then ->4 else if blocking
31 then ->5 else ->6
32
33case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=True}) -> (_, _) ->  ---> let (\v0\, cap) = \x in
34 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0;
35 bits = \v0\ !! 1;
36 args = drop 2 \v0
37 in ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap then ->2 else ->3
38
39case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) ->  ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \<and> capTCBCanWrite cap
40 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
41 then ->2 else if isUntypedCap cap
42 then ->3 else if isArchObjectCap cap
43 then ->4 else if blocking
44 then let ptr = capIndex in ->5 else ->6
45
46case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (capIndex, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) ->  ---> let (capPtr, cap) = \x; capIndex = capPtr in
47 if isThreadCap cap \<and> capTCBCanWrite cap
48 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
49 then ->2 else if isUntypedCap cap
50 then ->3 else if isArchObjectCap cap
51 then ->4 else ->5
52
53case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) ->  ---> let (capPtr, cap) = \x; capIndex = capPtr in
54 if isThreadCap cap \<and> capTCBCanWrite cap
55 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
56 then ->2 else if isUntypedCap cap
57 then ->3 else if isArchObjectCap cap
58 then ->4 else ->5
59
60case \x of Just (slot, 0, rights) -> _ ->  ---> case \x of
61 Some \v0\ \<Rightarrow> let (slot, \v1\, rights) = \v0\ in
62 if \v1\ = 0 then ->1 else ->2 | None \<Rightarrow> ->2
63
64case \x of (slot, 0, rights) -> (_, bitsLeft, _) ->  ---> let (slot, bitsLeft, rights) = \x in
65 if bitsLeft = 0
66 then ->1 else ->2
67
68case \x of (index:bits:args, cnode@(CNodeCap {})) -> (_, _) ->  ---> let (L, cnode) = \x in
69 if isCNodeCap cnode \<and> length L > 1 then
70 let index = L !! 0;
71 bits = L !! 1;
72 args = drop 2 L
73 in ->1 else ->2
74
75case \x of (index:bits:args, cnode@(CNodeCap { capCNodeCanModify = True })) -> (_, CNodeCap { capCNodeCanModify = True }) -> (_, _) ->  ---> let (L, cnode) = \x in
76 if isCNodeCap cnode \<and> capCNodeCanModify cnode then
77 if length L > 1 then
78 let index = L !! 0;
79 bits = L !! 1;
80 args = drop 2 L
81 in ->1 else ->2 else ->3
82
83case \x of (YieldToCall, _, thread) -> (call@(ThreadControlCall {}), faultep:replyep:priority:cRoot:cRootData:vRoot:vRootData:buffer:_, target) -> (call@(ExchangeRegistersCall {}), src:save:_, dest) -> (_, _, _) ->  ---> let (call, L, \v0\) = \x in
84 if isYieldToCall call
85 then let thread = \v0\ in ->1 else if isThreadControlCall call \<and> length L > 6
86 then let target = \v0\;
87 faultep = L !! 0;
88 replyep = L !! 1;
89 priority = L !! 2;
90 cRoot = L !! 3;
91 cRootData = L !! 4;
92 vRoot = L !! 5;
93 vRootData = L !! 6;
94 buffer = L !! 7
95 in ->2 else if isExchangeRegistersCall call \<and> length L > 1
96 then let dest = \v0\;
97 src = L !! 0;
98 save = L !! 1
99 in ->3 else ->4
100
101case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> (_,_) ->  ---> let (call, \v0\) = \x in
102 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0
103 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0
104 then ->2 else ->3
105
106case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> _ ->  ---> let (call, \v0\) = \x in
107 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0
108 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0
109 then ->2 else ->3
110
111case \x of untypedCap@(UntypedCap {}) -> _ ->  ---> let untypedCap = \x in
112 if isUntypedCap untypedCap
113 then ->1
114 else ->1
115
116case \x of ex2@(UserHandledFault {}) -> ex2 ->  ---> let ex2 = \x in
117 if isUserHandledFault ex2
118 then ->1 else ->2
119
120case \x of 0 -> size ->  ---> let size = \x in if size = 0
121 then ->1 else ->2
122
123case \x of 0 -> ctePtr ->  ---> let ctePtr = \x in if ctePtr = 0
124 then ->1 else ->2
125
126case \x of (first:rest,_) -> ([], 0) -> ([], _) ->  ---> let \v0\ = \x in case fst \v0\ of
127 first#rest \<Rightarrow> ->1 | [] \<Rightarrow> if snd \v0\ = 0
128 then ->2 else ->3
129
130case \x of Just x@(CNodeData {}) -> _ ->  ---> let \v0\ = \x in
131 if \v0\ \<noteq> None \<and> isCNodeData (the \v0\)
132 then let x = the \v0\ in ->1 else ->2
133
134case \x of (Just new, EndpointData 0) -> (Just _, EndpointData _) -> (Just new, AsyncEndpointData 0) -> (Just _, AsyncEndpointData _) -> (Nothing, old@(CNodeData {})) -> (Just new, old@(CNodeData {})) -> (_, old) ->  ---> let (\v0\, old) = \x; new = the \v0\; \v1\ = (\v0\ \<noteq> None) in
135 if \v1\ \<and> old = EndpointData 0
136 then ->1 else if \v1\ \<and> isEndpointData old
137 then ->2 else if \v1\ \<and> old = AsyncEndpointData 0
138 then ->3 else if \v1\ \<and> isAsyncEndpointData old
139 then ->4 else if (\<not> \v1\) \<and> isCNodeData old
140 then ->5 else if \v1\ \<and> isCNodeData old
141 then ->6 else ->7
142
143case \x of 0 -> slot ->  ---> let slot = \x in
144 if slot = 0 then ->1 else ->2
145
146case \x of CTE { cteCap = UntypedCap {} } -> cte@(CTE { cteMDBNode = mdb }) ->  ---> let cte = \x in
147 if isUntypedCap (cteCap cte)
148 then ->1 else let mdb = cteMDBNode cte
149 in ->2
150
151case \x of cap@(EndpointCap {}) -> _ ->  ---> let cap = \x in
152 if isEndpointCap cap
153 then ->1 else ->2
154
155case \x of (a@UntypedCap {}, b@UntypedCap {}) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) ->  ---> let (a, b) = \x in
156 if isUntypedCap a \<and> isUntypedCap b
157 then ->1 else if isEndpointCap a \<and> isEndpointCap b
158 then ->2 else if isNotificationCap a \<and> isNotificationCap b
159 then ->3 else if isCNodeCap a \<and> isCNodeCap b
160 then ->4 else if isThreadCap a \<and> isThreadCap b
161 then ->5 else if isFrameCap a \<and> isFrameCap b
162 then ->6 else if isArchObjectCap a \<and> isArchObjectCap b
163 then let a = capCap a; b = capCap b in ->7 else ->8
164
165case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> cap@(ArchObjectCap {}) -> _ ->  ---> let cap = \x in
166 if isEndpointCap cap \<and> capEPCanSend cap
167 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
168 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap
169 then ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap
170 then ->4 else if isUntypedCap cap
171 then ->5 else if isArchObjectCap cap
172 then ->6 else ->7
173
174case \x of 0 -> 1 -> 2 -> _ ->  ---> let \v0\ = \x in
175 if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else ->4
176
177case \x of (CTE a@(UntypedCap {}) _, CTE b _) -> (CTE a mdbA, CTE b mdbB) ->  ---> let (\v0\, \v1\) = \x in
178 case \v0\ of CTE a mdbA \<Rightarrow> (
179 case \v1\ of CTE b mdbB \<Rightarrow> (
180 if isUntypedCap a
181 then ->1 else ->2 ))
182
183case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> (NotificationCap {}) -> _ ->  ---> let \v0\ = \x in
184 if isEndpointCap \v0\ \<and> capEPBadge \v0\ = 0
185 then ->1 else if isNotificationCap \v0\ \<and> capNtfnBadge \v0\ = 0
186 then ->2 else if isEndpointCap \v0
187 then ->3 else if isNotificationCap \v0
188 then ->4 else ->5
189
190case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, True) -> (ThreadCap { capTCBPtr = tcb }, True, True) -> (CNodeCap { capCNodePtr = cn }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, False) -> (ThreadCap { capTCBPtr = tcb }, True, False) -> (Zombie { zombieObject = Right tcb }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, True) -> (Zombie { zombieObject = Left (_, 0) }, True, _) -> (Zombie { zombieObject = Right tcb }, True, True) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
191 if isEndpointCap \v0\ \<and> \v1
192 then let ptr = capEPPtr \v0
193 in ->1 else if isNotificationCap \v0\ \<and> \v1
194 then let ptr = capNtfnPtr \v0
195 in ->2 else if isCNodeCap \v0\ \<and> \v1\ \<and> \v2
196 then let cap = \v0
197 in ->3 else if isThreadCap \v0\ \<and> \v1\ \<and> \v2
198 then let tcb = capTCBPtr \v0
199 in ->4 else if isCNodeCap \v0\ \<and> \v1\ \<and> (\<not> \v2\)
200 then let cn = capCNodePtr \v0
201 in ->5 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1))
202 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1
203 in ->6 else if isThreadCap \v0\ \<and> \v1\ \<and> (\<not> \v2\)
204 then let tcb = capTCBPtr \v0
205 in ->7 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> isRight (zombieObject \v0\)
206 then let tcb = theRight (zombieObject \v0\)
207 in ->8 else if isZombie \v0\ \<and> \v2\ \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1))
208 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1
209 in ->9 else if isZombie \v0\ \<and> \v1\ \<and> (\<exists>\v3\. zombieObject \v0\ = Left (\v3\, 0))
210 then ->10 else if isZombie \v0\ \<and> isRight (zombieObject \v0\) \<and> \v1\ \<and> \v2
211 then let tcb = theRight (zombieObject \v0\)
212 in ->11 else if isArchObjectCap \v0
213 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
214 in ->12 else if isFrameCap \v0
215 then ->13 else if isNullCap \v0
216 then ->14 else if isZombie \v0\ \<and> (\<not> \v1\)
217 then ->15 else ->16
218
219case \x of (new, cap@(EndpointCap {})) -> (new, cap@(NotificationCap {})) -> (w, cap@(CNodeCap {})) -> (w, ArchObjectCap { capCap = aoCap }) -> (_, cap) ->  ---> let (new, cap) = \x;
220     w = new in
221 if isEndpointCap cap
222 then ->1 else if isNotificationCap cap
223 then ->2 else if isCNodeCap cap
224 then ->3 else if isArchObjectCap cap
225 then let aoCap = capCap cap
226 in ->4 else ->5
227
228case \x of cap@(EndpointCap { capEPCanSend = True }) -> _ ->  ---> let cap = \x in
229 if isEndpointCap cap \<and> capEPCanSend cap
230 then ->1 else ->2
231
232case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
233 if isEndpointCap \v0\ \<and> \v1
234 then let ptr = capEPPtr \v0
235 in ->1 else if isNotificationCap \v0\ \<and> \v1
236 then let ptr = capNtfnPtr \v0
237 in ->2 else if isCNodeCap \v0\ \<and> \v1
238 then let cap = \v0\; exposed = \v2
239 in ->3 else if isThreadCap \v0\ \<and> \v1
240 then let tcb = capTCBPtr \v0\; exposed = \v2
241 in ->4 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
242 then let ptr = capCTEPtr \v0\;
243 n = capNumber \v0\ - 1
244 in ->5 else if isZombie \v0\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
245 then let ptr = capCTEPtr \v0\;
246 n = capNumber \v0\ - 1
247 in ->6 else if isZombie \v0\ \<and> capNumber \v0\ = 0
248 then ->7 else if isArchObjectCap \v0
249 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
250 in ->8 else if isFrameCap \v0
251 then ->9 else if isNullCap \v0
252 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
253 then ->11 else ->12
254
255case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=False}) -> (_, _) ->  ---> let (\v0\, cap) = \x in
256 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0;
257 bits = \v0\ !! 1;
258 args = drop 2 \v0
259 in ->1 else if isCNodeCap cap \<and> (\<not> capCNodeCanModify cap) then ->2 else ->3
260
261case \x of 32 -> 64 -> _ ->  ---> if \x = 32
262 then ->1 else if \x = 64
263 then ->2 else ->3
264
265case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@(FrameCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) ->  ---> let c = \x in
266 if isNullCap c
267 then ->1 else if isUntypedCap c
268 then ->2 else if isEndpointCap c
269 then ->3 else if isNotificationCap c
270 then ->4 else if isCNodeCap c
271 then ->5 else if isThreadCap c
272 then ->6 else if isFrameCap c
273 then ->7 else if isArchObjectCap c
274 then let aoCap = capCap c
275 in ->8 else (* assuming Zombie *) ->9
276
277case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) ->  ---> let (src, new) = \x in
278 if (isEndpointCap src \<and> isEndpointCap new)
279 then ->1 else if (isNotificationCap src \<and> isNotificationCap new)
280 then ->2 else ->3
281
282case \x of c2@(Zombie { capCTEPtr = ptr2 }) -> _ ->  ---> let c2 = \x;
283 ptr2 = capCTEPtr c2 in
284 if isZombie c2
285 then ->1 else ->2
286
287case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
288 if isEndpointCap \v0\ \<and> \v1
289 then let ptr = capEPPtr \v0
290 in ->1 else if isNotificationCap \v0\ \<and> \v1
291 then let ptr = capNtfnPtr \v0
292 in ->2 else if isCNodeCap \v0\ \<and> \v1
293 then let cap = \v0\; exposed = \v2
294 in ->3 else if isThreadCap \v0\ \<and> \v1
295 then let tcb = capTCBPtr \v0\; exposed = \v2
296 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
297 then let ptr = capCTEPtr \v0\;
298 n = capNumber \v0\ - 1
299 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
300 then let ptr = capCTEPtr \v0\;
301 n = capNumber \v0\ - 1;
302 c = \v0
303 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
304 then ->7 else if isArchObjectCap \v0
305 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
306 in ->8 else if isFrameCap \v0
307 then ->9 else if isNullCap \v0
308 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
309 then ->11 else ->12
310
311case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) ->  ---> let (src,new) = \x in
312 if isEndpointCap src & isEndpointCap new
313 then ->1
314 else if isNotificationCap src & isNotificationCap new
315 then ->2
316 else ->3
317
318case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> NotificationCap {} -> _ ->  ---> if isEndpointCap \x \<and> capEPBadge \x = 0
319 then ->1 else if isNotificationCap \x \<and> capNtfnBadge \x = 0
320 then ->2 else if isEndpointCap \x then ->3 else if isNotificationCap \x
321 then ->4 else ->5
322
323case \x of (_, cap@(EndpointCap {capEPCanSend=True})) -> (_, cap@(NotificationCap {capNtfnCanSend=True})) -> (sl, cap@(ThreadCap {capTCBCanWrite=True})) -> (_, cap@(CNodeCap {capCNodeCanModify=True})) -> (slot, cap@(UntypedCap {})) -> (slot, cap@(ArchObjectCap {})) -> (_, _) ->  ---> let (slot, cap) = \x in
324 if isEndpointCap cap \<and> capEPCanSend cap
325 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
326 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap
327 then let sl = slot
328 in ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap
329 then ->4 else if isUntypedCap cap
330 then ->5 else if isArchObjectCap cap
331 then ->6 else ->7
332
333case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ ->  ---> if isEndpointCap \x & capEPBadge \x = 0
334 then ->1
335 else if isNotificationCap \x & capNtfnBadge \x = 0
336 then ->2
337 else if isEndpointCap \x
338 then let badge = capEPBadge \x in
339 ->3
340 else if isNotificationCap \x
341 then let badge = capNtfnBadge \x in
342 ->4
343 else ->5
344
345case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) ->  ---> let (a,b) = \x in
346 if b = NullCap
347 then ->1
348 else if isUntypedCap a
349 then ->2
350 else if isEndpointCap a & isEndpointCap b
351 then ->3
352 else if isNotificationCap a & isNotificationCap b
353 then ->4
354 else if isCNodeCap a & isCNodeCap b
355 then ->5
356 else if isThreadCap a & isThreadCap b
357 then ->6
358 else if isFrameCap a & isFrameCap b
359 then ->7
360 else if isArchObjectCap a & isArchObjectCap b
361 then let a = capCap a; b = capCap b in
362 ->8
363 else ->9
364
365case \x of EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ ->  ---> if isEndpointCap \x & capEPBadge \x ~= 0
366 then let badge = capEPBadge \x in
367 ->1
368 else if isNotificationCap \x & capNtfnBadge \x ~= 0
369 then let badge = capNtfnBadge \x in
370 ->2
371 else ->3
372
373case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
374 if isEndpointCap \v0\ \<and> \v1
375 then let ptr = capEPPtr \v0
376 in ->1 else if isNotificationCap \v0\ \<and> \v1
377 then let ptr = capNtfnPtr \v0
378 in ->2 else if isCNodeCap \v0\ \<and> \v1
379 then let cap = \v0\; exposed = \v2
380 in ->3 else if isThreadCap \v0\ \<and> \v1
381 then let tcb = capTCBPtr \v0\; exposed = \v2
382 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
383 then let ptr = capCTEPtr \v0\;
384 n = capNumber \v0\ - 1
385 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
386 then let z = \v0\;
387 ptr = capCTEPtr \v0\;
388 n = capNumber \v0\ - 1;
389 c = \v0
390 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
391 then ->7 else if isArchObjectCap \v0
392 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
393 in ->8 else if isFrameCap \v0
394 then ->9 else if isNullCap \v0
395 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
396 then ->11 else ->12
397
398case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 6 -> (_, _) | label > 6 -> _ ->  ---> let (\v0\, \v1\) = \x
399 in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 6 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->4 else if label > 6 then ->5 else ->6
400
401case \x of Zombie {} -> cap@(UntypedCap {}) -> ArchObjectCap cap -> cap ->  ---> let cap = \x
402 in case cap of Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1 | UntypedCap \v0\ \v1\ \<Rightarrow> ->2 | ArchObjectCap cap \<Rightarrow> ->3 | _ \<Rightarrow> ->4
403
404case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> _ ->  ---> let \v0\ = \x
405 in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else ->9
406
407case \x of MI { msgExtraCaps = 0 } -> MI { msgExtraCaps = count } ->  ---> let \v0\ = \x
408 in if msgExtraCaps \v0\ = 0 then ->1 else let count = msgExtraCaps \v0\ in ->2
409
410case \x of c@PageTableCap { capPTMappedAddress = Just _ } -> PageTableCap { capPTMappedAddress = Nothing } -> c@PageDirectoryCap { capPDMappedASID = Just _ } -> PageDirectoryCap { capPDMappedASID = Nothing } -> c@PageCap {} -> c@ASIDControlCap -> c@ASIDPoolCap {} ->  ---> let c = \x
411 in case c of
412 PageTableCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->2 else ->1
413 | PageDirectoryCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->4 else ->3
414 | PageCap \v0\ \v1\ \v2\ \v3\ \<Rightarrow> ->5
415 | ASIDControlCap \<Rightarrow> ->6
416 | ASIDPoolCap \v0\ \v1\ \<Rightarrow> ->7
417
418case \x of c@(PageCap {}) -> c ->  ---> let c = \x in
419 if isPageCap c
420 then ->1
421 else ->2
422
423case \x of (a@PageCap {}, b@PageCap {}) -> (a@PageTableCap {}, b@PageTableCap {}) -> (a@PageDirectoryCap {}, b@PageDirectoryCap {}) -> (ASIDControlCap, ASIDControlCap) -> (a@ASIDPoolCap {}, b@ASIDPoolCap {}) -> (_, _) ->  ---> let (a, b) = \x in
424 if (isPageCap a & isPageCap b) then ->1 else if (isPageTableCap a & isPageTableCap b) then ->2 else if (isPageDirectoryCap a & isPageDirectoryCap b) then ->3 else if (isASIDControlCap a & isASIDControlCap b) then ->4 else if (isASIDPoolCap a & isASIDPoolCap b) then ->5 else ->6
425
426case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject ->  ---> case \x of
427 Arch.Types.APIObjectType \v0\ \<Rightarrow> ->1 | Arch.Types.SmallPageObject \<Rightarrow> ->2 | Arch.Types.LargePageObject \<Rightarrow> ->3 | Arch.Types.SectionObject \<Rightarrow> ->4 | Arch.Types.SuperSectionObject \<Rightarrow> ->5 | Arch.Types.PageTableObject \<Rightarrow> ->6 | Arch.Types.PageDirectoryObject \<Rightarrow> ->7
428
429case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 7 -> (_, _) | label > 7 -> _ ->  ---> let (\v0\, \v1\) = \x
430 in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if label = 6 then ->4 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 7 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->5 else if label > 7 then ->6 else ->7
431
432case \x of IdleEP | blocking -> SendEP queue | blocking -> IdleEP -> SendEP _ -> RecvEP (dest:queue) -> RecvEP [] ->  ---> case \x of
433 IdleEP \<Rightarrow> if blocking then ->1 else ->3 | SendEP queue \<Rightarrow> if blocking then ->2 else ->4 | RecvEP \v0\ \<Rightarrow> (case \v0\ of dest # queue \<Rightarrow> ->5 | [] \<Rightarrow> ->6 )
434
435case \x of Zombie {} -> cap@(UntypedCap {}) -> ReplyCap {} -> ArchObjectCap cap -> cap ->  --->     let cap = \x
436      in case cap of
437         Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1
438         | UntypedCap \v0\ \v1\ \<Rightarrow> ->2
439         | ReplyCap \v0\ \v1\ \<Rightarrow> ->3
440         | ArchObjectCap cap \<Rightarrow> ->4
441         | _ \<Rightarrow> ->5
442
443case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (IRQHandlerCap { capIRQ = irq }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) ->  --->     let (\v0\, \v1\, \v2\) = \x in
444     if isEndpointCap \v0\ \<and> \v1\
445     then let ptr = capEPPtr \v0
446 in ->1
447     else if isNotificationCap \v0\ \<and> \v1\
448     then let ptr = capNtfnPtr \v0
449 in ->2
450     else if isCNodeCap \v0\ \<and> \v1\
451     then let cap = \v0\; exposed = \v2\ in ->3
452     else if isThreadCap \v0\ \<and> \v1\
453     then let tcb = capTCBPtr \v0\; exposed = \v2\ in ->4
454     else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
455     then let ptr = capCTEPtr \v0\;
456              n = capNumber \v0\ - 1
457          in ->5
458     else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
459     then let z = \v0\;
460              ptr = capCTEPtr \v0\;
461              n = capNumber \v0\ - 1;
462              c = \v0\
463          in ->6
464     else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
465     then ->7
466     else if isIRQHandlerCap \v0\ \<and> \v1\
467     then let irq = capIRQ \v0\ in ->8
468     else if isArchObjectCap \v0\
469     then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->9
470     else if isNullCap \v0\
471     then ->10
472     else if isZombie \v0\ \<and> (\<not> \v1\)
473     then ->11
474     else ->12
475
476case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (IRQControlCap, IRQControlCap) -> (IRQHandlerCap a, IRQHandlerCap b) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) ->  --->let (a,b) = \x in
477    if b = NullCap
478    then ->1
479    else if isUntypedCap a
480    then ->2
481    else if isEndpointCap a & isEndpointCap b
482    then ->3
483    else if isNotificationCap a & isNotificationCap b
484    then ->4
485    else if isCNodeCap a & isCNodeCap b
486    then ->5
487    else if isThreadCap a & isThreadCap b
488    then ->6
489    else if a = IRQControlCap & b = IRQControlCap
490    then ->7
491    else if isIRQHandlerCap a & isIRQHandlerCap b
492    then let a = capIRQ a; b = capIRQ b in ->8
493    else if isArchObjectCap a & isArchObjectCap b
494    then let a = capCap a; b = capCap b in
495          ->9
496    else ->10
497
498case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, ArchObjectCap { capCap = aoCap }) -> (_, _, cap) ->  --->let (\v0\, \v1\, \v2\ ) = \x in
499    if isEndpointCap \v2\
500    then let preserve = \v0\; new = \v1\; cap = \v2\ in ->1
501    else if isNotificationCap \v2\
502    then let preserve = \v0\; new = \v1\; cap = \v2\ in ->2
503    else if isCNodeCap \v2\
504    then let w = \v1\; cap = \v2\ in ->3
505    else if isArchObjectCap \v2\
506    then let p = \v0\; w = \v1\; aoCap = capCap \v2\ in ->4
507    else let cap = \v2\ in ->5
508
509case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) ->  --->let c = \x in
510    if isNullCap c then ->1
511    else if isUntypedCap c then ->2
512    else if isEndpointCap c then ->3
513    else if isNotificationCap c then ->4
514    else if isReplyCap c then ->5
515    else if isCNodeCap c then ->6
516    else if isThreadCap c then ->7
517    else if isIRQControlCap c then ->8
518    else if isIRQHandlerCap c then ->9
519    else if isArchObjectCap c then let aoCap = capCap c in ->10
520    else (* assuming Zombie *) ->11
521
522case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> 8 -> 9 -> _ ->  --->let \v0\ = \x
523 in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else if \v0\ = 8 then ->9 else if \v0\ = 9 then ->10 else ->11
524
525case \x of ArchObjectCap (pageCap@PageCap {}) -> _ ->  ---> let \v0\ = \x in
526    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
527    then
528        let pageCap = capCap \v0\
529        in ->1
530    else ->2
531
532case \x of ArchObjectCap (frameCap@PageCap {}) -> _ ->  ---> let \v0\ = \x in
533    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
534    then
535        let frameCap = capCap \v0\
536        in ->1
537    else ->2
538
539case \x of ((Zombie { capCTEPtr = ptr, capNumber = n+1 }), False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
540     if isZombie \v0\ \<and> (\<not> \v1\) \<and> capNumber \v0\ \<noteq> 0
541     then let ptr = capCTEPtr \v0\;
542              n = capNumber \v0\ - 1
543          in ->1
544     else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ \<noteq> 0
545     then let z = \v0\;
546              ptr = capCTEPtr \v0\;
547              n = capNumber \v0\ - 1
548          in ->2
549     else ->3
550
551case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) ->  ---> let c = \x in
552    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
553    then ->1
554    else if isPageTableCap c \<and> capPTMappedAddress c = None
555    then ->2
556    else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None
557    then ->3
558    else if isPageDirectoryCap c \<and> capPDMappedASID c = None
559    then ->4
560    else if isPageCap c
561    then ->5
562    else if isASIDControlCap c
563    then ->6
564    else if isASIDPoolCap c
565    then ->7
566    else undefined
567
568case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) ->  ---> let (a, b) = \x in
569    if isPageCap a \<and> isPageCap b
570    then ->1
571    else if isPageTableCap a \<and> isPageTableCap b
572    then ->2
573    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
574    then ->3
575    else if isASIDControlCap a \<and> isASIDControlCap b
576    then ->4
577    else if isASIDPoolCap a \<and> isASIDPoolCap b
578    then ->5
579    else ->6
580
581case \x of ArchObjectCap (frame@PageCap {}) -> _ ->  ---> let \v0\ = \x in
582    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
583    then let frame = capCap \v0\
584         in ->1
585    else ->2
586
587case \x of ArchObjectCap (PageDirectoryCap { capPDMappedASID = Just _, capPDBasePtr = cur_pd }) | cur_pd == pd -> _ ->  ---> let \v0\ = \x in
588    if isArchObjectCap \v0\ \<and> isPageDirectoryCap (capCap \v0\) \<and> capPDMappedASID (capCap \v0\) \<noteq> None \<and> capPDBasePtr (capCap \v0\) = pd
589    then let cur_pd = pd in ->1
590    else ->2
591
592case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
593    if \v0\ = 0 then
594        if length \v1\ > 1 \<and> length \v2\ > 0
595        then let vaddr = \v1\ !! 0;
596            attr = \v1\ !! 1;
597            pdCap = fst (\v2\ !! 0)
598        in ->1
599        else ->2
600    else ->3
601
602case \x of (0, vaddr:rightsMask:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, rightsMask:attr:_, _) -> (1, _, _) -> (2, _, _) -> (3, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
603    if \v0\ = 0 then
604        if length \v1\ > 2 \<and> length \v2\ > 0
605        then let vaddr = \v1\ !! 0;
606            rightsMask = \v1\ !! 1;
607            attr = \v1\ !! 2;
608            pdCap = fst (\v2\ !! 0)
609        in ->1
610        else ->2
611    else if \v0\ = 1 then
612        if length \v1\ > 1
613        then let rightsMask = \v1\ !! 0;
614            attr = \v1\ !! 1
615        in ->3
616        else ->4
617    else if \v0\ = 2
618    then ->5
619    else if \v0\ = 3
620    then ->6
621    else ->7
622
623case \x of (0, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (0, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
624    if \v0\ = 0 then
625        if length \v1\ > 1 \<and> length \v2\ > 1
626        then let index = \v1\ !! 0;
627            depth = \v1\ !! 1;
628            (untyped, parentSlot) = \v2\ !! 0;
629            croot = fst (\v2\ !! 1)
630        in ->1
631        else ->2
632    else ->3
633
634case \x of (0, (pdCap,pdCapSlot):_) -> (0, _) -> _ ->  ---> let (\v0\, \v1\) = \x in
635    if \v0\ = 0 then
636        if length \v1\ > 0
637        then let (pdCap, pdCapSlot) = \v1\ !! 0
638        in ->1
639        else ->2
640    else ->3
641
642case \x of (PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
643    if isPageDirectoryCap cap
644    then ->1
645    else if isPageTableCap cap
646    then ->2
647    else if isPageCap cap
648    then ->3
649    else if isASIDControlCap cap
650    then ->4
651    else if isASIDPoolCap cap
652    then ->5
653    else undefined
654
655case \x of ((index:bits:args), cap@(CNodeCap {capCNodeCanModify=True})) -> (_, (CNodeCap {capCNodeCanModify=True})) -> (_, _) ->  ---> let (\v0\, cap) = \x in
656    if isCNodeCap cap \<and> capCNodeCanModify cap
657    then
658        (case \v0\ of
659            (index # bits # args) \<Rightarrow> ->1
660          | _ \<Rightarrow> ->2
661    )
662    else ->3
663
664case \x of ((src@EndpointCap {}), (new@EndpointCap {})) -> ((src@NotificationCap {}), (new@NotificationCap {})) -> (_, _) ->  ---> let (src, new) = \x in
665    if isEndpointCap src \<and> isEndpointCap new
666    then ->1
667    else if isNotificationCap src \<and> isNotificationCap new
668    then ->2
669    else ->3
670
671case \x of (CTE { cteCap = UntypedCap {} }) -> cte@(CTE { cteMDBNode = mdb }) ->  ---> let \v0\ = \x in
672    if isUntypedCap (cteCap \v0\)
673    then ->1
674    else let cte = \v0\;
675        mdb = cteMDBNode cte
676    in ->2
677
678case \x of 0 | length msg >= length syscallMessage -> _ ->  ---> if \x = 0 \<and> length msg \<ge> length syscallMessage
679    then ->1
680    else ->2
681
682case \x of 0 | length msg >= length exceptionMessage -> _ ->  ---> if \x = 0 \<and> length msg \<ge> length exceptionMessage
683    then ->1
684    else ->2
685
686case \x of (0,irqW:index:depth:_,cnode:_) -> (0,_,_) -> (1,_,_) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
687    if \v0\ = 0 then
688        if length \v1\ > 2 \<and> length \v2\ > 0
689        then let irqW = \v1\ !! 0;
690            index = \v1\ !! 1;
691            depth = \v1\ !! 2;
692            cnode = \v2\ !! 0
693        in ->1
694        else ->2
695    else if \v0\ = 1
696    then ->3
697    else ->4
698
699case \x of (0,_) -> (1,(cap,slot):_) -> (1,_) -> (2,_) -> _ ->  ---> let (\v0\, \v1\) = \x in
700    if \v0\ = 0
701    then ->1
702    else if \v0\ = 1
703    then if length \v1\ > 0
704        then let (cap, slot) = \v1\ !! 0
705        in ->2
706        else ->3
707    else if \v0\ = 2
708    then ->4
709    else ->5
710
711case \x of (Zombie {}) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
712    if isZombie cap
713    then ->1
714    else if isUntypedCap cap
715    then ->2
716    else if isReplyCap cap
717    then ->3
718    else if isArchObjectCap cap
719    then let cap = capCap cap
720        in ->4
721    else ->5
722
723case \x of ((EndpointCap { capEPPtr = ptr }), True) -> ((NotificationCap { capNtfnPtr = ptr }), True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True) -> ((ThreadCap { capTCBPtr = tcb}), True) -> (z@(Zombie {}), True) -> ((ArchObjectCap { capCap = cap }), final) -> ((IRQHandlerCap { capIRQ = irq }), True) -> (NullCap, _) -> ((Zombie {}), False) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
724    if isEndpointCap \v0\ \<and> \v1\
725    then let ptr = capEPPtr \v0\
726        in ->1
727    else if isNotificationCap \v0\ \<and> \v1\
728    then let ptr = capNtfnPtr \v0\
729        in ->2
730    else if isCNodeCap \v0\ \<and> \v1\
731    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
732        in ->3
733    else if isThreadCap \v0\ \<and> \v1\
734    then let tcb = capTCBPtr \v0\
735        in ->4
736    else if isZombie \v0\ \<and> \v1\
737    then let z = \v0\
738        in ->5
739    else if isArchObjectCap \v0\
740    then let cap = capCap \v0\; final = \v1\
741        in ->6
742    else if isIRQHandlerCap \v0\ \<and> \v1\
743    then let irq = capIRQ \v0\
744        in ->7
745    else if isNullCap \v0\
746    then ->8
747    else if isZombie \v0\ \<and> \<not> \v1\
748    then ->9
749    else ->10
750
751case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) ->  ---> let (a, b) = \x in
752    if isNullCap b
753    then ->1
754    else if isUntypedCap a
755    then ->2
756    else if isEndpointCap a \<and> isEndpointCap b
757    then ->3
758    else if isNotificationCap a \<and> isNotificationCap b
759    then ->4
760    else if isCNodeCap a \<and> isCNodeCap b
761    then ->5
762    else if isThreadCap a \<and> isThreadCap b
763    then ->6
764    else if isIRQControlCap a \<and> isIRQControlCap b
765    then ->7
766    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
767    then (case (a, b) of
768        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->8
769        )
770    else if isArchObjectCap a \<and> isArchObjectCap b
771    then (case (a, b) of
772        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->9
773        )
774    else ->10
775
776case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, (ArchObjectCap { capCap = aoCap })) -> (_, _, cap) ->  ---> let (\v0\, \v1\, \v2\) = \x in
777    if isEndpointCap \v2\
778    then let preserve = \v0\; new = \v1\; cap = \v2\
779        in ->1
780    else if isNotificationCap \v2\
781    then let preserve = \v0\; new = \v1\; cap = \v2\
782        in ->2
783    else if isCNodeCap \v2\
784    then let w = \v1\; cap = \v2\
785        in ->3
786    else if isArchObjectCap \v2\
787    then let p = \v0\; w = \v1\; aoCap = capCap \v2\
788        in ->4
789    else let cap = \v2\
790    in ->5
791
792case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) ->  ---> let c = \x; aoCap = capCap \x in
793    if isNullCap c
794    then ->1
795    else if isUntypedCap c
796    then ->2
797    else if isEndpointCap c
798    then ->3
799    else if isNotificationCap c
800    then ->4
801    else if isReplyCap c
802    then ->5
803    else if isCNodeCap c
804    then ->6
805    else if isThreadCap c
806    then ->7
807    else if isIRQControlCap c
808    then ->8
809    else if isIRQHandlerCap c
810    then ->9
811    else if isArchObjectCap c
812    then ->10
813    else if isZombie c
814    then ->11
815    else undefined
816
817case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ ->  ---> let cap = \x in
818    if isEndpointCap cap \<and> capEPCanSend cap
819    then ->1
820    else if isNotificationCap cap \<and> capNtfnCanSend cap
821    then ->2
822    else if isReplyCap cap \<and> \<not> capReplyMaster cap
823    then ->3
824    else if isThreadCap cap \<and> capTCBCanWrite cap
825    then ->4
826    else if isCNodeCap cap \<and> capCNodeCanModify cap
827    then ->5
828    else if isUntypedCap cap
829    then ->6
830    else if isIRQControlCap cap
831    then ->7
832    else if isIRQHandlerCap cap
833    then let irq = capIRQ cap
834        in ->8
835    else if isArchObjectCap cap
836    then let cap = capCap cap
837        in ->9
838    else ->10
839
840case \x of (EndpointCap { capEPPtr = p1 }, Just p2, _) | p1 == p2 -> (_, _, destSlot:slots') -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
841    if isEndpointCap \v0\ \<and> \v1\ \<noteq> None \<and> capEPPtr \v0\ = the \v1\
842    then let p1 = capEPPtr \v0\; p2 = p1
843        in ->1
844    else (case \v2\ of
845        destSlot # slots' \<Rightarrow> ->2
846      | _ \<Rightarrow> ->3
847    )
848
849case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> (NullCap, _, _) -> ((Zombie {}), False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
850    if isEndpointCap \v0\
851    then let ptr = capEPPtr \v0\; final = \v1\
852        in ->1
853    else if isNotificationCap \v0\
854    then let ptr = capNtfnPtr \v0\; final = \v1\
855        in ->2
856    else if isReplyCap \v0\
857    then ->3
858    else if \v2\
859    then ->4
860    else if isCNodeCap \v0\ \<and> \v1\
861    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
862        in ->5
863    else if isThreadCap \v0\ \<and> \v1\
864    then let tcb = capTCBPtr \v0\
865        in ->6
866    else if isZombie \v0\ \<and> \v1\
867    then let z = \v0\
868        in ->7
869    else if isArchObjectCap \v0\
870    then let cap = capCap \v0\; final = \v1\
871        in ->8
872    else if isIRQHandlerCap \v0\ \<and> \v1\
873    then let irq = capIRQ \v0\
874        in ->9
875    else if isNullCap \v0\
876    then ->10
877    else if isZombie \v0\ \<and> \<not> \v1\
878    then ->11
879    else ->12
880
881case \x of (cap@PageCap { capVPIsDevice = isDevice }) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) ->  ---> let cap = \x in
882    if isPageCap cap
883    then let isDevice = capVPIsDevice cap
884        in ->1
885    else if isPageTableCap cap
886    then let ptr = capPTBasePtr cap
887        in ->2
888    else if isPageDirectoryCap cap
889    then let ptr = capPDBasePtr cap
890        in ->3
891    else if isASIDControlCap cap
892    then ->4
893    else if isASIDPoolCap cap
894    then let base = capASIDBase cap; ptr = capASIDPool cap
895        in ->5
896    else undefined
897
898case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ ->  ---> let cap = \x in
899    if isPageCap cap \<and> \<not> capVPIsDevice cap
900    then ->1
901    else ->2
902
903case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (_, _) | label == 7 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 8 -> (_, _) | label > 8 -> _ ->  ---> let (\v0\, \v1\) = \x in
904    case (if label < 4 then 1
905          else if label = 4 then 2
906          else if label = 5 then 3
907          else if label = 6 then 4
908          else if label = 7 then 5
909          else if label = 8 then 6
910          else if label > 8 then 7 else 0, \v0\, \v1\) of
911    (Suc 0, srcIndex # srcDepth # args, srcRootCap # _)
912        \<Rightarrow> ->1
913  | (Suc (Suc 0), _, _)
914        \<Rightarrow> ->2
915  | (Suc (Suc (Suc 0)), _, _)
916        \<Rightarrow> ->3
917  | (Suc (Suc (Suc (Suc 0))), _, _)
918        \<Rightarrow> ->4
919  | (Suc (Suc (Suc (Suc (Suc 0)))), _, _)
920        \<Rightarrow> ->5
921  | (Suc (Suc (Suc (Suc (Suc (Suc 0))))),
922     pivotNewData#pivotIndex#pivotDepth#srcNewData#srcIndex#srcDepth#_,
923     pivotRootCap#srcRootCap#_)
924        \<Rightarrow> ->6
925  | (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))), _, _)
926        \<Rightarrow> ->7
927  | _ \<Rightarrow> ->8
928
929case \x of c2@(Zombie { capZombiePtr = ptr2 }) -> _ ->  ---> let \v0\ = \x in
930    if isZombie \v0\
931    then let c2 = \v0\; ptr2 = capZombiePtr c2
932        in ->1
933    else ->2
934
935case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n+1 }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
936    if isZombie \v0\ \<and> capZombieNumber \v0\ = 0
937    then ->1
938    else if isZombie \v0\ \<and> \<not> \v1\
939    then let ptr = capZombiePtr \v0\
940        in ->2
941    else if isZombie \v0\ \<and> \v1\
942    then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z - 1
943        in ->3
944    else ->4
945
946case \x of NullCap -> (CNodeCap {}) -> (ThreadCap {}) -> (Zombie { capZombiePtr = ptr, capZombieType = tp, capZombieNumber = n}) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
947    if isNullCap cap
948    then ->1
949    else if isCNodeCap cap
950    then ->2
951    else if isThreadCap cap
952    then ->3
953    else if isZombie cap
954    then let ptr = capZombiePtr cap; tp = capZombieType cap;
955             n = capZombieNumber cap
956        in ->4
957    else if isEndpointCap cap
958    then let ep = capEPPtr cap; b = capEPBadge cap
959        in ->5
960    else if isArchObjectCap cap
961    then let cap = capCap cap
962        in ->6
963    else ->7
964
965case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) ->  ---> let (a, b) = \x in
966    if isNullCap b
967    then ->1
968    else if isUntypedCap a
969    then ->2
970    else if isEndpointCap a \<and> isEndpointCap b
971    then ->3
972    else if isNotificationCap a \<and> isNotificationCap b
973    then ->4
974    else if isCNodeCap a \<and> isCNodeCap b
975    then ->5
976    else if isThreadCap a \<and> isThreadCap b
977    then ->6
978    else if isIRQControlCap a \<and> isIRQControlCap b
979    then ->7
980    else if isIRQControlCap a \<and> isIRQHandlerCap b
981    then ->8
982    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
983    then (case (a, b) of
984        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9
985        )
986    else if isArchObjectCap a \<and> isArchObjectCap b
987    then (case (a, b) of
988        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10
989        )
990    else ->11
991
992case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) ->  ---> let (a, b) = \x in
993    if isUntypedCap a
994    then ->1
995    else if isEndpointCap a \<and> isEndpointCap b
996    then ->2
997    else if isNotificationCap a \<and> isNotificationCap b
998    then ->3
999    else if isCNodeCap a \<and> isCNodeCap b
1000    then ->4
1001    else if isThreadCap a \<and> isThreadCap b
1002    then ->5
1003    else if isReplyCap a \<and> isReplyCap b
1004    then ->6
1005    else if isIRQControlCap a \<and> isIRQControlCap b
1006    then ->7
1007    else if isIRQControlCap a \<and> isIRQHandlerCap b
1008    then ->8
1009    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
1010    then (case (a, b) of
1011        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9
1012        )
1013    else if isArchObjectCap a \<and> isArchObjectCap b
1014    then (case (a, b) of
1015        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10
1016        )
1017    else ->11
1018
1019case \x of ((a@PageCap {}), (b@PageCap {})) -> (a, b) ->  ---> let (a, b) = \x in
1020    if isPageCap a \<and> isPageCap b
1021    then ->1
1022    else ->2
1023
1024case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (a, b) ->  ---> let (a, b) = \x in
1025    if isPageCap a \<and> isPageCap b
1026    then let ptrA = capVPBasePtr a
1027        in ->1
1028    else ->2
1029
1030case \x of NullCap -> c2@(Zombie { capZombiePtr = ptr2 }) -> _ ->  ---> let c2 = \x in
1031    if isNullCap c2
1032    then ->1
1033    else if isZombie c2
1034    then let ptr2 = capZombiePtr c2
1035        in ->2
1036    else ->3
1037
1038case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
1039    if isEndpointCap \v0\
1040    then let ptr = capEPPtr \v0\; final = \v1\
1041        in ->1
1042    else if isNotificationCap \v0\
1043    then let ptr = capNtfnPtr \v0\; final = \v1\
1044        in ->2
1045    else if isReplyCap \v0\
1046    then ->3
1047    else if isNullCap \v0\
1048    then ->4
1049    else if \v2\
1050    then ->5
1051    else if isCNodeCap \v0\ \<and> \v1\
1052    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
1053        in ->6
1054    else if isThreadCap \v0\ \<and> \v1\
1055    then let tcb = capTCBPtr \v0\
1056        in ->7
1057    else if isZombie \v0\ \<and> \v1\
1058    then let z = \v0\
1059        in ->8
1060    else if isArchObjectCap \v0\
1061    then let cap = capCap \v0\; final = \v1\
1062        in ->9
1063    else if isIRQHandlerCap \v0\ \<and> \v1\
1064    then let irq = capIRQ \v0\
1065        in ->10
1066    else if isZombie \v0\ \<and> \<not> \v1\
1067    then ->11
1068    else ->12
1069
1070case \x of (cap@CNodeCap {}) -> (cap@Zombie {}) -> (cap@ThreadCap {}) -> _ ->  --->    let cap = \x in
1071    if isCNodeCap cap then ->1
1072    else if isZombie cap then ->2
1073    else if isThreadCap cap then ->3
1074    else ->4
1075
1076case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
1077    if isZombie cap
1078    then ->1
1079    else if isIRQControlCap cap
1080    then ->2
1081    else if isUntypedCap cap
1082    then ->3
1083    else if isReplyCap cap
1084    then ->4
1085    else if isArchObjectCap cap
1086    then let cap = capCap cap
1087        in ->5
1088    else ->6
1089
1090case \x of NullCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
1091    if isNullCap cap
1092    then ->1
1093    else if isZombie cap
1094    then let ptr = capZombiePtr cap; tp = capZombieType cap;
1095             n = capZombieNumber cap
1096        in ->2
1097    else if isEndpointCap cap
1098    then let ep = capEPPtr cap; b = capEPBadge cap
1099        in ->3
1100    else if isArchObjectCap cap
1101    then let cap = capCap cap
1102        in ->4
1103    else ->5
1104
1105case \x of cte@(CTE { cteMDBNode = mdb }) ->  ---> let cte = \x; mdb = cteMDBNode cte
1106 in ->1
1107
1108case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
1109    if \v0\ = 0 then
1110        if length \v1\ > 1 \<and> length \v2\ > 0
1111        then let vaddr = \v1\ !! 0;
1112            attr = \v1\ !! 1;
1113            pdCap = fst (\v2\ !! 0)
1114        in ->1
1115        else ->2
1116    else if \v0\ = 1 then ->3
1117    else ->4
1118
1119case \x of (slot, 0) -> (_, bitsLeft) ->  ---> let (slot, bitsLeft) = \x in
1120 if bitsLeft = 0
1121 then ->1 else ->2
1122
1123case \x of ((index:bits:args), cap@(CNodeCap {})) -> (_, (CNodeCap {})) -> (_, _) ->  ---> let (\v0\, cap) = \x in
1124    if isCNodeCap cap
1125    then
1126        (case \v0\ of
1127            (index # bits # args) \<Rightarrow> ->1
1128          | _ \<Rightarrow> ->2
1129    )
1130    else ->3
1131
1132case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ ->  ---> let cap = \x in
1133    if isEndpointCap cap \<and> capEPCanSend cap
1134    then ->1
1135    else if isNotificationCap cap \<and> capNtfnCanSend cap
1136    then ->2
1137    else if isReplyCap cap \<and> \<not> capReplyMaster cap
1138    then ->3
1139    else if isThreadCap cap
1140    then ->4
1141    else if isCNodeCap cap
1142    then ->5
1143    else if isUntypedCap cap
1144    then ->6
1145    else if isIRQControlCap cap
1146    then ->7
1147    else if isIRQHandlerCap cap
1148    then let irq = capIRQ cap
1149        in ->8
1150    else if isArchObjectCap cap
1151    then let cap = capCap cap
1152        in ->9
1153    else ->10
1154
1155case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap { capBlockSize = b }) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
1156    if isZombie cap
1157    then ->1
1158    else if isIRQControlCap cap
1159    then ->2
1160    else if isUntypedCap cap
1161    then let b = capBlockSize cap
1162        in ->3
1163    else if isReplyCap cap
1164    then ->4
1165    else if isArchObjectCap cap
1166    then let cap = capCap cap
1167        in ->5
1168    else ->6
1169
1170case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
1171    if isZombie \v0\ \<and> capZombieNumber \v0\ = 0
1172    then ->1
1173    else if isZombie \v0\ \<and> \<not> \v1\
1174    then let ptr = capZombiePtr \v0\
1175        in ->2
1176    else if isZombie \v0\ \<and> \v1\
1177    then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z
1178        in ->3
1179    else ->4
1180
1181case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (DomainCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> (cap@(IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) ->  ---> let (\v0\, \v1\, \v2\) = \x in
1182    if isEndpointCap \v0\
1183    then let ptr = capEPPtr \v0\; final = \v1\
1184        in ->1
1185    else if isNotificationCap \v0\
1186    then let ptr = capNtfnPtr \v0\; final = \v1\
1187        in ->2
1188    else if isReplyCap \v0\
1189    then ->3
1190    else if isNullCap \v0\
1191    then ->4
1192    else if isDomainCap \v0\
1193    then ->5
1194    else if \v2\
1195    then ->6
1196    else if isCNodeCap \v0\ \<and> \v1\
1197    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
1198        in ->7
1199    else if isThreadCap \v0\ \<and> \v1\
1200    then let tcb = capTCBPtr \v0\
1201        in ->8
1202    else if isZombie \v0\ \<and> \v1\
1203    then let z = \v0\
1204        in ->9
1205    else if isArchObjectCap \v0\
1206    then let cap = capCap \v0\; final = \v1\
1207        in ->10
1208    else if isIRQHandlerCap \v0\ \<and> \v1\
1209    then let irq = capIRQ \v0\; cap = \v0\
1210        in ->11
1211    else if isZombie \v0\ \<and> \<not> \v1\
1212    then ->12
1213    else ->13
1214
1215case \x of NullCap -> DomainCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
1216    if isNullCap cap
1217    then ->1
1218    else if isDomainCap cap
1219    then ->2
1220    else if isZombie cap
1221    then let ptr = capZombiePtr cap; tp = capZombieType cap;
1222             n = capZombieNumber cap
1223        in ->3
1224    else if isEndpointCap cap
1225    then let ep = capEPPtr cap; b = capEPBadge cap
1226        in ->4
1227    else if isArchObjectCap cap
1228    then let cap = capCap cap
1229        in ->5
1230    else ->6
1231
1232case \x of NullCap -> DomainCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) ->  ---> let c = \x; aoCap = capCap \x in
1233    if isNullCap c
1234    then ->1
1235    else if isDomainCap c
1236    then ->2
1237    else if isUntypedCap c
1238    then ->3
1239    else if isEndpointCap c
1240    then ->4
1241    else if isNotificationCap c
1242    then ->5
1243    else if isReplyCap c
1244    then ->6
1245    else if isCNodeCap c
1246    then ->7
1247    else if isThreadCap c
1248    then ->8
1249    else if isIRQControlCap c
1250    then ->9
1251    else if isIRQHandlerCap c
1252    then ->10
1253    else if isArchObjectCap c
1254    then ->11
1255    else if isZombie c
1256    then ->12
1257    else undefined
1258
1259case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> DomainCap -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ ->  ---> let cap = \x in
1260    if isEndpointCap cap \<and> capEPCanSend cap
1261    then ->1
1262    else if isNotificationCap cap \<and> capNtfnCanSend cap
1263    then ->2
1264    else if isReplyCap cap \<and> \<not> capReplyMaster cap
1265    then ->3
1266    else if isThreadCap cap
1267    then ->4
1268    else if isDomainCap cap
1269    then ->5
1270    else if isCNodeCap cap
1271    then ->6
1272    else if isUntypedCap cap
1273    then ->7
1274    else if isIRQControlCap cap
1275    then ->8
1276    else if isIRQHandlerCap cap
1277    then let irq = capIRQ cap
1278        in ->9
1279    else if isArchObjectCap cap
1280    then let cap = capCap cap
1281        in ->10
1282    else ->11
1283
1284
1285case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (DomainCap, DomainCap) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) ->  ---> let (a, b) = \x in
1286    if isUntypedCap a
1287    then ->1
1288    else if isEndpointCap a \<and> isEndpointCap b
1289    then ->2
1290    else if isNotificationCap a \<and> isNotificationCap b
1291    then ->3
1292    else if isCNodeCap a \<and> isCNodeCap b
1293    then ->4
1294    else if isThreadCap a \<and> isThreadCap b
1295    then ->5
1296    else if isReplyCap a \<and> isReplyCap b
1297    then ->6
1298    else if isDomainCap a \<and> isDomainCap b
1299    then ->7
1300    else if isIRQControlCap a \<and> isIRQControlCap b
1301    then ->8
1302    else if isIRQControlCap a \<and> isIRQHandlerCap b
1303    then ->9
1304    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
1305    then (case (a, b) of
1306        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->10
1307        )
1308    else if isArchObjectCap a \<and> isArchObjectCap b
1309    then (case (a, b) of
1310        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->11
1311        )
1312    else ->12
1313
1314case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
1315    if isPageDirectoryCap cap
1316    then ->1
1317    else if isPageTableCap cap
1318    then ->2
1319    else if isPageCap cap
1320    then ->3
1321    else if isASIDControlCap cap
1322    then ->4
1323    else if isASIDPoolCap cap
1324    then ->5
1325    else undefined
1326
1327case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedAddress = Just _ }) -> (PageDirectoryCap { capPDMappedAddress = Nothing }) -> (c@PDPointerTableCap { capPDPTMappedAddress = Just _ }) -> (PDPointerTableCap { capPDPTMappedAddress = Nothing }) -> (c@PML4Cap { capPML4MappedASID = Just _ }) -> (PML4Cap { capPML4MappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@IOPortCap {}) -> IOPortControlCap -> ---> let c = \x in
1328    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
1329    then ->1
1330    else if isPageTableCap c \<and> capPTMappedAddress c = None
1331    then ->2
1332    else if isPageDirectoryCap c \<and> capPDMappedAddress c \<noteq> None
1333    then ->3
1334    else if isPageDirectoryCap c \<and> capPDMappedAddress c = None
1335    then ->4
1336    else if isPDPointerTableCap c \<and> capPDPTMappedAddress c \<noteq> None
1337    then ->5
1338    else if isPDPointerTableCap c \<and> capPDPTMappedAddress c = None
1339    then ->6
1340    else if isPML4Cap c \<and> capPML4MappedASID c \<noteq> None
1341    then ->7
1342    else if isPML4Cap c \<and> capPML4MappedASID c = None
1343    then ->8
1344    else if isPageCap c
1345    then ->9
1346    else if isASIDControlCap c
1347    then ->10
1348    else if isASIDPoolCap c
1349    then ->11
1350    else if isIOPortCap c
1351    then ->12
1352    else if isIOPortControlCap c
1353    then ->13
1354    else undefined
1355
1356case \x of (c@IOPortCap {}) -> c ->  ---> let c = \x in
1357   if isIOPortCap c
1358   then ->1
1359   else ->2
1360
1361case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) ->  ---> let cap = \x in
1362    if isPageCap cap
1363    then ->1
1364    else if isPageTableCap cap
1365    then let ptr = capPTBasePtr cap
1366        in ->2
1367    else if isPageDirectoryCap cap
1368    then let ptr = capPDBasePtr cap
1369        in ->3
1370    else if isPDPointerTableCap cap
1371    then let ptr = capPDPTBasePtr cap
1372        in ->4
1373    else if isPML4Cap cap
1374    then let ptr = capPML4BasePtr cap
1375        in ->5
1376    else if isIOPortCap cap
1377    then ->6
1378    else if isIOSpaceCap cap
1379    then ->7
1380    else if isIOPageTableCap cap
1381    then let ptr = capIOPTBasePtr cap
1382        in ->8
1383    else if isASIDControlCap cap
1384    then ->9
1385    else if isASIDPoolCap cap
1386    then let base = capASIDBase cap; ptr = capASIDPool cap
1387        in ->10
1388    else undefined
1389
1390case \x of (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, index:depth:ioapic:pin:level:polarity:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, _, _) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, index:depth:pciBus:pciDev:pciFunc:handle:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
1391    case (label, args, extraCaps) of
1392      (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC,
1393        index#depth#ioapic#pin#level#polarity#irqW#_, cnode#_) => ->1
1394    | (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, _, _) => ->2
1395    | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI,
1396        index#depth#pciBus#pciDev#pciFunc#handle#irqW#_, cnode#_) => ->3
1397    | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, _, _) => ->4
1398    | _ => ->5
1399
1400case \x of (ArchInv.IssueIRQHandlerIOAPIC (IRQ irq) destSlot srcSlot ioapic pin level polarity vector) -> (ArchInv.IssueIRQHandlerMSI (IRQ irq) destSlot srcSlot pciBus pciDev pciFunc handle) ->  ---> let inv = \x in
1401    case inv of
1402      (IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic pin level polarity vector) => ->1
1403    | (IssueIRQHandlerMSI irq destSlot srcSlot pciBus pciDev pciFunc handle) => ->2
1404
1405case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap {}) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) ->  ---> let cap = \x in
1406    if isPageCap cap
1407    then ->1
1408    else if isPageTableCap cap
1409    then let ptr = capPTBasePtr cap in ->2
1410    else if isPageDirectoryCap cap
1411    then let ptr = capPDBasePtr cap in ->3
1412    else if isPDPointerTableCap cap
1413    then let ptr = capPDPTBasePtr cap in ->4
1414    else if isPML4Cap cap
1415    then let ptr = capPML4BasePtr cap in ->5
1416    else if isIOPortCap cap
1417    then ->6
1418    else if isIOSpaceCap cap
1419    then ->7
1420    else if isIOPageTableCap cap
1421    then let ptr = capIOPTBasePtr cap in ->8
1422    else if isASIDControlCap cap
1423    then ->9
1424    else if isASIDPoolCap cap
1425    then let base = capASIDBase cap; ptr = capASIDPool cap in ->10
1426    else undefined
1427
1428case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.PDPointerTableObject -> Arch.Types.PML4Object ->  ---> let t = \x in
1429    case t of
1430     APIObjectType _ => ->1
1431   | SmallPageObject => ->2
1432   | LargePageObject => ->3
1433   | HugePageObject => ->4
1434   | PageTableObject => ->5
1435   | PageDirectoryObject => ->6
1436   | PDPointerTableObject => ->7
1437   | PML4Object => ->8
1438
1439case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> ((a@PDPointerTableCap {}), (b@PDPointerTableCap {})) -> ((a@PML4Cap {}), (b@PML4Cap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@IOPortCap {}), (b@IOPortCap {})) -> (IOPortControlCap, IOPortControlCap) -> (IOPortControlCap, (IOPortCap {})) -> (_, _) ->  ---> let (a,b) = \x in
1440    if isPageCap a \<and> isPageCap b
1441    then ->1
1442    else if isPageTableCap a \<and> isPageTableCap b
1443    then ->2
1444    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
1445    then ->3
1446    else if isPDPointerTableCap a \<and> isPDPointerTableCap b
1447    then ->4
1448    else if isPML4Cap a \<and> isPML4Cap b
1449    then ->5
1450    else if isASIDControlCap a \<and> isASIDControlCap b
1451    then ->6
1452    else if isASIDPoolCap a \<and> isASIDPoolCap b
1453    then ->7
1454    else if isIOPortCap a \<and> isIOPortCap b
1455    then ->8
1456    else if isIOPortControlCap a \<and> isIOPortControlCap b
1457    then ->9
1458    else if isIOPortControlCap a \<and> isIOPortCap b
1459    then ->10
1460    else ->11
1461
1462
1463case \x of (oper@(InvokeIOPort _)) -> (oper@(InvokeIOPortControl _)) -> oper ->  ---> let oper = \x in
1464    case oper of
1465      InvokeIOPort _ => ->1
1466    | InvokeIOPortControl _ => ->2
1467    | _ => ->3
1468
1469case \x of (cap@PageCap {}) -> _ ->  ---> let cap = \x in
1470    if isPageCap cap
1471    then ->1
1472    else ->2
1473
1474case \x of (ArchInvocationLabel X64IOPortControlIssue, f:l:index:depth:_, cnode:_) -> (ArchInvocationLabel X64IOPortControlIssue, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
1475    case (label, args, extraCaps) of
1476      (ArchInvocationLabel X64IOPortControlIssue, f#l#index#depth#_, cnode#_) => ->1
1477    | (ArchInvocationLabel X64IOPortControlIssue, _, _) => ->2
1478    | _ => ->3
1479
1480case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
1481    case (label, args, extraCaps) of
1482      (ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1
1483    | (ArchInvocationLabel X64PDPTMap, _, _) => ->2
1484    | (ArchInvocationLabel X64PDPTUnmap, _, _) => ->3
1485    | _ => ->4
1486
1487case \x of (ArchInvocationLabel X64PageDirectoryMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
1488    case (label, args, extraCaps) of
1489      (ArchInvocationLabel X64PageDirectoryMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1
1490    | (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2
1491    | (ArchInvocationLabel X64PageDirectoryUnmap, _, _) => ->3
1492    | _ => ->4
1493
1494case \x of (ArchInvocationLabel X64PageTableMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageTableMap, _, _) -> (ArchInvocationLabel X64PageTableUnmap, _, _) -> _ ->  --->let (label, args, extraCaps) = \x in
1495    case (label, args, extraCaps) of
1496      (ArchInvocationLabel X64PageTableMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1
1497    | (ArchInvocationLabel X64PageTableMap, _, _) => ->2
1498    | (ArchInvocationLabel X64PageTableUnmap, _, _) => ->3
1499    | _ => ->4
1500
1501
1502case \x of (ArchInvocationLabel X64ASIDControlMakePool, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (ArchInvocationLabel X64ASIDControlMakePool, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
1503    case (label, args, extraCaps) of
1504      (ArchInvocationLabel X64ASIDControlMakePool, index#depth#_, (untyped,parentSlot)#(croot,_):_) => ->1
1505    | (ArchInvocationLabel X64ASIDControlMakePool, _, _) => ->2
1506    | _ => ->3
1507
1508case \x of (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot):_) -> (ArchInvocationLabel X64ASIDPoolAssign, _) -> _ ->  ---> let (label, extraCaps) = \x in
1509    case (label, extraCaps) of
1510      (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot)#_) => ->1
1511    | (ArchInvocationLabel X64ASIDPoolAssign, _) => ->2
1512    | _ => ->3
1513
1514case \x of cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> _ ->  ---> let cap = \x in
1515    if isPDPointerTableCap cap
1516    then ->1
1517    else if isPageDirectoryCap cap
1518    then ->2
1519    else if isPageTableCap cap
1520    then ->3
1521    else if isPageCap cap
1522    then ->4
1523    else if isASIDPoolCap cap
1524    then ->5
1525    else ->6
1526
1527case \x of (cap@(IOPortCap { capIOPortFirstPort = first_allowed, capIOPortLastPort = last_allowed })) -> _ ->  ---> let cap = \x in
1528    if isIOPortCap cap
1529    then let first_allowed = capIOPortFirstPort cap; last_allowed = capIOPortLastPort cap in ->1
1530    else ->2
1531
1532case \x of (ArchInvocationLabel X64IOPortIn8, port':_) -> (ArchInvocationLabel X64IOPortIn8, _) -> (ArchInvocationLabel X64IOPortIn16, port':_) -> (ArchInvocationLabel X64IOPortIn16, _) -> (ArchInvocationLabel X64IOPortIn32, port':_) -> (ArchInvocationLabel X64IOPortIn32, _) -> (ArchInvocationLabel X64IOPortOut8, port':out:_) -> (ArchInvocationLabel X64IOPortOut8, _) -> (ArchInvocationLabel X64IOPortOut16, port':out:_) -> (ArchInvocationLabel X64IOPortOut16, _) -> (ArchInvocationLabel X64IOPortOut32, port':out:_) -> (ArchInvocationLabel X64IOPortOut32, _) -> (_, _) ->  ---> let (label, args) = \x in
1533    case (label, args) of
1534      (ArchInvocationLabel X64IOPortIn8, port'#_) => ->1
1535    | (ArchInvocationLabel X64IOPortIn8, _) => ->2
1536    | (ArchInvocationLabel X64IOPortIn16, port'#_) => ->3
1537    | (ArchInvocationLabel X64IOPortIn16, _) => ->4
1538    | (ArchInvocationLabel X64IOPortIn32, port'#_) => ->5
1539    | (ArchInvocationLabel X64IOPortIn32, _) => ->6
1540    | (ArchInvocationLabel X64IOPortOut8, port'#out:_) => ->7
1541    | (ArchInvocationLabel X64IOPortOut8, _) => ->8
1542    | (ArchInvocationLabel X64IOPortOut16, port'#out#_) => ->9
1543    | (ArchInvocationLabel X64IOPortOut16, _) => ->10
1544    | (ArchInvocationLabel X64IOPortOut32, port'#out#_) => ->11
1545    | (ArchInvocationLabel X64IOPortOut32, _) => ->12
1546    | _ => ->13
1547
1548case \x of cap@(IOPortCap {}) -> _ ->  ---> let cap = \x in
1549    if isIOPortCap cap
1550    then ->1
1551    else ->2
1552
1553case \x of cap@(IOPortCap {}) -> IOPortControlCap -> _ ->  ---> let cap = \x in
1554    if isIOPortCap cap
1555    then ->1
1556    else if isIOPortControlCap cap
1557    then ->2
1558    else ->3
1559
1560case \x of (cap @ (CNodeCap {})) -> (cap @ (ThreadCap {})) -> (cap @ (Zombie {})) -> _ ->  ---> let cap = \x in
1561    if isCNodeCap cap
1562    then ->1
1563    else if isThreadCap cap
1564    then ->2
1565    else if isZombie cap
1566    then ->3
1567    else ->4
1568
1569case \x of ArchInv.IOPortIn8 -> ArchInv.IOPortIn16 -> ArchInv.IOPortIn32 -> ArchInv.IOPortOut8 w -> ArchInv.IOPortOut16 w -> ArchInv.IOPortOut32 w ->  ---> let port_data = \x in
1570    case port_data of
1571      IOPortIn8 => ->1
1572    | IOPortIn16 => ->2
1573    | IOPortIn32 => ->3
1574    | IOPortOut8 w => ->4
1575    | IOPortOut16 w => ->5
1576    | IOPortOut32 w => ->6
1577
1578case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageMap, _, _) -> (ArchInvocationLabel X64PageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageRemap, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> (ArchInvocationLabel X64PageGetAddress, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
1579    case (ilabel, args, extraCaps) of
1580     (ArchInvocationLabel X64PageMap, vaddr#rightsMask#attr#_, (vspaceCap, _)#_) => ->1
1581   | (ArchInvocationLabel X64PageMap, _, _) => ->2
1582   | (ArchInvocationLabel X64PageRemap, rightsMask#attr#_, (vspaceCap, _)#_) => ->3
1583   | (ArchInvocationLabel X64PageRemap, _, _) => ->4
1584   | (ArchInvocationLabel X64PageUnmap, _, _) => ->5
1585   | (ArchInvocationLabel X64PageGetAddress, _, _) => ->6
1586   | _ => ->7
1587
1588case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
1589    case (ilabel, args, extraCaps) of
1590      (ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1
1591    | (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2
1592    | (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3
1593    | _ => ->4
1594
1595case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
1596    case (ilabel, args, extraCaps) of
1597      (ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1
1598    | (ArchInvocationLabel X64PageMapIO, _, _) => ->2
1599    | (ArchInvocationLabel X64PageUnmap, _, _) => ->3
1600    | _ => ->4
1601
1602case \x of cap@(PDPointerTableCap {}) -> _ ->  ---> let cap = \x in
1603  if isPDPointerTableCap cap
1604  then ->1
1605  else ->2
1606
1607case \x of cap@(PageDirectoryCap {}) -> _ ->  ---> let cap = \x in
1608  if isPageDirectoryCap cap
1609  then ->1
1610  else ->2
1611
1612case \x of cap@(PageTableCap {}) -> _ ->  ---> let cap = \x in
1613  if isPageTableCap cap
1614   then ->1
1615   else ->2
1616
1617case \x of cap@(ASIDPoolCap {}) -> _ ->  ---> let cap = \x in
1618  if isASIDPoolCap cap
1619  then ->1
1620  else ->2
1621
1622case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> cap@(IOPageTableCap {}) -> cap@(PML4Cap {}) -> _ ->  --->  let cap = \x in
1623  if isPageCap cap
1624  then ->1
1625  else if isPDPointerTableCap cap
1626  then ->2
1627  else if isPageDirectoryCap cap
1628  then ->3
1629  else if isPageTableCap cap
1630  then ->4
1631  else if isASIDControlCap cap
1632  then ->5
1633  else if isASIDPoolCap cap
1634  then ->6
1635  else if isIOPageTableCap cap
1636  then ->7
1637  else if isPML4Cap cap
1638  then ->8
1639  else ->9
1640
1641case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (PML4Cap {}) -> _ ->  ---> let cap = \x in
1642  if isPageCap cap
1643  then ->1
1644  else if isPDPointerTableCap cap
1645  then ->2
1646  else if isPageDirectoryCap cap
1647  then ->3
1648  else if isPageTableCap cap
1649  then ->4
1650  else if isASIDControlCap cap
1651  then ->5
1652  else if isASIDPoolCap cap
1653  then ->6
1654  else if isPML4Cap cap
1655  then ->7
1656  else ->8
1657
1658
1659case \x of cap@(IOPageTableCap {}) -> _ ->  ---> let cap = \x in
1660  if isIOPageTableCap
1661  then ->1
1662  else ->2
1663
1664case \x of (cap@UntypedCap {}) -> _ ->  ---> let cap = \x in
1665  if isUntypedCap cap
1666  then ->1
1667  else ->2
1668
1669case \x of cap@(PageCap {}) -> _ ->  ---> let cap = \x in
1670  if isPageCap cap
1671  then ->1
1672  else ->2
1673
1674case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) ->  ---> let \v0\ = \x in
1675    case \v0\ of
1676      PageMap asid cap ct ctSlot entries => ->1
1677    | PageRemap entries => ->2
1678    | PageUnmap cap ctSlot => ->3
1679    | PageIOMap cap cptr ctdpte slot => ->4
1680    | PageIOUnmap (ArchObjectCap cap) ctSlot =>
1681        if isPageCap cap
1682        then ->5
1683        else ->6
1684    | PageIOUnmap _ _ => ->6
1685    | PageGetAddr ptr => ->7
1686
1687case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
1688    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool
1689    then ->1
1690    else ->2
1691
1692case \x of (cap@IOPageTableCap {}) -> _ ->  ---> let cap = \x in
1693  if isIOPageTableCap cap
1694  then ->1
1695  else ->2
1696
1697case \x of cap@(PageCap {}) -> _ ->  ---> let cap = \x in
1698  if isPageCap cap
1699  then ->1
1700  else ->2
1701
1702case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) ->  ---> let \v0\ = \x in
1703    case \v0\ of
1704      PageMap asid cap ct ctSlot entries => ->1
1705    | PageRemap entries => ->2
1706    | PageUnmap cap ctSlot => ->3
1707    | PageIOMap cap cptr ctdpte slot => ->4
1708    | PageIOUnmap (ArchObjectCap cap) ctSlot =>
1709        if isPageCap cap
1710        then ->5
1711        else ->6
1712    | PageIOUnmap _ _ => ->6
1713    | PageGetAddr ptr => ->7
1714
1715case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
1716    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool
1717    then ->1
1718    else ->2
1719
1720case \x of (cap@IOPageTableCap {}) -> _ ->  ---> let cap = \x in
1721  if isIOPageTableCap cap
1722  then ->1
1723  else ->2
1724
1725case \x of (X64NoHypFaults) -> ---> let hyp = \x in
1726  case hyp of X64NoHypFaults => ->1
1727
1728case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (IOPortControlCap, (IOPortCap {})) -> (a, b) ->  ---> let (a, b) = \x in
1729    if isPageCap a \<and> isPageCap b
1730    then let ptrA = capVPBasePtr a
1731        in ->1
1732    else if isIOPortControlCap a \<and> isIOPortCap b
1733    then -> 2
1734    else ->3
1735
1736
1737
1738
1739case \x of cap@(VCPUCap {}) -> _ ->  ---> let cap = \x in
1740   if isVCPUCap cap then -> 1
1741   else ->2
1742
1743case \x of ((field:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
1744   if isVCPUCap cap \<and> length ls > 0
1745   then let field = ls !! 0 in ->1
1746   else ->2
1747
1748case \x of ((field:val:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
1749   if isVCPUCap cap \<and> length ls > 1
1750   then let field = ls !! 0; val = ls !! 1
1751       in ->1
1752   else ->2
1753
1754case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@VCPUCap {}) ->  ---> let c = \x in
1755    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
1756    then ->1
1757    else if isPageTableCap c \<and> capPTMappedAddress c = None
1758    then ->2
1759    else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None
1760    then ->3
1761    else if isPageDirectoryCap c \<and> capPDMappedASID c = None
1762    then ->4
1763    else if isPageCap c
1764    then ->5
1765    else if isASIDControlCap c
1766    then ->6
1767    else if isASIDPoolCap c
1768    then ->7
1769    else if isVCPUCap c
1770    then ->8
1771    else undefined
1772
1773case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap {}), _) -> (_, _) ->  ---> let (cap, bl) = \x in
1774    if isASIDPoolCap cap \<and> bl
1775    then let b = capASIDBase cap; ptr = capASIDPool cap
1776         in ->1
1777    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
1778    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
1779         in ->2
1780    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
1781    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
1782         in ->3
1783    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
1784    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap in ->4
1785    else if isVCPUCap cap then ->5
1786    else ->6
1787
1788
1789case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (VCPUCap {}) ->  ---> let cap = \x in
1790    if isPageCap cap
1791    then ->1
1792    else if isPageTableCap cap
1793    then let ptr = capPTBasePtr cap
1794        in ->2
1795    else if isPageDirectoryCap cap
1796    then let ptr = capPDBasePtr cap
1797        in ->3
1798    else if isASIDControlCap cap
1799    then ->4
1800    else if isASIDPoolCap cap
1801    then let base = capASIDBase cap; ptr = capASIDPool cap
1802        in ->5
1803    else if isVCPUCap cap
1804    then ->6
1805    else undefined
1806
1807case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@VCPUCap {}), (b@VCPUCap {})) -> (_, _) ->  ---> let (a, b) = \x in
1808    if isPageCap a \<and> isPageCap b
1809    then ->1
1810    else if isPageTableCap a \<and> isPageTableCap b
1811    then ->2
1812    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
1813    then ->3
1814    else if isASIDControlCap a \<and> isASIDControlCap b
1815    then ->4
1816    else if isASIDPoolCap a \<and> isASIDPoolCap b
1817    then ->5
1818    else if isVCPUCap a \<and> isVCPUCap b
1819    then ->6
1820    else ->7
1821
1822case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.VCPUObject ->  ---> case \x of
1823 Arch.Types.APIObjectType \v0\ \<Rightarrow> ->1 | Arch.Types.SmallPageObject \<Rightarrow> ->2 | Arch.Types.LargePageObject \<Rightarrow> ->3 | Arch.Types.SectionObject \<Rightarrow> ->4 | Arch.Types.SuperSectionObject \<Rightarrow> ->5 | Arch.Types.PageTableObject \<Rightarrow> ->6 | Arch.Types.PageDirectoryObject \<Rightarrow> ->7 | Arch.Type.VCPUObject \<Rightarrow> -> 8
1824
1825case \x of ArchInv.InvokeVCPU iv -> _ ->  ---> let inv = \x
1826     in case inv of ArchInv.InvokeVCPU iv \<Rightarrow> ->1 | _ \<Rightarrow> ->2
1827
1828case \x of ((mr0:mr1:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
1829   if isVCPUCap cap \<and> length ls > 1
1830   then let mr0 = ls !! 0; mr1 = ls !! 1
1831       in ->1
1832   else ->2
1833
1834
1835case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->   ---> let cap = \x in
1836    if isPageDirectoryCap cap
1837    then ->1
1838    else if isPageTableCap cap
1839    then ->2
1840    else if isPageCap cap
1841    then ->3
1842    else if isASIDControlCap cap
1843    then ->4
1844    else if isASIDPoolCap cap
1845    then ->5
1846    else if isVCPUCap cap
1847    then ->6
1848    else undefined
1849
1850case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap { capVCPUPtr = vcpu }), True) -> (_, _) -> ---> let (cap, bl) = \x in
1851    if isASIDPoolCap cap \<and> bl
1852    then let b = capASIDBase cap; ptr = capASIDPool cap
1853         in ->1
1854    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
1855    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
1856         in ->2
1857    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
1858    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
1859         in ->3
1860    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
1861    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
1862         in ->4
1863    else if isVCPUCap cap \<and> bl
1864    then let vcpu = capVCPUPtr cap
1865         in ->5
1866    else ->6
1867
1868
1869case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (cap@VCPUCap { capVCPUPtr = vcpu }) ->  ---> let cap = \x in
1870    if isPageCap cap
1871    then ->1
1872    else if isPageTableCap cap
1873    then let ptr = capPTBasePtr cap
1874        in ->2
1875    else if isPageDirectoryCap cap
1876    then let ptr = capPDBasePtr cap
1877        in ->3
1878    else if isASIDControlCap cap
1879    then ->4
1880    else if isASIDPoolCap cap
1881    then let base = capASIDBase cap; ptr = capASIDPool cap
1882        in ->5
1883    else if isVCPUCap cap
1884    then let vcpu = capVCPUPtr cap
1885        in ->6
1886    else undefined
1887
1888
1889case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap { capVCPUPtr = vcpu }), True) -> (_, _) ->  ---> let (cap, bl) = \x in
1890    if isASIDPoolCap cap \<and> bl
1891    then let b = capASIDBase cap; ptr = capASIDPool cap
1892         in ->1
1893    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
1894    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
1895         in ->2
1896    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
1897    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
1898         in ->3
1899    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
1900    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
1901         in ->4
1902    else if isVCPUCap cap \<and> bl
1903    then let vcpu = capVCPUPtr cap
1904         in ->5
1905    else ->6
1906
1907case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> (_, _) ->  ---> let (cap, bl) = \x in
1908    if isASIDPoolCap cap \<and> bl
1909    then let b = capASIDBase cap; ptr = capASIDPool cap
1910         in ->1
1911    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
1912    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
1913         in ->2
1914    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
1915    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
1916         in ->3
1917    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
1918    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
1919         in ->4
1920    else ->5
1921
1922case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->   ---> let cap = \x in
1923    if isPageDirectoryCap cap
1924    then ->1
1925    else if isPageTableCap cap
1926    then ->2
1927    else if isPageCap cap
1928    then ->3
1929    else if isASIDControlCap cap
1930    then ->4
1931    else if isASIDPoolCap cap
1932    then ->5
1933    else if isVCPUCap cap
1934    then ->6
1935    else undefined
1936
1937case \x of UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
1938    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool \<and> \<not> capIsDevice \v0\
1939    then ->1
1940    else ->2
1941
1942case \x of UntypedCap {capIsDevice = False} | capBlockSize untyped == objBits pool -> _ ->  ---> if isUntypedCap \x \<and> (\<not> capIsDevice \x) \<and> (capBlockSize \x = objBits pool)
1943    then ->1
1944    else ->2
1945
1946case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@FrameCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) ->  ---> let c = \x in
1947  if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
1948  then ->1
1949  else if isPageTableCap c \<and> capPTMappedAddress c = None
1950  then ->2
1951  else if isFrameCap c
1952  then ->3
1953  else if c = ASIDControlCap
1954  then ->4
1955  else if isASIDPoolCap c
1956  then ->5
1957  else undefined
1958
1959case \x of c@(FrameCap {}) -> c ->  ---> let c = \x in
1960  if isFrameCap c
1961  then ->1
1962  else ->2
1963
1964case \x of ((a@FrameCap {}), (b@FrameCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) ->  ---> let (a,b) = \x in
1965  if isFrameCap a \<and> isFrameCap b
1966  then ->1
1967  else if isPageTableCap a \<and> isPageTableCap b
1968  then ->2
1969  else if a = ASIDControlCap \<and> b = ASIDControlCap
1970  then ->3
1971  else if isASIDPoolCap a \<and> isASIDPoolCap b
1972  then ->4
1973  else ->5
1974
1975case \x of ((a@FrameCap { capFBasePtr = ptrA }), (b@FrameCap {})) -> (a, b) ->  ---> let (a, b) = \x in
1976    if isFrameCap a \<and> isFrameCap b
1977    then let ptrA = capFBasePtr a in ->1
1978    else ->2
1979
1980case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject ->  ---> let t = \x in
1981    case t of
1982     APIObjectType _ => ->1
1983   | SmallPageObject => ->2
1984   | LargePageObject => ->3
1985   | HugePageObject => ->4
1986   | PageTableObject => ->5
1987
1988case \x of (cap@FrameCap {}) -> _ ->  ---> let cap = \x in
1989  if isFrameCap cap
1990  then ->1
1991  else ->2
1992
1993case \x of cap@(FrameCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
1994  if isFrameCap cap
1995  then ->1
1996  else if isPageTableCap cap
1997  then ->2
1998  else if isASIDControlCap cap
1999  then ->3
2000  else if isASIDPoolCap cap
2001  then ->4
2002  else undefined
2003
2004case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler,_,_) -> _ ->  ---> let (label, args, extraCaps) = \x in
2005    case (label, args, extraCaps) of
2006      (ArchInvocationLabel ARMIRQIssueIRQHandler,
2007        irqW#triggerW#index#depth#_, cnode#_) => ->1
2008    | (ArchInvocationLabel ARMIRQIssueIRQHandler, _, _) => ->2
2009    | _ => ->3
2010
2011case \x of (ArchInv.IssueIRQHandler (IRQ irq) destSlot srcSlot trigger) ->  ---> case \x of
2012  IssueIRQHandler irq destSlot srcSlot trigger => ->1
2013