caseconvs

case \x of 0 -> 1 -> _ ->  ---> if \x = 0
 then ->1 else if \x = 1 then ->2 else ->3

case \x of nodeCap@(CNodeCap {}) -> _ ->  ---> let nodeCap = \x in
 if isCNodeCap nodeCap
 then ->1 else ->2

case \x of root@(CNodeCap {}) -> _ ->  ---> let root = \x in
 if isCNodeCap root
 then ->1 else ->2

case \x of rt@(CNodeCap {}) -> _ ->  ---> let rt = \x in
 if isCNodeCap rt
 then ->1 else ->2

case \x of cap@(EndpointCap { capEPCanSend = True }) -> cap@(NotificationCap { capNtfnCanSend = True }) -> cap ->  ---> let cap = \x in
 if isEndpointCap cap \<and> capEPCanSend cap
 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
 then ->2 else ->3

case \x of EndpointCap { \v0\EPCanReceive = True } -> NotificationCap { \v0\NtfnCanReceive = True } -> _ ->  ---> let \v0\ = \x in
 if isEndpointCap \v0\ \<and> \v0\EPCanReceive \v0
 then ->1 else if isNotificationCap \v0\ \<and> \v0\NtfnCanReceive \v0
 then ->2 else ->3

case \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
 then ->1 else if isCNodeCap cap
 then ->2 else if isUntypedCap cap
 then ->3 else if isArchObjectCap cap
 then ->4 else if blocking
 then ->5 else ->6

case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=True}) -> (_, _) ->  ---> let (\v0\, cap) = \x in
 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0;
 bits = \v0\ !! 1;
 args = drop 2 \v0
 in ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap then ->2 else ->3

case \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
 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
 then ->2 else if isUntypedCap cap
 then ->3 else if isArchObjectCap cap
 then ->4 else if blocking
 then let ptr = capIndex in ->5 else ->6

case \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
 if isThreadCap cap \<and> capTCBCanWrite cap
 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
 then ->2 else if isUntypedCap cap
 then ->3 else if isArchObjectCap cap
 then ->4 else ->5

case \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
 if isThreadCap cap \<and> capTCBCanWrite cap
 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap
 then ->2 else if isUntypedCap cap
 then ->3 else if isArchObjectCap cap
 then ->4 else ->5

case \x of Just (slot, 0, rights) -> _ ->  ---> case \x of
 Some \v0\ \<Rightarrow> let (slot, \v1\, rights) = \v0\ in
 if \v1\ = 0 then ->1 else ->2 | None \<Rightarrow> ->2

case \x of (slot, 0, rights) -> (_, bitsLeft, _) ->  ---> let (slot, bitsLeft, rights) = \x in
 if bitsLeft = 0
 then ->1 else ->2

case \x of (index:bits:args, cnode@(CNodeCap {})) -> (_, _) ->  ---> let (L, cnode) = \x in
 if isCNodeCap cnode \<and> length L > 1 then
 let index = L !! 0;
 bits = L !! 1;
 args = drop 2 L
 in ->1 else ->2

case \x of (index:bits:args, cnode@(CNodeCap { capCNodeCanModify = True })) -> (_, CNodeCap { capCNodeCanModify = True }) -> (_, _) ->  ---> let (L, cnode) = \x in
 if isCNodeCap cnode \<and> capCNodeCanModify cnode then
 if length L > 1 then
 let index = L !! 0;
 bits = L !! 1;
 args = drop 2 L
 in ->1 else ->2 else ->3

case \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
 if isYieldToCall call
 then let thread = \v0\ in ->1 else if isThreadControlCall call \<and> length L > 6
 then let target = \v0\;
 faultep = L !! 0;
 replyep = L !! 1;
 priority = L !! 2;
 cRoot = L !! 3;
 cRootData = L !! 4;
 vRoot = L !! 5;
 vRootData = L !! 6;
 buffer = L !! 7
 in ->2 else if isExchangeRegistersCall call \<and> length L > 1
 then let dest = \v0\;
 src = L !! 0;
 save = L !! 1
 in ->3 else ->4

case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> (_,_) ->  ---> let (call, \v0\) = \x in
 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0
 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0
 then ->2 else ->3

case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> _ ->  ---> let (call, \v0\) = \x in
 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0
 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0
 then ->2 else ->3

case \x of untypedCap@(UntypedCap {}) -> _ ->  ---> let untypedCap = \x in
 if isUntypedCap untypedCap
 then ->1
 else ->1

case \x of ex2@(UserHandledFault {}) -> ex2 ->  ---> let ex2 = \x in
 if isUserHandledFault ex2
 then ->1 else ->2

case \x of 0 -> size ->  ---> let size = \x in if size = 0
 then ->1 else ->2

case \x of 0 -> ctePtr ->  ---> let ctePtr = \x in if ctePtr = 0
 then ->1 else ->2

case \x of (first:rest,_) -> ([], 0) -> ([], _) ->  ---> let \v0\ = \x in case fst \v0\ of
 first#rest \<Rightarrow> ->1 | [] \<Rightarrow> if snd \v0\ = 0
 then ->2 else ->3

case \x of Just x@(CNodeData {}) -> _ ->  ---> let \v0\ = \x in
 if \v0\ \<noteq> None \<and> isCNodeData (the \v0\)
 then let x = the \v0\ in ->1 else ->2

case \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
 if \v1\ \<and> old = EndpointData 0
 then ->1 else if \v1\ \<and> isEndpointData old
 then ->2 else if \v1\ \<and> old = AsyncEndpointData 0
 then ->3 else if \v1\ \<and> isAsyncEndpointData old
 then ->4 else if (\<not> \v1\) \<and> isCNodeData old
 then ->5 else if \v1\ \<and> isCNodeData old
 then ->6 else ->7

case \x of 0 -> slot ->  ---> let slot = \x in
 if slot = 0 then ->1 else ->2

case \x of CTE { cteCap = UntypedCap {} } -> cte@(CTE { cteMDBNode = mdb }) ->  ---> let cte = \x in
 if isUntypedCap (cteCap cte)
 then ->1 else let mdb = cteMDBNode cte
 in ->2

case \x of cap@(EndpointCap {}) -> _ ->  ---> let cap = \x in
 if isEndpointCap cap
 then ->1 else ->2

case \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
 if isUntypedCap a \<and> isUntypedCap b
 then ->1 else if isEndpointCap a \<and> isEndpointCap b
 then ->2 else if isNotificationCap a \<and> isNotificationCap b
 then ->3 else if isCNodeCap a \<and> isCNodeCap b
 then ->4 else if isThreadCap a \<and> isThreadCap b
 then ->5 else if isFrameCap a \<and> isFrameCap b
 then ->6 else if isArchObjectCap a \<and> isArchObjectCap b
 then let a = capCap a; b = capCap b in ->7 else ->8

case \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
 if isEndpointCap cap \<and> capEPCanSend cap
 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap
 then ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap
 then ->4 else if isUntypedCap cap
 then ->5 else if isArchObjectCap cap
 then ->6 else ->7

case \x of 0 -> 1 -> 2 -> _ ->  ---> let \v0\ = \x in
 if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else ->4

case \x of (CTE a@(UntypedCap {}) _, CTE b _) -> (CTE a mdbA, CTE b mdbB) ->  ---> let (\v0\, \v1\) = \x in
 case \v0\ of CTE a mdbA \<Rightarrow> (
 case \v1\ of CTE b mdbB \<Rightarrow> (
 if isUntypedCap a
 then ->1 else ->2 ))

case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> (NotificationCap {}) -> _ ->  ---> let \v0\ = \x in
 if isEndpointCap \v0\ \<and> capEPBadge \v0\ = 0
 then ->1 else if isNotificationCap \v0\ \<and> capNtfnBadge \v0\ = 0
 then ->2 else if isEndpointCap \v0
 then ->3 else if isNotificationCap \v0
 then ->4 else ->5

case \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
 if isEndpointCap \v0\ \<and> \v1
 then let ptr = capEPPtr \v0
 in ->1 else if isNotificationCap \v0\ \<and> \v1
 then let ptr = capNtfnPtr \v0
 in ->2 else if isCNodeCap \v0\ \<and> \v1\ \<and> \v2
 then let cap = \v0
 in ->3 else if isThreadCap \v0\ \<and> \v1\ \<and> \v2
 then let tcb = capTCBPtr \v0
 in ->4 else if isCNodeCap \v0\ \<and> \v1\ \<and> (\<not> \v2\)
 then let cn = capCNodePtr \v0
 in ->5 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1))
 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1
 in ->6 else if isThreadCap \v0\ \<and> \v1\ \<and> (\<not> \v2\)
 then let tcb = capTCBPtr \v0
 in ->7 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> isRight (zombieObject \v0\)
 then let tcb = theRight (zombieObject \v0\)
 in ->8 else if isZombie \v0\ \<and> \v2\ \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1))
 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1
 in ->9 else if isZombie \v0\ \<and> \v1\ \<and> (\<exists>\v3\. zombieObject \v0\ = Left (\v3\, 0))
 then ->10 else if isZombie \v0\ \<and> isRight (zombieObject \v0\) \<and> \v1\ \<and> \v2
 then let tcb = theRight (zombieObject \v0\)
 in ->11 else if isArchObjectCap \v0
 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
 in ->12 else if isFrameCap \v0
 then ->13 else if isNullCap \v0
 then ->14 else if isZombie \v0\ \<and> (\<not> \v1\)
 then ->15 else ->16

case \x of (new, cap@(EndpointCap {})) -> (new, cap@(NotificationCap {})) -> (w, cap@(CNodeCap {})) -> (w, ArchObjectCap { capCap = aoCap }) -> (_, cap) ->  ---> let (new, cap) = \x;
     w = new in
 if isEndpointCap cap
 then ->1 else if isNotificationCap cap
 then ->2 else if isCNodeCap cap
 then ->3 else if isArchObjectCap cap
 then let aoCap = capCap cap
 in ->4 else ->5

case \x of cap@(EndpointCap { capEPCanSend = True }) -> _ ->  ---> let cap = \x in
 if isEndpointCap cap \<and> capEPCanSend cap
 then ->1 else ->2

case \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
 if isEndpointCap \v0\ \<and> \v1
 then let ptr = capEPPtr \v0
 in ->1 else if isNotificationCap \v0\ \<and> \v1
 then let ptr = capNtfnPtr \v0
 in ->2 else if isCNodeCap \v0\ \<and> \v1
 then let cap = \v0\; exposed = \v2
 in ->3 else if isThreadCap \v0\ \<and> \v1
 then let tcb = capTCBPtr \v0\; exposed = \v2
 in ->4 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
 then let ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1
 in ->5 else if isZombie \v0\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
 then let ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1
 in ->6 else if isZombie \v0\ \<and> capNumber \v0\ = 0
 then ->7 else if isArchObjectCap \v0
 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
 in ->8 else if isFrameCap \v0
 then ->9 else if isNullCap \v0
 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
 then ->11 else ->12

case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=False}) -> (_, _) ->  ---> let (\v0\, cap) = \x in
 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0;
 bits = \v0\ !! 1;
 args = drop 2 \v0
 in ->1 else if isCNodeCap cap \<and> (\<not> capCNodeCanModify cap) then ->2 else ->3

case \x of 32 -> 64 -> _ ->  ---> if \x = 32
 then ->1 else if \x = 64
 then ->2 else ->3

case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@(FrameCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) ->  ---> let c = \x in
 if isNullCap c
 then ->1 else if isUntypedCap c
 then ->2 else if isEndpointCap c
 then ->3 else if isNotificationCap c
 then ->4 else if isCNodeCap c
 then ->5 else if isThreadCap c
 then ->6 else if isFrameCap c
 then ->7 else if isArchObjectCap c
 then let aoCap = capCap c
 in ->8 else (* assuming Zombie *) ->9

case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) ->  ---> let (src, new) = \x in
 if (isEndpointCap src \<and> isEndpointCap new)
 then ->1 else if (isNotificationCap src \<and> isNotificationCap new)
 then ->2 else ->3

case \x of c2@(Zombie { capCTEPtr = ptr2 }) -> _ ->  ---> let c2 = \x;
 ptr2 = capCTEPtr c2 in
 if isZombie c2
 then ->1 else ->2

case \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
 if isEndpointCap \v0\ \<and> \v1
 then let ptr = capEPPtr \v0
 in ->1 else if isNotificationCap \v0\ \<and> \v1
 then let ptr = capNtfnPtr \v0
 in ->2 else if isCNodeCap \v0\ \<and> \v1
 then let cap = \v0\; exposed = \v2
 in ->3 else if isThreadCap \v0\ \<and> \v1
 then let tcb = capTCBPtr \v0\; exposed = \v2
 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
 then let ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1
 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
 then let ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1;
 c = \v0
 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
 then ->7 else if isArchObjectCap \v0
 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
 in ->8 else if isFrameCap \v0
 then ->9 else if isNullCap \v0
 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
 then ->11 else ->12

case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) ->  ---> let (src,new) = \x in
 if isEndpointCap src & isEndpointCap new
 then ->1
 else if isNotificationCap src & isNotificationCap new
 then ->2
 else ->3

case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> NotificationCap {} -> _ ->  ---> if isEndpointCap \x \<and> capEPBadge \x = 0
 then ->1 else if isNotificationCap \x \<and> capNtfnBadge \x = 0
 then ->2 else if isEndpointCap \x then ->3 else if isNotificationCap \x
 then ->4 else ->5

case \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
 if isEndpointCap cap \<and> capEPCanSend cap
 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap
 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap
 then let sl = slot
 in ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap
 then ->4 else if isUntypedCap cap
 then ->5 else if isArchObjectCap cap
 then ->6 else ->7

case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ ->  ---> if isEndpointCap \x & capEPBadge \x = 0
 then ->1
 else if isNotificationCap \x & capNtfnBadge \x = 0
 then ->2
 else if isEndpointCap \x
 then let badge = capEPBadge \x in
 ->3
 else if isNotificationCap \x
 then let badge = capNtfnBadge \x in
 ->4
 else ->5

case \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
 if b = NullCap
 then ->1
 else if isUntypedCap a
 then ->2
 else if isEndpointCap a & isEndpointCap b
 then ->3
 else if isNotificationCap a & isNotificationCap b
 then ->4
 else if isCNodeCap a & isCNodeCap b
 then ->5
 else if isThreadCap a & isThreadCap b
 then ->6
 else if isFrameCap a & isFrameCap b
 then ->7
 else if isArchObjectCap a & isArchObjectCap b
 then let a = capCap a; b = capCap b in
 ->8
 else ->9

case \x of EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ ->  ---> if isEndpointCap \x & capEPBadge \x ~= 0
 then let badge = capEPBadge \x in
 ->1
 else if isNotificationCap \x & capNtfnBadge \x ~= 0
 then let badge = capNtfnBadge \x in
 ->2
 else ->3

case \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
 if isEndpointCap \v0\ \<and> \v1
 then let ptr = capEPPtr \v0
 in ->1 else if isNotificationCap \v0\ \<and> \v1
 then let ptr = capNtfnPtr \v0
 in ->2 else if isCNodeCap \v0\ \<and> \v1
 then let cap = \v0\; exposed = \v2
 in ->3 else if isThreadCap \v0\ \<and> \v1
 then let tcb = capTCBPtr \v0\; exposed = \v2
 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
 then let ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1
 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
 then let z = \v0\;
 ptr = capCTEPtr \v0\;
 n = capNumber \v0\ - 1;
 c = \v0
 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
 then ->7 else if isArchObjectCap \v0
 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\)
 in ->8 else if isFrameCap \v0
 then ->9 else if isNullCap \v0
 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\)
 then ->11 else ->12

case \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
 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

case \x of Zombie {} -> cap@(UntypedCap {}) -> ArchObjectCap cap -> cap ->  ---> let cap = \x
 in case cap of Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1 | UntypedCap \v0\ \v1\ \<Rightarrow> ->2 | ArchObjectCap cap \<Rightarrow> ->3 | _ \<Rightarrow> ->4

case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> _ ->  ---> let \v0\ = \x
 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

case \x of MI { msgExtraCaps = 0 } -> MI { msgExtraCaps = count } ->  ---> let \v0\ = \x
 in if msgExtraCaps \v0\ = 0 then ->1 else let count = msgExtraCaps \v0\ in ->2

case \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 case c of
 PageTableCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->2 else ->1
 | PageDirectoryCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->4 else ->3
 | PageCap \v0\ \v1\ \v2\ \v3\ \<Rightarrow> ->5
 | ASIDControlCap \<Rightarrow> ->6
 | ASIDPoolCap \v0\ \v1\ \<Rightarrow> ->7

case \x of c@(PageCap {}) -> c ->  ---> let c = \x in
 if isPageCap c
 then ->1
 else ->2

case \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
 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

case \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
 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

case \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
 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

case \x of IdleEP | blocking -> SendEP queue | blocking -> IdleEP -> SendEP _ -> RecvEP (dest:queue) -> RecvEP [] ->  ---> case \x of
 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 )

case \x of Zombie {} -> cap@(UntypedCap {}) -> ReplyCap {} -> ArchObjectCap cap -> cap ->  --->     let cap = \x
      in case cap of
         Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1
         | UntypedCap \v0\ \v1\ \<Rightarrow> ->2
         | ReplyCap \v0\ \v1\ \<Rightarrow> ->3
         | ArchObjectCap cap \<Rightarrow> ->4
         | _ \<Rightarrow> ->5

case \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
     if isEndpointCap \v0\ \<and> \v1\
     then let ptr = capEPPtr \v0
 in ->1
     else if isNotificationCap \v0\ \<and> \v1\
     then let ptr = capNtfnPtr \v0
 in ->2
     else if isCNodeCap \v0\ \<and> \v1\
     then let cap = \v0\; exposed = \v2\ in ->3
     else if isThreadCap \v0\ \<and> \v1\
     then let tcb = capTCBPtr \v0\; exposed = \v2\ in ->4
     else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0
     then let ptr = capCTEPtr \v0\;
              n = capNumber \v0\ - 1
          in ->5
     else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0
     then let z = \v0\;
              ptr = capCTEPtr \v0\;
              n = capNumber \v0\ - 1;
              c = \v0\
          in ->6
     else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0
     then ->7
     else if isIRQHandlerCap \v0\ \<and> \v1\
     then let irq = capIRQ \v0\ in ->8
     else if isArchObjectCap \v0\
     then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->9
     else if isNullCap \v0\
     then ->10
     else if isZombie \v0\ \<and> (\<not> \v1\)
     then ->11
     else ->12

case \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
    if b = NullCap
    then ->1
    else if isUntypedCap a
    then ->2
    else if isEndpointCap a & isEndpointCap b
    then ->3
    else if isNotificationCap a & isNotificationCap b
    then ->4
    else if isCNodeCap a & isCNodeCap b
    then ->5
    else if isThreadCap a & isThreadCap b
    then ->6
    else if a = IRQControlCap & b = IRQControlCap
    then ->7
    else if isIRQHandlerCap a & isIRQHandlerCap b
    then let a = capIRQ a; b = capIRQ b in ->8
    else if isArchObjectCap a & isArchObjectCap b
    then let a = capCap a; b = capCap b in
          ->9
    else ->10

case \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
    if isEndpointCap \v2\
    then let preserve = \v0\; new = \v1\; cap = \v2\ in ->1
    else if isNotificationCap \v2\
    then let preserve = \v0\; new = \v1\; cap = \v2\ in ->2
    else if isCNodeCap \v2\
    then let w = \v1\; cap = \v2\ in ->3
    else if isArchObjectCap \v2\
    then let p = \v0\; w = \v1\; aoCap = capCap \v2\ in ->4
    else let cap = \v2\ in ->5

case \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
    if isNullCap c then ->1
    else if isUntypedCap c then ->2
    else if isEndpointCap c then ->3
    else if isNotificationCap c then ->4
    else if isReplyCap c then ->5
    else if isCNodeCap c then ->6
    else if isThreadCap c then ->7
    else if isIRQControlCap c then ->8
    else if isIRQHandlerCap c then ->9
    else if isArchObjectCap c then let aoCap = capCap c in ->10
    else (* assuming Zombie *) ->11

case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> 8 -> 9 -> _ ->  --->let \v0\ = \x
 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

case \x of ArchObjectCap (pageCap@PageCap {}) -> _ ->  ---> let \v0\ = \x in
    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
    then
        let pageCap = capCap \v0\
        in ->1
    else ->2

case \x of ArchObjectCap (frameCap@PageCap {}) -> _ ->  ---> let \v0\ = \x in
    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
    then
        let frameCap = capCap \v0\
        in ->1
    else ->2

case \x of ((Zombie { capCTEPtr = ptr, capNumber = n+1 }), False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
     if isZombie \v0\ \<and> (\<not> \v1\) \<and> capNumber \v0\ \<noteq> 0
     then let ptr = capCTEPtr \v0\;
              n = capNumber \v0\ - 1
          in ->1
     else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ \<noteq> 0
     then let z = \v0\;
              ptr = capCTEPtr \v0\;
              n = capNumber \v0\ - 1
          in ->2
     else ->3

case \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
    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
    then ->1
    else if isPageTableCap c \<and> capPTMappedAddress c = None
    then ->2
    else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None
    then ->3
    else if isPageDirectoryCap c \<and> capPDMappedASID c = None
    then ->4
    else if isPageCap c
    then ->5
    else if isASIDControlCap c
    then ->6
    else if isASIDPoolCap c
    then ->7
    else undefined

case \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
    if isPageCap a \<and> isPageCap b
    then ->1
    else if isPageTableCap a \<and> isPageTableCap b
    then ->2
    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
    then ->3
    else if isASIDControlCap a \<and> isASIDControlCap b
    then ->4
    else if isASIDPoolCap a \<and> isASIDPoolCap b
    then ->5
    else ->6

case \x of ArchObjectCap (frame@PageCap {}) -> _ ->  ---> let \v0\ = \x in
    if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\)
    then let frame = capCap \v0\
         in ->1
    else ->2

case \x of ArchObjectCap (PageDirectoryCap { capPDMappedASID = Just _, capPDBasePtr = cur_pd }) | cur_pd == pd -> _ ->  ---> let \v0\ = \x in
    if isArchObjectCap \v0\ \<and> isPageDirectoryCap (capCap \v0\) \<and> capPDMappedASID (capCap \v0\) \<noteq> None \<and> capPDBasePtr (capCap \v0\) = pd
    then let cur_pd = pd in ->1
    else ->2

case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 1 \<and> length \v2\ > 0
        then let vaddr = \v1\ !! 0;
            attr = \v1\ !! 1;
            pdCap = fst (\v2\ !! 0)
        in ->1
        else ->2
    else ->3

case \x of (0, vaddr:rightsMask:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, rightsMask:attr:_, _) -> (1, _, _) -> (2, _, _) -> (3, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 2 \<and> length \v2\ > 0
        then let vaddr = \v1\ !! 0;
            rightsMask = \v1\ !! 1;
            attr = \v1\ !! 2;
            pdCap = fst (\v2\ !! 0)
        in ->1
        else ->2
    else if \v0\ = 1 then
        if length \v1\ > 1
        then let rightsMask = \v1\ !! 0;
            attr = \v1\ !! 1
        in ->3
        else ->4
    else if \v0\ = 2
    then ->5
    else if \v0\ = 3
    then ->6
    else ->7

case \x of (0, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (0, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 1 \<and> length \v2\ > 1
        then let index = \v1\ !! 0;
            depth = \v1\ !! 1;
            (untyped, parentSlot) = \v2\ !! 0;
            croot = fst (\v2\ !! 1)
        in ->1
        else ->2
    else ->3

case \x of (0, (pdCap,pdCapSlot):_) -> (0, _) -> _ ->  ---> let (\v0\, \v1\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 0
        then let (pdCap, pdCapSlot) = \v1\ !! 0
        in ->1
        else ->2
    else ->3

case \x of (PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
    if isPageDirectoryCap cap
    then ->1
    else if isPageTableCap cap
    then ->2
    else if isPageCap cap
    then ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then ->5
    else undefined

case \x of ((index:bits:args), cap@(CNodeCap {capCNodeCanModify=True})) -> (_, (CNodeCap {capCNodeCanModify=True})) -> (_, _) ->  ---> let (\v0\, cap) = \x in
    if isCNodeCap cap \<and> capCNodeCanModify cap
    then
        (case \v0\ of
            (index # bits # args) \<Rightarrow> ->1
          | _ \<Rightarrow> ->2
    )
    else ->3

case \x of ((src@EndpointCap {}), (new@EndpointCap {})) -> ((src@NotificationCap {}), (new@NotificationCap {})) -> (_, _) ->  ---> let (src, new) = \x in
    if isEndpointCap src \<and> isEndpointCap new
    then ->1
    else if isNotificationCap src \<and> isNotificationCap new
    then ->2
    else ->3

case \x of (CTE { cteCap = UntypedCap {} }) -> cte@(CTE { cteMDBNode = mdb }) ->  ---> let \v0\ = \x in
    if isUntypedCap (cteCap \v0\)
    then ->1
    else let cte = \v0\;
        mdb = cteMDBNode cte
    in ->2

case \x of 0 | length msg >= length syscallMessage -> _ ->  ---> if \x = 0 \<and> length msg \<ge> length syscallMessage
    then ->1
    else ->2

case \x of 0 | length msg >= length exceptionMessage -> _ ->  ---> if \x = 0 \<and> length msg \<ge> length exceptionMessage
    then ->1
    else ->2

case \x of (0,irqW:index:depth:_,cnode:_) -> (0,_,_) -> (1,_,_) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 2 \<and> length \v2\ > 0
        then let irqW = \v1\ !! 0;
            index = \v1\ !! 1;
            depth = \v1\ !! 2;
            cnode = \v2\ !! 0
        in ->1
        else ->2
    else if \v0\ = 1
    then ->3
    else ->4

case \x of (0,_) -> (1,(cap,slot):_) -> (1,_) -> (2,_) -> _ ->  ---> let (\v0\, \v1\) = \x in
    if \v0\ = 0
    then ->1
    else if \v0\ = 1
    then if length \v1\ > 0
        then let (cap, slot) = \v1\ !! 0
        in ->2
        else ->3
    else if \v0\ = 2
    then ->4
    else ->5

case \x of (Zombie {}) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
    if isZombie cap
    then ->1
    else if isUntypedCap cap
    then ->2
    else if isReplyCap cap
    then ->3
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->4
    else ->5

case \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
    if isEndpointCap \v0\ \<and> \v1\
    then let ptr = capEPPtr \v0\
        in ->1
    else if isNotificationCap \v0\ \<and> \v1\
    then let ptr = capNtfnPtr \v0\
        in ->2
    else if isCNodeCap \v0\ \<and> \v1\
    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
        in ->3
    else if isThreadCap \v0\ \<and> \v1\
    then let tcb = capTCBPtr \v0\
        in ->4
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\
        in ->5
    else if isArchObjectCap \v0\
    then let cap = capCap \v0\; final = \v1\
        in ->6
    else if isIRQHandlerCap \v0\ \<and> \v1\
    then let irq = capIRQ \v0\
        in ->7
    else if isNullCap \v0\
    then ->8
    else if isZombie \v0\ \<and> \<not> \v1\
    then ->9
    else ->10

case \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
    if isNullCap b
    then ->1
    else if isUntypedCap a
    then ->2
    else if isEndpointCap a \<and> isEndpointCap b
    then ->3
    else if isNotificationCap a \<and> isNotificationCap b
    then ->4
    else if isCNodeCap a \<and> isCNodeCap b
    then ->5
    else if isThreadCap a \<and> isThreadCap b
    then ->6
    else if isIRQControlCap a \<and> isIRQControlCap b
    then ->7
    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
    then (case (a, b) of
        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->8
        )
    else if isArchObjectCap a \<and> isArchObjectCap b
    then (case (a, b) of
        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->9
        )
    else ->10

case \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
    if isEndpointCap \v2\
    then let preserve = \v0\; new = \v1\; cap = \v2\
        in ->1
    else if isNotificationCap \v2\
    then let preserve = \v0\; new = \v1\; cap = \v2\
        in ->2
    else if isCNodeCap \v2\
    then let w = \v1\; cap = \v2\
        in ->3
    else if isArchObjectCap \v2\
    then let p = \v0\; w = \v1\; aoCap = capCap \v2\
        in ->4
    else let cap = \v2\
    in ->5

case \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
    if isNullCap c
    then ->1
    else if isUntypedCap c
    then ->2
    else if isEndpointCap c
    then ->3
    else if isNotificationCap c
    then ->4
    else if isReplyCap c
    then ->5
    else if isCNodeCap c
    then ->6
    else if isThreadCap c
    then ->7
    else if isIRQControlCap c
    then ->8
    else if isIRQHandlerCap c
    then ->9
    else if isArchObjectCap c
    then ->10
    else if isZombie c
    then ->11
    else undefined

case \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
    if isEndpointCap cap \<and> capEPCanSend cap
    then ->1
    else if isNotificationCap cap \<and> capNtfnCanSend cap
    then ->2
    else if isReplyCap cap \<and> \<not> capReplyMaster cap
    then ->3
    else if isThreadCap cap \<and> capTCBCanWrite cap
    then ->4
    else if isCNodeCap cap \<and> capCNodeCanModify cap
    then ->5
    else if isUntypedCap cap
    then ->6
    else if isIRQControlCap cap
    then ->7
    else if isIRQHandlerCap cap
    then let irq = capIRQ cap
        in ->8
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->9
    else ->10

case \x of (EndpointCap { capEPPtr = p1 }, Just p2, _) | p1 == p2 -> (_, _, destSlot:slots') -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if isEndpointCap \v0\ \<and> \v1\ \<noteq> None \<and> capEPPtr \v0\ = the \v1\
    then let p1 = capEPPtr \v0\; p2 = p1
        in ->1
    else (case \v2\ of
        destSlot # slots' \<Rightarrow> ->2
      | _ \<Rightarrow> ->3
    )

case \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
    if isEndpointCap \v0\
    then let ptr = capEPPtr \v0\; final = \v1\
        in ->1
    else if isNotificationCap \v0\
    then let ptr = capNtfnPtr \v0\; final = \v1\
        in ->2
    else if isReplyCap \v0\
    then ->3
    else if \v2\
    then ->4
    else if isCNodeCap \v0\ \<and> \v1\
    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
        in ->5
    else if isThreadCap \v0\ \<and> \v1\
    then let tcb = capTCBPtr \v0\
        in ->6
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\
        in ->7
    else if isArchObjectCap \v0\
    then let cap = capCap \v0\; final = \v1\
        in ->8
    else if isIRQHandlerCap \v0\ \<and> \v1\
    then let irq = capIRQ \v0\
        in ->9
    else if isNullCap \v0\
    then ->10
    else if isZombie \v0\ \<and> \<not> \v1\
    then ->11
    else ->12

case \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
    if isPageCap cap
    then let isDevice = capVPIsDevice cap
        in ->1
    else if isPageTableCap cap
    then let ptr = capPTBasePtr cap
        in ->2
    else if isPageDirectoryCap cap
    then let ptr = capPDBasePtr cap
        in ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then let base = capASIDBase cap; ptr = capASIDPool cap
        in ->5
    else undefined

case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ ->  ---> let cap = \x in
    if isPageCap cap \<and> \<not> capVPIsDevice cap
    then ->1
    else ->2

case \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
    case (if label < 4 then 1
          else if label = 4 then 2
          else if label = 5 then 3
          else if label = 6 then 4
          else if label = 7 then 5
          else if label = 8 then 6
          else if label > 8 then 7 else 0, \v0\, \v1\) of
    (Suc 0, srcIndex # srcDepth # args, srcRootCap # _)
        \<Rightarrow> ->1
  | (Suc (Suc 0), _, _)
        \<Rightarrow> ->2
  | (Suc (Suc (Suc 0)), _, _)
        \<Rightarrow> ->3
  | (Suc (Suc (Suc (Suc 0))), _, _)
        \<Rightarrow> ->4
  | (Suc (Suc (Suc (Suc (Suc 0)))), _, _)
        \<Rightarrow> ->5
  | (Suc (Suc (Suc (Suc (Suc (Suc 0))))),
     pivotNewData#pivotIndex#pivotDepth#srcNewData#srcIndex#srcDepth#_,
     pivotRootCap#srcRootCap#_)
        \<Rightarrow> ->6
  | (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))), _, _)
        \<Rightarrow> ->7
  | _ \<Rightarrow> ->8

case \x of c2@(Zombie { capZombiePtr = ptr2 }) -> _ ->  ---> let \v0\ = \x in
    if isZombie \v0\
    then let c2 = \v0\; ptr2 = capZombiePtr c2
        in ->1
    else ->2

case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n+1 }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
    if isZombie \v0\ \<and> capZombieNumber \v0\ = 0
    then ->1
    else if isZombie \v0\ \<and> \<not> \v1\
    then let ptr = capZombiePtr \v0\
        in ->2
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z - 1
        in ->3
    else ->4

case \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
    if isNullCap cap
    then ->1
    else if isCNodeCap cap
    then ->2
    else if isThreadCap cap
    then ->3
    else if isZombie cap
    then let ptr = capZombiePtr cap; tp = capZombieType cap;
             n = capZombieNumber cap
        in ->4
    else if isEndpointCap cap
    then let ep = capEPPtr cap; b = capEPBadge cap
        in ->5
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->6
    else ->7

case \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
    if isNullCap b
    then ->1
    else if isUntypedCap a
    then ->2
    else if isEndpointCap a \<and> isEndpointCap b
    then ->3
    else if isNotificationCap a \<and> isNotificationCap b
    then ->4
    else if isCNodeCap a \<and> isCNodeCap b
    then ->5
    else if isThreadCap a \<and> isThreadCap b
    then ->6
    else if isIRQControlCap a \<and> isIRQControlCap b
    then ->7
    else if isIRQControlCap a \<and> isIRQHandlerCap b
    then ->8
    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
    then (case (a, b) of
        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9
        )
    else if isArchObjectCap a \<and> isArchObjectCap b
    then (case (a, b) of
        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10
        )
    else ->11

case \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
    if isUntypedCap a
    then ->1
    else if isEndpointCap a \<and> isEndpointCap b
    then ->2
    else if isNotificationCap a \<and> isNotificationCap b
    then ->3
    else if isCNodeCap a \<and> isCNodeCap b
    then ->4
    else if isThreadCap a \<and> isThreadCap b
    then ->5
    else if isReplyCap a \<and> isReplyCap b
    then ->6
    else if isIRQControlCap a \<and> isIRQControlCap b
    then ->7
    else if isIRQControlCap a \<and> isIRQHandlerCap b
    then ->8
    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
    then (case (a, b) of
        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9
        )
    else if isArchObjectCap a \<and> isArchObjectCap b
    then (case (a, b) of
        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10
        )
    else ->11

case \x of ((a@PageCap {}), (b@PageCap {})) -> (a, b) ->  ---> let (a, b) = \x in
    if isPageCap a \<and> isPageCap b
    then ->1
    else ->2

case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (a, b) ->  ---> let (a, b) = \x in
    if isPageCap a \<and> isPageCap b
    then let ptrA = capVPBasePtr a
        in ->1
    else ->2

case \x of NullCap -> c2@(Zombie { capZombiePtr = ptr2 }) -> _ ->  ---> let c2 = \x in
    if isNullCap c2
    then ->1
    else if isZombie c2
    then let ptr2 = capZombiePtr c2
        in ->2
    else ->3

case \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
    if isEndpointCap \v0\
    then let ptr = capEPPtr \v0\; final = \v1\
        in ->1
    else if isNotificationCap \v0\
    then let ptr = capNtfnPtr \v0\; final = \v1\
        in ->2
    else if isReplyCap \v0\
    then ->3
    else if isNullCap \v0\
    then ->4
    else if \v2\
    then ->5
    else if isCNodeCap \v0\ \<and> \v1\
    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
        in ->6
    else if isThreadCap \v0\ \<and> \v1\
    then let tcb = capTCBPtr \v0\
        in ->7
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\
        in ->8
    else if isArchObjectCap \v0\
    then let cap = capCap \v0\; final = \v1\
        in ->9
    else if isIRQHandlerCap \v0\ \<and> \v1\
    then let irq = capIRQ \v0\
        in ->10
    else if isZombie \v0\ \<and> \<not> \v1\
    then ->11
    else ->12

case \x of (cap@CNodeCap {}) -> (cap@Zombie {}) -> (cap@ThreadCap {}) -> _ ->  --->    let cap = \x in
    if isCNodeCap cap then ->1
    else if isZombie cap then ->2
    else if isThreadCap cap then ->3
    else ->4

case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
    if isZombie cap
    then ->1
    else if isIRQControlCap cap
    then ->2
    else if isUntypedCap cap
    then ->3
    else if isReplyCap cap
    then ->4
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->5
    else ->6

case \x of NullCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
    if isNullCap cap
    then ->1
    else if isZombie cap
    then let ptr = capZombiePtr cap; tp = capZombieType cap;
             n = capZombieNumber cap
        in ->2
    else if isEndpointCap cap
    then let ep = capEPPtr cap; b = capEPBadge cap
        in ->3
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->4
    else ->5

case \x of cte@(CTE { cteMDBNode = mdb }) ->  ---> let cte = \x; mdb = cteMDBNode cte
 in ->1

case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, _, _) -> _ ->  ---> let (\v0\, \v1\, \v2\) = \x in
    if \v0\ = 0 then
        if length \v1\ > 1 \<and> length \v2\ > 0
        then let vaddr = \v1\ !! 0;
            attr = \v1\ !! 1;
            pdCap = fst (\v2\ !! 0)
        in ->1
        else ->2
    else if \v0\ = 1 then ->3
    else ->4

case \x of (slot, 0) -> (_, bitsLeft) ->  ---> let (slot, bitsLeft) = \x in
 if bitsLeft = 0
 then ->1 else ->2

case \x of ((index:bits:args), cap@(CNodeCap {})) -> (_, (CNodeCap {})) -> (_, _) ->  ---> let (\v0\, cap) = \x in
    if isCNodeCap cap
    then
        (case \v0\ of
            (index # bits # args) \<Rightarrow> ->1
          | _ \<Rightarrow> ->2
    )
    else ->3

case \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
    if isEndpointCap cap \<and> capEPCanSend cap
    then ->1
    else if isNotificationCap cap \<and> capNtfnCanSend cap
    then ->2
    else if isReplyCap cap \<and> \<not> capReplyMaster cap
    then ->3
    else if isThreadCap cap
    then ->4
    else if isCNodeCap cap
    then ->5
    else if isUntypedCap cap
    then ->6
    else if isIRQControlCap cap
    then ->7
    else if isIRQHandlerCap cap
    then let irq = capIRQ cap
        in ->8
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->9
    else ->10

case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap { capBlockSize = b }) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
    if isZombie cap
    then ->1
    else if isIRQControlCap cap
    then ->2
    else if isUntypedCap cap
    then let b = capBlockSize cap
        in ->3
    else if isReplyCap cap
    then ->4
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->5
    else ->6

case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n }), True) -> (_, _) ->  ---> let (\v0\, \v1\) = \x in
    if isZombie \v0\ \<and> capZombieNumber \v0\ = 0
    then ->1
    else if isZombie \v0\ \<and> \<not> \v1\
    then let ptr = capZombiePtr \v0\
        in ->2
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z
        in ->3
    else ->4

case \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
    if isEndpointCap \v0\
    then let ptr = capEPPtr \v0\; final = \v1\
        in ->1
    else if isNotificationCap \v0\
    then let ptr = capNtfnPtr \v0\; final = \v1\
        in ->2
    else if isReplyCap \v0\
    then ->3
    else if isNullCap \v0\
    then ->4
    else if isDomainCap \v0\
    then ->5
    else if \v2\
    then ->6
    else if isCNodeCap \v0\ \<and> \v1\
    then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\
        in ->7
    else if isThreadCap \v0\ \<and> \v1\
    then let tcb = capTCBPtr \v0\
        in ->8
    else if isZombie \v0\ \<and> \v1\
    then let z = \v0\
        in ->9
    else if isArchObjectCap \v0\
    then let cap = capCap \v0\; final = \v1\
        in ->10
    else if isIRQHandlerCap \v0\ \<and> \v1\
    then let irq = capIRQ \v0\; cap = \v0\
        in ->11
    else if isZombie \v0\ \<and> \<not> \v1\
    then ->12
    else ->13

case \x of NullCap -> DomainCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap ->  ---> let cap = \x in
    if isNullCap cap
    then ->1
    else if isDomainCap cap
    then ->2
    else if isZombie cap
    then let ptr = capZombiePtr cap; tp = capZombieType cap;
             n = capZombieNumber cap
        in ->3
    else if isEndpointCap cap
    then let ep = capEPPtr cap; b = capEPBadge cap
        in ->4
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->5
    else ->6

case \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
    if isNullCap c
    then ->1
    else if isDomainCap c
    then ->2
    else if isUntypedCap c
    then ->3
    else if isEndpointCap c
    then ->4
    else if isNotificationCap c
    then ->5
    else if isReplyCap c
    then ->6
    else if isCNodeCap c
    then ->7
    else if isThreadCap c
    then ->8
    else if isIRQControlCap c
    then ->9
    else if isIRQHandlerCap c
    then ->10
    else if isArchObjectCap c
    then ->11
    else if isZombie c
    then ->12
    else undefined

case \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
    if isEndpointCap cap \<and> capEPCanSend cap
    then ->1
    else if isNotificationCap cap \<and> capNtfnCanSend cap
    then ->2
    else if isReplyCap cap \<and> \<not> capReplyMaster cap
    then ->3
    else if isThreadCap cap
    then ->4
    else if isDomainCap cap
    then ->5
    else if isCNodeCap cap
    then ->6
    else if isUntypedCap cap
    then ->7
    else if isIRQControlCap cap
    then ->8
    else if isIRQHandlerCap cap
    then let irq = capIRQ cap
        in ->9
    else if isArchObjectCap cap
    then let cap = capCap cap
        in ->10
    else ->11


case \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
    if isUntypedCap a
    then ->1
    else if isEndpointCap a \<and> isEndpointCap b
    then ->2
    else if isNotificationCap a \<and> isNotificationCap b
    then ->3
    else if isCNodeCap a \<and> isCNodeCap b
    then ->4
    else if isThreadCap a \<and> isThreadCap b
    then ->5
    else if isReplyCap a \<and> isReplyCap b
    then ->6
    else if isDomainCap a \<and> isDomainCap b
    then ->7
    else if isIRQControlCap a \<and> isIRQControlCap b
    then ->8
    else if isIRQControlCap a \<and> isIRQHandlerCap b
    then ->9
    else if isIRQHandlerCap a \<and> isIRQHandlerCap b
    then (case (a, b) of
        (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->10
        )
    else if isArchObjectCap a \<and> isArchObjectCap b
    then (case (a, b) of
        (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->11
        )
    else ->12

case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
    if isPageDirectoryCap cap
    then ->1
    else if isPageTableCap cap
    then ->2
    else if isPageCap cap
    then ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then ->5
    else undefined

case \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
    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
    then ->1
    else if isPageTableCap c \<and> capPTMappedAddress c = None
    then ->2
    else if isPageDirectoryCap c \<and> capPDMappedAddress c \<noteq> None
    then ->3
    else if isPageDirectoryCap c \<and> capPDMappedAddress c = None
    then ->4
    else if isPDPointerTableCap c \<and> capPDPTMappedAddress c \<noteq> None
    then ->5
    else if isPDPointerTableCap c \<and> capPDPTMappedAddress c = None
    then ->6
    else if isPML4Cap c \<and> capPML4MappedASID c \<noteq> None
    then ->7
    else if isPML4Cap c \<and> capPML4MappedASID c = None
    then ->8
    else if isPageCap c
    then ->9
    else if isASIDControlCap c
    then ->10
    else if isASIDPoolCap c
    then ->11
    else if isIOPortCap c
    then ->12
    else if isIOPortControlCap c
    then ->13
    else undefined

case \x of (c@IOPortCap {}) -> c ->  ---> let c = \x in
   if isIOPortCap c
   then ->1
   else ->2

case \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
    if isPageCap cap
    then ->1
    else if isPageTableCap cap
    then let ptr = capPTBasePtr cap
        in ->2
    else if isPageDirectoryCap cap
    then let ptr = capPDBasePtr cap
        in ->3
    else if isPDPointerTableCap cap
    then let ptr = capPDPTBasePtr cap
        in ->4
    else if isPML4Cap cap
    then let ptr = capPML4BasePtr cap
        in ->5
    else if isIOPortCap cap
    then ->6
    else if isIOSpaceCap cap
    then ->7
    else if isIOPageTableCap cap
    then let ptr = capIOPTBasePtr cap
        in ->8
    else if isASIDControlCap cap
    then ->9
    else if isASIDPoolCap cap
    then let base = capASIDBase cap; ptr = capASIDPool cap
        in ->10
    else undefined

case \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
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC,
        index#depth#ioapic#pin#level#polarity#irqW#_, cnode#_) => ->1
    | (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, _, _) => ->2
    | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI,
        index#depth#pciBus#pciDev#pciFunc#handle#irqW#_, cnode#_) => ->3
    | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, _, _) => ->4
    | _ => ->5

case \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
    case inv of
      (IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic pin level polarity vector) => ->1
    | (IssueIRQHandlerMSI irq destSlot srcSlot pciBus pciDev pciFunc handle) => ->2

case \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
    if isPageCap cap
    then ->1
    else if isPageTableCap cap
    then let ptr = capPTBasePtr cap in ->2
    else if isPageDirectoryCap cap
    then let ptr = capPDBasePtr cap in ->3
    else if isPDPointerTableCap cap
    then let ptr = capPDPTBasePtr cap in ->4
    else if isPML4Cap cap
    then let ptr = capPML4BasePtr cap in ->5
    else if isIOPortCap cap
    then ->6
    else if isIOSpaceCap cap
    then ->7
    else if isIOPageTableCap cap
    then let ptr = capIOPTBasePtr cap in ->8
    else if isASIDControlCap cap
    then ->9
    else if isASIDPoolCap cap
    then let base = capASIDBase cap; ptr = capASIDPool cap in ->10
    else undefined

case \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
    case t of
     APIObjectType _ => ->1
   | SmallPageObject => ->2
   | LargePageObject => ->3
   | HugePageObject => ->4
   | PageTableObject => ->5
   | PageDirectoryObject => ->6
   | PDPointerTableObject => ->7
   | PML4Object => ->8

case \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
    if isPageCap a \<and> isPageCap b
    then ->1
    else if isPageTableCap a \<and> isPageTableCap b
    then ->2
    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
    then ->3
    else if isPDPointerTableCap a \<and> isPDPointerTableCap b
    then ->4
    else if isPML4Cap a \<and> isPML4Cap b
    then ->5
    else if isASIDControlCap a \<and> isASIDControlCap b
    then ->6
    else if isASIDPoolCap a \<and> isASIDPoolCap b
    then ->7
    else if isIOPortCap a \<and> isIOPortCap b
    then ->8
    else if isIOPortControlCap a \<and> isIOPortControlCap b
    then ->9
    else if isIOPortControlCap a \<and> isIOPortCap b
    then ->10
    else ->11


case \x of (oper@(InvokeIOPort _)) -> (oper@(InvokeIOPortControl _)) -> oper ->  ---> let oper = \x in
    case oper of
      InvokeIOPort _ => ->1
    | InvokeIOPortControl _ => ->2
    | _ => ->3

case \x of (cap@PageCap {}) -> _ ->  ---> let cap = \x in
    if isPageCap cap
    then ->1
    else ->2

case \x of (ArchInvocationLabel X64IOPortControlIssue, f:l:index:depth:_, cnode:_) -> (ArchInvocationLabel X64IOPortControlIssue, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64IOPortControlIssue, f#l#index#depth#_, cnode#_) => ->1
    | (ArchInvocationLabel X64IOPortControlIssue, _, _) => ->2
    | _ => ->3

case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1
    | (ArchInvocationLabel X64PDPTMap, _, _) => ->2
    | (ArchInvocationLabel X64PDPTUnmap, _, _) => ->3
    | _ => ->4

case \x of (ArchInvocationLabel X64PageDirectoryMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64PageDirectoryMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1
    | (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2
    | (ArchInvocationLabel X64PageDirectoryUnmap, _, _) => ->3
    | _ => ->4

case \x of (ArchInvocationLabel X64PageTableMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageTableMap, _, _) -> (ArchInvocationLabel X64PageTableUnmap, _, _) -> _ ->  --->let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64PageTableMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1
    | (ArchInvocationLabel X64PageTableMap, _, _) => ->2
    | (ArchInvocationLabel X64PageTableUnmap, _, _) => ->3
    | _ => ->4


case \x of (ArchInvocationLabel X64ASIDControlMakePool, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (ArchInvocationLabel X64ASIDControlMakePool, _, _) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel X64ASIDControlMakePool, index#depth#_, (untyped,parentSlot)#(croot,_):_) => ->1
    | (ArchInvocationLabel X64ASIDControlMakePool, _, _) => ->2
    | _ => ->3

case \x of (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot):_) -> (ArchInvocationLabel X64ASIDPoolAssign, _) -> _ ->  ---> let (label, extraCaps) = \x in
    case (label, extraCaps) of
      (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot)#_) => ->1
    | (ArchInvocationLabel X64ASIDPoolAssign, _) => ->2
    | _ => ->3

case \x of cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> _ ->  ---> let cap = \x in
    if isPDPointerTableCap cap
    then ->1
    else if isPageDirectoryCap cap
    then ->2
    else if isPageTableCap cap
    then ->3
    else if isPageCap cap
    then ->4
    else if isASIDPoolCap cap
    then ->5
    else ->6

case \x of (cap@(IOPortCap { capIOPortFirstPort = first_allowed, capIOPortLastPort = last_allowed })) -> _ ->  ---> let cap = \x in
    if isIOPortCap cap
    then let first_allowed = capIOPortFirstPort cap; last_allowed = capIOPortLastPort cap in ->1
    else ->2

case \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
    case (label, args) of
      (ArchInvocationLabel X64IOPortIn8, port'#_) => ->1
    | (ArchInvocationLabel X64IOPortIn8, _) => ->2
    | (ArchInvocationLabel X64IOPortIn16, port'#_) => ->3
    | (ArchInvocationLabel X64IOPortIn16, _) => ->4
    | (ArchInvocationLabel X64IOPortIn32, port'#_) => ->5
    | (ArchInvocationLabel X64IOPortIn32, _) => ->6
    | (ArchInvocationLabel X64IOPortOut8, port'#out:_) => ->7
    | (ArchInvocationLabel X64IOPortOut8, _) => ->8
    | (ArchInvocationLabel X64IOPortOut16, port'#out#_) => ->9
    | (ArchInvocationLabel X64IOPortOut16, _) => ->10
    | (ArchInvocationLabel X64IOPortOut32, port'#out#_) => ->11
    | (ArchInvocationLabel X64IOPortOut32, _) => ->12
    | _ => ->13

case \x of cap@(IOPortCap {}) -> _ ->  ---> let cap = \x in
    if isIOPortCap cap
    then ->1
    else ->2

case \x of cap@(IOPortCap {}) -> IOPortControlCap -> _ ->  ---> let cap = \x in
    if isIOPortCap cap
    then ->1
    else if isIOPortControlCap cap
    then ->2
    else ->3

case \x of cap@(CNodeCap {}) -> cap@(ThreadCap {}) -> cap@(Zombie {}) -> _ ->  ---> let cap = \x in
    if isCNodeCap cap
    then ->1
    else if isThreadCap cap
    then ->2
    else if isZombie cap
    then ->3
    else ->4

case \x of ArchInv.IOPortIn8 -> ArchInv.IOPortIn16 -> ArchInv.IOPortIn32 -> ArchInv.IOPortOut8 w -> ArchInv.IOPortOut16 w -> ArchInv.IOPortOut32 w ->  ---> let port_data = \x in
    case port_data of
      IOPortIn8 => ->1
    | IOPortIn16 => ->2
    | IOPortIn32 => ->3
    | IOPortOut8 w => ->4
    | IOPortOut16 w => ->5
    | IOPortOut32 w => ->6

case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageMap, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> (ArchInvocationLabel X64PageGetAddress, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
    case (ilabel, args, extraCaps) of
     (ArchInvocationLabel X64PageMap, vaddr#rightsMask#attr#_, (vspaceCap, _)#_) => ->1
   | (ArchInvocationLabel X64PageMap, _, _) => ->2
   | (ArchInvocationLabel X64PageUnmap, _, _) => ->3
   | (ArchInvocationLabel X64PageGetAddress, _, _) => ->4
   | _ => ->5

case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
    case (ilabel, args, extraCaps) of
      (ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1
    | (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2
    | (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3
    | _ => ->4

case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ ->  ---> let (ilabel, args, extraCaps) = \x in
    case (ilabel, args, extraCaps) of
      (ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1
    | (ArchInvocationLabel X64PageMapIO, _, _) => ->2
    | (ArchInvocationLabel X64PageUnmap, _, _) => ->3
    | _ => ->4

case \x of cap@(PDPointerTableCap {}) -> _ ->  ---> let cap = \x in
  if isPDPointerTableCap cap
  then ->1
  else ->2

case \x of cap@(PageDirectoryCap {}) -> _ ->  ---> let cap = \x in
  if isPageDirectoryCap cap
  then ->1
  else ->2

case \x of cap@(PageTableCap {}) -> _ ->  ---> let cap = \x in
  if isPageTableCap cap
   then ->1
   else ->2

case \x of cap@(ASIDPoolCap {}) -> _ ->  ---> let cap = \x in
  if isASIDPoolCap cap
  then ->1
  else ->2

case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> cap@(IOPageTableCap {}) -> cap@(PML4Cap {}) -> _ ->  --->  let cap = \x in
  if isPageCap cap
  then ->1
  else if isPDPointerTableCap cap
  then ->2
  else if isPageDirectoryCap cap
  then ->3
  else if isPageTableCap cap
  then ->4
  else if isASIDControlCap cap
  then ->5
  else if isASIDPoolCap cap
  then ->6
  else if isIOPageTableCap cap
  then ->7
  else if isPML4Cap cap
  then ->8
  else ->9

case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (PML4Cap {}) -> _ ->  ---> let cap = \x in
  if isPageCap cap
  then ->1
  else if isPDPointerTableCap cap
  then ->2
  else if isPageDirectoryCap cap
  then ->3
  else if isPageTableCap cap
  then ->4
  else if isASIDControlCap cap
  then ->5
  else if isASIDPoolCap cap
  then ->6
  else if isPML4Cap cap
  then ->7
  else ->8


case \x of cap@(IOPageTableCap {}) -> _ ->  ---> let cap = \x in
  if isIOPageTableCap
  then ->1
  else ->2

case \x of (cap@UntypedCap {}) -> _ ->  ---> let cap = \x in
  if isUntypedCap cap
  then ->1
  else ->2

case \x of cap@(PageCap {}) -> _ ->  ---> let cap = \x in
  if isPageCap cap
  then ->1
  else ->2

case \x of (PageMap asid cap ctSlot entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) ->  ---> let \v0\ = \x in
    case \v0\ of
      PageMap asid cap ct ctSlot entries => ->1
    | PageUnmap cap ctSlot => ->2
    | PageIOMap cap cptr ctdpte slot => ->3
    | PageIOUnmap (ArchObjectCap cap) ctSlot =>
        if isPageCap cap
        then ->4
        else ->5
    | PageIOUnmap _ _ => ->5
    | PageGetAddr ptr => ->6

case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool
    then ->1
    else ->2

case \x of (cap@IOPageTableCap {}) -> _ ->  ---> let cap = \x in
  if isIOPageTableCap cap
  then ->1
  else ->2

case \x of cap@(PageCap {}) -> _ ->  ---> let cap = \x in
  if isPageCap cap
  then ->1
  else ->2

case \x of (PageMap asid cap ctSlot entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) ->  ---> let \v0\ = \x in
    case \v0\ of
      PageMap asid cap ct ctSlot entries => ->1
    | PageUnmap cap ctSlot => ->2
    | PageIOMap cap cptr ctdpte slot => ->3
    | PageIOUnmap (ArchObjectCap cap) ctSlot =>
        if isPageCap cap
        then ->4
        else ->5
    | PageIOUnmap _ _ => ->5
    | PageGetAddr ptr => ->6

case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool
    then ->1
    else ->2

case \x of (cap@IOPageTableCap {}) -> _ ->  ---> let cap = \x in
  if isIOPageTableCap cap
  then ->1
  else ->2

case \x of (X64NoHypFaults) -> ---> let hyp = \x in
  case hyp of X64NoHypFaults => ->1

case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (IOPortControlCap, (IOPortCap {})) -> (a, b) ->  ---> let (a, b) = \x in
    if isPageCap a \<and> isPageCap b
    then let ptrA = capVPBasePtr a
        in ->1
    else if isIOPortControlCap a \<and> isIOPortCap b
    then -> 2
    else ->3




case \x of cap@(VCPUCap {}) -> _ ->  ---> let cap = \x in
   if isVCPUCap cap then -> 1
   else ->2

case \x of ((field:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
   if isVCPUCap cap \<and> length ls > 0
   then let field = ls !! 0 in ->1
   else ->2

case \x of ((field:val:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
   if isVCPUCap cap \<and> length ls > 1
   then let field = ls !! 0; val = ls !! 1
       in ->1
   else ->2

case \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
    if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
    then ->1
    else if isPageTableCap c \<and> capPTMappedAddress c = None
    then ->2
    else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None
    then ->3
    else if isPageDirectoryCap c \<and> capPDMappedASID c = None
    then ->4
    else if isPageCap c
    then ->5
    else if isASIDControlCap c
    then ->6
    else if isASIDPoolCap c
    then ->7
    else if isVCPUCap c
    then ->8
    else undefined

case \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
    if isASIDPoolCap cap \<and> bl
    then let b = capASIDBase cap; ptr = capASIDPool cap
         in ->1
    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
         in ->2
    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
         in ->3
    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap in ->4
    else if isVCPUCap cap then ->5
    else ->6


case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (VCPUCap {}) ->  ---> let cap = \x in
    if isPageCap cap
    then ->1
    else if isPageTableCap cap
    then let ptr = capPTBasePtr cap
        in ->2
    else if isPageDirectoryCap cap
    then let ptr = capPDBasePtr cap
        in ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then let base = capASIDBase cap; ptr = capASIDPool cap
        in ->5
    else if isVCPUCap cap
    then ->6
    else undefined

case \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
    if isPageCap a \<and> isPageCap b
    then ->1
    else if isPageTableCap a \<and> isPageTableCap b
    then ->2
    else if isPageDirectoryCap a \<and> isPageDirectoryCap b
    then ->3
    else if isASIDControlCap a \<and> isASIDControlCap b
    then ->4
    else if isASIDPoolCap a \<and> isASIDPoolCap b
    then ->5
    else if isVCPUCap a \<and> isVCPUCap b
    then ->6
    else ->7

case \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
 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

case \x of ArchInv.InvokeVCPU iv -> _ ->  ---> let inv = \x
     in case inv of InvokeVCPU iv \<Rightarrow> ->1 | _ \<Rightarrow> ->2

case \x of ((mr0:mr1:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
   if isVCPUCap cap \<and> length ls > 1
   then let mr0 = ls !! 0; mr1 = ls !! 1
       in ->1
   else ->2

case \x of ((mr0:_), cap@(VCPUCap {})) -> (_, _) ->  ---> let (ls, cap) = \x in
   if isVCPUCap cap \<and> length ls > 0
   then let mr0 = ls !! 0
        in ->1
   else ->2

case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->   ---> let cap = \x in
    if isPageDirectoryCap cap
    then ->1
    else if isPageTableCap cap
    then ->2
    else if isPageCap cap
    then ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then ->5
    else if isVCPUCap cap
    then ->6
    else undefined

case \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
    if isASIDPoolCap cap \<and> bl
    then let b = capASIDBase cap; ptr = capASIDPool cap
         in ->1
    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
         in ->2
    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
         in ->3
    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
         in ->4
    else if isVCPUCap cap \<and> bl
    then let vcpu = capVCPUPtr cap
         in ->5
    else ->6


case \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
    if isPageCap cap
    then ->1
    else if isPageTableCap cap
    then let ptr = capPTBasePtr cap
        in ->2
    else if isPageDirectoryCap cap
    then let ptr = capPDBasePtr cap
        in ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then let base = capASIDBase cap; ptr = capASIDPool cap
        in ->5
    else if isVCPUCap cap
    then let vcpu = capVCPUPtr cap
        in ->6
    else undefined


case \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
    if isASIDPoolCap cap \<and> bl
    then let b = capASIDBase cap; ptr = capASIDPool cap
         in ->1
    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
         in ->2
    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
         in ->3
    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
         in ->4
    else if isVCPUCap cap \<and> bl
    then let vcpu = capVCPUPtr cap
         in ->5
    else ->6

case \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
    if isASIDPoolCap cap \<and> bl
    then let b = capASIDBase cap; ptr = capASIDPool cap
         in ->1
    else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None
    then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap
         in ->2
    else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None
    then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap
         in ->3
    else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None
    then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap
         in ->4
    else ->5

case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->   ---> let cap = \x in
    if isPageDirectoryCap cap
    then ->1
    else if isPageTableCap cap
    then ->2
    else if isPageCap cap
    then ->3
    else if isASIDControlCap cap
    then ->4
    else if isASIDPoolCap cap
    then ->5
    else if isVCPUCap cap
    then ->6
    else undefined

case \x of UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> _ ->  ---> let \v0\ = \x in
    if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool \<and> \<not> capIsDevice \v0\
    then ->1
    else ->2

case \x of UntypedCap {capIsDevice = False} | capBlockSize untyped == objBits pool -> _ ->  ---> if isUntypedCap \x \<and> (\<not> capIsDevice \x) \<and> (capBlockSize \x = objBits pool)
    then ->1
    else ->2

case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@FrameCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) ->  ---> let c = \x in
  if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
  then ->1
  else if isPageTableCap c \<and> capPTMappedAddress c = None
  then ->2
  else if isFrameCap c
  then ->3
  else if c = ASIDControlCap
  then ->4
  else if isASIDPoolCap c
  then ->5
  else undefined

case \x of c@(FrameCap {}) -> c ->  ---> let c = \x in
  if isFrameCap c
  then ->1
  else ->2

case \x of ((a@FrameCap {}), (b@FrameCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) ->  ---> let (a,b) = \x in
  if isFrameCap a \<and> isFrameCap b
  then ->1
  else if isPageTableCap a \<and> isPageTableCap b
  then ->2
  else if a = ASIDControlCap \<and> b = ASIDControlCap
  then ->3
  else if isASIDPoolCap a \<and> isASIDPoolCap b
  then ->4
  else ->5

case \x of ((a@FrameCap { capFBasePtr = ptrA }), (b@FrameCap {})) -> (a, b) ->  ---> let (a, b) = \x in
    if isFrameCap a \<and> isFrameCap b
    then let ptrA = capFBasePtr a in ->1
    else ->2

case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject ->  ---> let t = \x in
    case t of
     APIObjectType _ => ->1
   | SmallPageObject => ->2
   | LargePageObject => ->3
   | HugePageObject => ->4
   | PageTableObject => ->5

case \x of (cap@FrameCap {}) -> _ ->  ---> let cap = \x in
  if isFrameCap cap
  then ->1
  else ->2

case \x of cap@(FrameCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) ->  ---> let cap = \x in
  if isFrameCap cap
  then ->1
  else if isPageTableCap cap
  then ->2
  else if isASIDControlCap cap
  then ->3
  else if isASIDPoolCap cap
  then ->4
  else undefined

case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler,_,_) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel ARMIRQIssueIRQHandler,
        irqW#triggerW#index#depth#_, cnode#_) => ->1
    | (ArchInvocationLabel ARMIRQIssueIRQHandler, _, _) => ->2
    | _ => ->3

case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger,_,_) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel ARMIRQIssueIRQHandlerTrigger,
        irqW#triggerW#index#depth#_, cnode#_) => ->1
    | (ArchInvocationLabel ARMIRQIssueIRQHandlerTrigger, _, _) => ->2
    | _ => ->3

case \x of (ArchInv.IssueIRQHandler (IRQ irq) destSlot srcSlot trigger) ->  ---> case \x of
  IssueIRQHandler irq destSlot srcSlot trigger => ->1

case \x of EndpointCap { capEPCanSend = True, capEPCanGrant = canGrant, capEPCanGrantReply = canGrantReply } | (canGrant || canGrantReply) -> _ ->  ---> case \x of
  EndpointCap epptr _ True _ canGrant canGrantReply =>
     if canGrant \<or> canGrantReply then ->1
     else ->2
  | _ => ->2

case \x of 0 -> level ->  ---> case \x of
    0 => \1
  | Suc level' => (%level. \2) (Suc level')

case \x of (ArchInvocationLabel ArchLabels.RISCVIRQIssueIRQHandler, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.RISCVIRQIssueIRQHandler,_,_) -> _ ->  ---> let (label, args, extraCaps) = \x in
    case (label, args, extraCaps) of
      (ArchInvocationLabel RISCVIRQIssueIRQHandler,
        irqW#triggerW#index#depth#_, cnode#_) => ->1
    | (ArchInvocationLabel RISCVIRQIssueIRQHandler, _, _) => ->2
    | _ => ->3

case \x of ((a@FrameCap {}), (b@FrameCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@VCPUCap {}), (b@VCPUCap {})) -> (_, _) ->  ---> let (a,b) = \x in
  if isFrameCap a \<and> isFrameCap b
  then ->1
  else if isPageTableCap a \<and> isPageTableCap b
  then ->2
  else if a = ASIDControlCap \<and> b = ASIDControlCap
  then ->3
  else if isASIDPoolCap a \<and> isASIDPoolCap b
  then ->4
  else if isVCPUCap a \<and> isVCPUCap b
  then ->5
  else ->6

case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@FrameCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@VCPUCap {}) ->  ---> let c = \x in
  if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
  then ->1
  else if isPageTableCap c \<and> capPTMappedAddress c = None
  then ->2
  else if isFrameCap c
  then ->3
  else if c = ASIDControlCap
  then ->4
  else if isASIDPoolCap c
  then ->5
  else if isVCPUCap c
  then ->6
  else undefined

case \x of cap@(PageTableCap { capPTType = VSRootPT_T }) -> _ ->  ---> let cap = \x in
  if isPageTableCap cap \<and> capPTType cap = VSRootPT_T
  then ->1
  else ->2

case \x of cap@(FrameCap {}) -> cap@(PageTableCap { capPTType = NormalPT_T }) -> cap@(PageTableCap { capPTType = VSRootPT_T }) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->  ---> let cap = \x in
  if isFrameCap cap
  then ->1
  else if isPageTableCap cap \<and> capPTType cap = NormalPT_T
  then ->2
  else if isPageTableCap cap \<and> capPTType cap = VSRootPT_T
  then ->3
  else if isASIDControlCap cap
  then ->4
  else if isASIDPoolCap cap
  then ->5
  else if isVCPUCap cap
  then ->6
  else undefined

case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> Arch.Types.VSpaceObject -> Arch.Types.VCPUObject ->  ---> case \x of
    APIObjectType \v0\ \<Rightarrow> ->1
  | SmallPageObject \<Rightarrow> ->2
  | LargePageObject \<Rightarrow> ->3
  | HugePageObject \<Rightarrow> ->4
  | PageTableObject \<Rightarrow> ->5
  | VSpaceObject \<Rightarrow> ->6
  | VCPUObject \<Rightarrow> ->7