---------------------- MODULE CommittedCompositionMC ----------------------
EXTENDS ConnectedTimingMC, AdditionalContracts, SpecimenFactsB
                                                                          
                                                                        
                                                                           
                                                                              
                                                                                 
PJoin(base,extra) == [k \in DOMAIN base \cup DOMAIN extra |-> IF k \in DOMAIN extra THEN extra[k] ELSE base[k]]
ProtocolP == INSTANCE AbilityProceduresMC WITH q9p <- qT11
PChildDefinition == ProtocolP!ChildDefinition9p
PDefinitions == [k \in {ConditionalKey96(PChildDefinition)} |-> PChildDefinition]
PActivity == [ActivityContext9 EXCEPT !.activeRules={"AuditPaidObserve","ProtocolReactionControl"}]
PObjects == [id \in {1} |-> PJoin([ItemInspectionCardT11("SideAHand",CardFacts10["Specimen0046"].kind) EXCEPT !.card="Specimen0046"],
 [virtual |-> FALSE,properties |-> [kind |-> CardFacts10["Specimen0046"].kind],area |-> "NoValue",targetSite |-> "NoValue"])]
PPrinted == [card \in DOMAIN CardFacts10 |-> [kind |-> CardFacts10[card].kind]]
POwners == [card \in DOMAIN CardFacts10 |-> CardFacts10[card].side]
PInitialSnapshot ==
 [id |-> 1,checkpointId |-> 0,point |-> "BeforeCheckpoint",definitions |-> PDefinitions,objects |-> PObjects,
  present |-> {200},ordinaryActivity |-> [k \in DOMAIN PDefinitions |-> FALSE],cardActivity |-> EmptyT11,
  activationEpoch |-> [k \in DOMAIN PDefinitions |-> 0],activationSerial |-> 0,activity |-> PActivity,
  points |-> ZeroCountsT11,progress |-> EmptyT11,link |-> ZeroCountsT11,exposureMarkers |-> ZeroCountsT11,
  objectiveCompletionEvents |-> {},usedObjects |-> {},holds |-> EmptyT11,effects |-> EmptyT11]
PInitial(amount,moves) == PJoin([IInitialT11 EXCEPT !.objects=PObjects],
 [amount |-> amount,moves |-> moves,wallet |-> ItemInspectionWalletInitialT11,paid |-> EmptyT11,plan |-> EmptyT11,
  child |-> EmptyT11,childPlan |-> EmptyT11,uses |-> EmptyT11,turnUses |-> EmptyT11,useEvents |-> <<>>,
  native |-> EmptyT11,ledger |-> NewConditionalLedger96(PInitialSnapshot),registry |-> NewLingeringRegistry910,
  frames |-> EmptyT11,sites |-> {},checkpointEvents |-> EmptyT11,currentCP |-> 0,costCP |-> 0,cpResume |-> "NoValue",cpRole |-> "NoValue",
  childReturned |-> FALSE,work |-> <<>>,announcement |-> EmptyT11,paidReturned |-> FALSE,
  checkpointHistory |-> <<>>,childWindow |-> 900])
CONSTANTS PaidAmounts,PaidMoves
PInit == guideCaseT11=0 /\ \E amount \in PaidAmounts,moves \in PaidMoves : qT11=PInitial(amount,moves)
PItemInspectionView(q) == [itemInspection |-> IAT11(q),objects |-> q.objects,NeutralValue00013 |-> IF q.amount=0 THEN "FacilityObserve0" ELSE "FacilityObserve1",turnUses |-> q.turnUses]
PPaidDefinition(q) == ItemInspectionPaidDefinitionT11(PItemInspectionView(q))
PContext(q,d) == [ItemInspectionPaidContextT11(PItemInspectionView(q),d) EXCEPT !.turn=q.flow.turn,!.traversal=q.control.traversal,!.traversalControl=q.control,!.layout=q.layout]
PLegality(w,option,transaction) == [LegalityT11(w,option) EXCEPT !.transactionId=transaction]
PMid(q) == ItemInspectionTemporalMidT11(PItemInspectionView(q))
PPaidOption(q,w,d) == ItemInspectionPaidOptionT11(PItemInspectionView(q),w,d)
PUse(p) == ItemInspectionPaidUseT11(p)
PTurnUses(p) == ItemInspectionPaidTurnUsesT11(p)
                                                                            
                                                                                 
PChildTurnUses(q) == [id \in {u \in DOMAIN q.turnUses : q.turnUses[u].source=PChildDefinition.syntax.source} |-> q.turnUses[id]]
PCurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 [SnapshotWithConditionalRegistry96(q.ledger.lastSnapshot,ledger) EXCEPT !.objects=objects,!.id=id,!.point=point,!.checkpointId=checkpoint]
PWorld(q,f) == [id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,present |-> PInitialSnapshot.present,
 activity |-> [PActivity EXCEPT !.instances=ConditionalActivityRows96(q.ledger.instances)]]
PLex(d) == [tag |-> "NormalizedAbilityLexemes",definition |-> d,source |-> d.syntax.source,card |-> "NoValue",
 sourceSHA |-> "0186148ecd6da8170b6555aa90d3f0115a8d5150d807078b75ac2339a2a1421e",mentions |-> EmptyT11,
 origin |-> [tag |-> "AbilityTextOrigin",recipientSource |-> d.syntax.source,provider |-> d.activity.provider,rule |-> d.syntax.source.rule]]
PLexemes == [k \in DOMAIN PDefinitions |-> PLex(PDefinitions[k])]
PInside(q) == {TimingRef9("Turn",q.flow.turn.id),TimingRef9("SchemaAtom138",q.control.traversal.id),TimingRef9("Inspection",IBT11(q).id)} \cup
 (IF StillItemInspectioning7(IAT11(q),q.objects) THEN {TimingRef9("ItemInspection",IAT11(q).id)} ELSE {})
PFrame(q) == q.frames[q.currentCP]
PSetFrame(q,f) == [q EXCEPT !.frames[f.id]=f]
PCPOccurrences(q) ==
 LET u==q.useEvents[1] IN
 [id \in {u.useId} |-> [id |-> id,kind |-> u.tag,object |-> u.source.object,actor |-> u.player,side |-> u.player,
  snapshot |-> q.ledger.lastSnapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(PChildDefinition),
  traversal |-> q.control.traversal,structure |-> TimingRef9("ItemInspection",IAT11(q).id),actualEvent |-> u,
  transaction |-> q.native.transaction,abilityInstance |-> u.abilityInstance,source |-> u.source,turnId |-> q.paid.turnId]]
PCPData(q,f) ==
 LET b==PCurrentSnapshot(q,q.objects,q.ledger,f.snapshotId,"CheckpointBeginning",f.id)
 IN [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> f.id,previousCheckpoint |-> q.ledger.lastCheckpoint,
  serial |-> q.ledger.serial+1,previousSnapshot |-> q.ledger.lastSnapshot,beginSnapshot |-> b,
  processingSnapshot |-> [b EXCEPT !.point="ProcedureCodee605a78f5d5e"],stepSerial |-> q.ledger.stepSerial,
  occurrences |-> IF q.cpRole="Cost" THEN PCPOccurrences(q) ELSE EmptyT11,caller |-> f.caller]
POpenCP(kind,caller,resume,role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 snapshot==100+id
     event==PJoin([id |-> id,caller |-> caller,complete |-> TRUE],
       CASE kind="SchemaAtom126" -> [tag |-> "PriorityAboutToBeReceived",player |-> WindowTop9(q.stack).priority]
        [] kind="Cost" -> [tag |-> "CostPaid",transactionId |-> q.paid.transaction,nativePayment |-> q.native,useEvent |-> q.useEvents[1]]
        [] OTHER -> [tag |-> "InstructionFinished",origin |-> "Ability",instruction |-> IF role="ChildFinal" THEN "AbilityInstruction710" ELSE "AbilityInstruction700",
          instructionRef |-> InstructionWindowRef93(IF role="ChildFinal" THEN q.childPlan ELSE q.plan),
          finishedPlan |-> IF role="ChildFinal" THEN q.childPlan ELSE q.plan])
     site==[kind |-> kind,caller |-> caller,eventId |-> id,snapshotId |-> snapshot,inside |-> PInside(q)]
     frame==NewCheckpoint103(id,caller,snapshot,PInside(q))
     frames==PJoin(q.frames,[k \in {id} |-> frame])
 IN /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,frame,id,site,event,PInside(q))
    /\ (kind="Cost" => q.paid.costPaid /\ q.wallet.checkpointDue /\ Len(q.useEvents)=1)
    /\ (kind="Instruction" => IF role="ChildFinal" THEN q.childPlan.phase="Complete" ELSE q.plan.phase="Complete")
    /\ qT11'=[q EXCEPT !.frames=frames,!.sites=@ \cup {CheckpointSiteKey103(site)},!.currentCP=id,
         !.checkpointEvents=PJoin(@,[k \in {id} |-> event]),!.costCP=IF role="Cost" THEN id ELSE @,!.cpResume=resume,!.cpRole=role,!.stage="PCP"]
PCPNext(f) ==
 LET rest==SubSeq(f.owed,2,Len(f.owed)) IN
 [f EXCEPT !.owed=rest,!.done=@ \cup {f.point},!.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"]
PLegal(selected) == selected={}
PCPWork ==
 LET q==qT11 f==PFrame(q) next==PCPNext(f) world==PWorld(q,f) IN
 CASE f.point="ProcedureCodee605a78f5d5e" ->
   LET cp==PCPData(q,f) key==[definition |-> ConditionalKey96(PChildDefinition),occurrence |-> 1]
       allocation==[k \in IF q.cpRole="Cost" THEN {key} ELSE {} |-> 201]
       bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> q.childWindow,group |-> 4]]
       conditions==[k \in DOMAIN PDefinitions |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> 200,source |-> PChildDefinition.syntax.source,
          occurrence |-> id,snapshotId |-> cp.occurrences[id].snapshot.id,results |-> EmptyT11]]]
       ledger==ProtocolP!CPAfter9p(q.ledger,cp,allocation,bindings)
       after==[next EXCEPT !.recognition=cp,!.recognized=CheckpointMemberMap103(ledger,f.id)]
       x==[route |-> "Ordinary",cp |-> cp,definitions |-> PDefinitions,lexemes |-> PLexemes,conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]
   IN /\ RecognizeCheckpoint103(f,after,q.ledger,ledger,q.stack,q.stack,x)
      /\ qT11'=[PSetFrame(q,after) EXCEPT !.ledger=ledger]
 [] f.point="ProcedureCode88eda145024f" ->
   LET cursor==LingeringCheckpointFrame910(q.ledger,f.recognition,world)
       cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> cursor,expired |-> {},complete |-> TRUE]
       registry==[q.registry EXCEPT !.cleanupIds=@ \cup {f.id}]
       snapshot==SnapshotWithConditionalRegistry96(q.ledger.lastSnapshot,q.ledger)
   IN /\ CheckpointCleanupEffects103(f,next,q.registry,registry,q.ledger,q.ledger,q.ledger,q.stack,q.stack,
        snapshot,snapshot,world,cursor,[cursor EXCEPT !.returned=TRUE,!.point="ProcedureCodeb681cc249a04"],cleanup)
      /\ qT11'=[PSetFrame(q,next) EXCEPT !.registry=registry]
 [] f.point="ProcedureCodeb681cc249a04" ->
   /\ CheckpointVictory103(f,next,q.objects,[id \in DOMAIN q.objects |-> 0],f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCodefe50c31480ea" ->
   /\ CheckpointUniqueRetire103(f,next,q.objects,q.objects,[id \in DOMAIN q.objects |-> q.objects[id].card],{},{},{},
        [id \in DOMAIN q.objects |-> "SideA"],EmptyT11,EmptyT11,DOMAIN q.objects,PPrinted,POwners,{},f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCodea488e1ba6ca3" ->
   /\ CheckpointIllegalRetire103(f,next,q.objects,q.objects,{},PLegal,[id \in DOMAIN q.objects |-> "SideA"],q.flow.turn.owner,
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],[applies |-> FALSE],"NoValue",{},EmptyT11,DOMAIN q.objects,PPrinted,POwners,{},f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} ->
   /\ CheckpointHostedCleanup103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,
        IF q.paid=EmptyT11 THEN EmptyT11 ELSE [id \in {q.paid.id} |-> q.paid],EmptyT11,DOMAIN q.objects,PPrinted,POwners,{},f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCode2d73b20aa788" ->
   /\ CheckpointAuxiliarySiteCleanup103(f,next,[s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],q.objects,EmptyT11,f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCode2d6279f9d639" ->
   /\ CheckpointPositionCleanup103(f,next,q.layout,q.layout,q.control.traversal.position,EmptyT11,f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCode7f181ce21011" ->
   /\ CheckpointRootAdmissions103(f,next,q.capacity,q.capacity,IBT11(q),q.objects,EmptyT11,0,q.ledger.stepSerial,{},"SideB",f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCodeda83a77a1f12" ->
   /\ CheckpointRestoreDiscard103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,PPrinted,f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCode0811ebc5f40e" ->
   /\ CheckpointReturnDiscardCounters103(f,next,q.objects,q.objects,f.snapshotId)
   /\ qT11'=PSetFrame(q,next)
 [] f.point="ProcedureCodeb74d673a0fc6" ->
   IF DOMAIN f.recognized={} THEN
     LET returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] IN
     /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
     /\ qT11'=[PSetFrame(q,returned) EXCEPT !.stage=q.cpResume,
         !.checkpointHistory=Append(@,[id |-> f.id,role |-> q.cpRole,caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
   ELSE
     LET members==f.recognized site==WindowTop9(q.stack).site
         opening==PJoin(IOpeningT11(q.childWindow,"Reaction",site),
           [members |-> DOMAIN members,instances |-> members,group |-> 4,modifiersExist |-> FALSE,
            preparation |-> <<"ConditionsMet","PendingGroup">>,checkpointId |-> f.id,caller |-> f.caller,
            completion |-> PersistentCheckpointCompletion912(q.ledger,f.recognition,world)])
         window==NewPriorityWindow9(q.childWindow,"Reaction",site,members,4,NoTimingRef9,[id |-> 0],0)
         after==[f EXCEPT !.phase="Reaction",!.windowId=q.childWindow]
     IN /\ OpenCheckpointReaction103(f,after,q.ledger,q.stack,Append(q.stack,window),site,opening,q.usedWindows)
        /\ qT11'=[PSetFrame(q,after) EXCEPT !.stack=Append(@,window),!.usedWindows=@ \cup {q.childWindow},!.stage="PReceive"]
 [] OTHER -> FALSE
PNativeAtPayment(q,selected,after) ==
 /\ q.paid.transaction=2500 /\ q.paid.windowId=WindowTop9(q.stack).id /\ q.paid.ability.caller=q.paid.windowId
 /\ q.paid.option.target=IAT11(q).object /\ q.paid.turnId=q.flow.turn.id
 /\ q.paid.definition.triggerCost=PPaidDefinition(q).triggerCost
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.wallet,"SideB",selected,q.amount,{})
 /\ after=ItemInspectionWalletSpentT11(q.wallet,selected)
PNativeCommitted(q) ==
 /\ q.native.transaction=q.paid.transaction /\ q.native.window=q.paid.windowId /\ q.native.option=q.paid.option
 /\ q.native.source=q.paid.ability.source /\ q.native.turn=q.flow.turn.id /\ q.native.itemInspection=77 /\ q.native.siteInspection=20 /\ q.native.traversal=7
 /\ q.native.amount=q.amount /\ Cardinality(q.native.selected)=q.amount
 /\ q.native.after=ItemInspectionWalletSpentT11(q.native.before,q.native.selected)
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.native.before,"SideB",q.native.selected,q.amount,{})
 /\ q.wallet=[q.native.after EXCEPT !.checkpointDue=~q.frames[q.costCP].returned]
 /\ q.uses=ItemInspectionPaidUsesT11(q.paid) /\ q.turnUses=PTurnUses(q.paid) /\ q.useEvents= <<PUse(q.paid)>>
PPayment(q) == [tag |-> "PriorityOptionPayment",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 allTriggerCostsPaid |-> PNativeCommitted(q),costCheckpointAndReactionsDrained |-> CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack)]
PReturn(q) == [tag |-> "PriorityOptionReturn",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 triggerPayment |-> PPayment(q),allCostsPaid |-> PNativeCommitted(q),optionComplete |-> q.paid.ability.complete,
 childrenReturned |-> q.childReturned /\ q.plan.phase="Complete",reactionsDrained |-> CheckpointDrained103(q.frames[q.paid.checkpoint],q.ledger,q.stack),
 finalCheckpointId |-> q.paid.checkpoint]
PTargets(plan,targets) == [ProtocolP!Targets9p(plan) EXCEPT !.targets=targets]
PReadyCP(q) == ProtocolP!PriorityCP9p(WindowTop9(q.stack),q.currentCP)
PMidWindow ==
 LET q==qT11 w==WindowTop9(q.stack) a==IAT11(q) IN
 CASE w.stage="NeedCheckpoint" -> POpenCP("SchemaAtom126",ConditionalPriorityCaller96(w),"PMidReady","MidPriority")
 [] w.stage="Ready" ->
   LET d==PPaidDefinition(q) option==PPaidOption(q,w,d) busy==StartPriorityOptionFrame9(w,option,2500)
       p==OpenPaidProcedure95(250,d,option,w,2500,"Rule")
   IN /\ ReservePaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,busy),p,250,d,PContext(q,d),option,PLegality(w,option,2500),{},a,a,PMid(q),{PMid(q)},FALSE,FALSE)
      /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,busy),!.paid=p,!.stage="PPay"]
 [] w.stage="Closed" ->
   LET rest==SubSeq(q.stack,1,Len(q.stack)-1) IN
   /\ PopClosedPriorityWindow9(q.stack,rest)
   /\ qT11'=IRecordT11([q EXCEPT !.stack=rest],"ProcedureCode1dd0e8f05be2",{},IF a.complete THEN "ItemInspectionReturn" ELSE "ItemInspectionAdvance")
 [] OTHER -> FALSE
PProtocolWork ==
 LET q==qT11 IN
 CASE q.stage="PMidReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(PFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),PReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage="Window"]
 [] q.stage="PPay" ->
   LET p==q.paid selected==IF q.amount=0 THEN {} ELSE {100} after==ItemInspectionWalletSpentT11(q.wallet,selected)
       paid==ItemInspectionPaidCommittedFrameT11(p) a==IAT11(q) used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE]
       payment==[tag |-> "PaidTriggerPayment",abilityInstance |-> p.id,transactionId |-> p.transaction,
        ability |-> p.definition.syntax.id,source |-> p.ability.source,triggerCost |-> p.definition.triggerCost,
        beforeObjects |-> q.objects,afterObjects |-> q.objects,announced |-> TRUE,allPaid |-> PNativeAtPayment(q,selected,after),
        additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE,
        sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}]
   IN /\ PayPaidMidItemInspection95(q.stack,p,paid,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.objects,payment,
        q.uses,ItemInspectionPaidUsesT11(p),q.turnUses,PTurnUses(p),1,{PUse(p)},a,used,PMid(q),{PMid(q)},FALSE,FALSE,
        [tag |-> "MidItemInspectionBeginDrained",itemInspectionId |-> a.id,windowId |-> p.windowId,checkpointId |-> p.initialCheckpoint,
         complete |-> CheckpointDrained103(q.frames[p.initialCheckpoint],q.ledger,q.stack)],{})
      /\ qT11'=[IWithItemInspectionT11(q,used) EXCEPT !.wallet=after,!.paid=paid,!.uses=ItemInspectionPaidUsesT11(p),!.turnUses=PTurnUses(p),
        !.useEvents= <<PUse(p)>>,!.native=[before |-> q.wallet,after |-> after,selected |-> selected,amount |-> q.amount,
         transaction |-> p.transaction,window |-> p.windowId,option |-> p.option,source |-> p.ability.source,
         turn |-> q.flow.turn.id,itemInspection |-> a.id,siteInspection |-> a.siteInspectionId,traversal |-> a.traversalId],!.stage="PCostOpen"]
      /\ ItemInspectionCostOwnerT11!DoSpendResourceUnits(ItemInspectionCostCommandT11(selected,q.amount))
 [] q.stage="PCostOpen" -> POpenCP("Cost",PaidCheckpointCaller96(q.paid),"PCostResume","Cost")
 [] q.stage="PCP" -> PCPWork
 [] q.stage="PReceive" -> POpenCP("SchemaAtom126",ConditionalPriorityCaller96(WindowTop9(q.stack)),"PChildReady","ChildPriority")
 [] q.stage="PChildReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(PFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),PReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage=IF q.childReturned THEN "PPass" ELSE "PSelect"]
 [] q.stage="PSelect" ->
   LET w==WindowTop9(q.stack) d==PChildDefinition option==PriorityOption9(70,"Conditional","SideB",200,201,d.syntax.source,0,{})
       busy==StartPriorityOptionFrame9(w,option,2600) p==OpenConditionalProcedure96(201,d,w,option,2600,"Rule")
       plan==OpenInstruction93(710,"Ability",201,d.syntax.source,"Rule",1,"NoValue",<<"CostReaction">>,FALSE)
       imminent==[p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE]
       announced==[plan EXCEPT !.phase="Imminent",!.announced=TRUE] ledger==[q.ledger EXCEPT !.instances[201].status="Imminent"]
   IN /\ BeginConditionalResolution96(q.ledger,ledger,q.stack,ReplaceWindowTop9(q.stack,busy),p,imminent,d,
        SnapshotWithConditionalRegistry96(q.ledger.lastSnapshot,q.ledger),201,option,PLegality(w,option,2600),EmptyT11,plan,announced,
        PTargets(plan,{}),ProtocolP!Entry9p(plan,0),PChildTurnUses(q),
        [tag |-> "AbilityRestrictions",ability |-> 200,source |-> d.syntax.source,results |-> EmptyT11])
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.stack=ReplaceWindowTop9(@,busy),!.child=imminent,!.childPlan=announced,!.stage="PChildBegin"]
 [] q.stage="PChildBegin" ->
   LET p==[q.child EXCEPT !.phase="Resolve",!.ability.phase="Resolving"] plan==[q.childPlan EXCEPT !.phase="Resolving"]
       expected==[tag |-> "ConditionalExpectedEffects",point |-> "ExpectedEffectsBeforeInterrupt",instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]
       ledger==[q.ledger EXCEPT !.instances[201].status="Resolving",!.instances[201].expected=[i \in {1} |->
         [instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]]]
   IN /\ ResolveConditionalWithoutInterrupt96(q.ledger,ledger,q.stack,q.child,p,q.childPlan,plan,
        ProtocolP!NoModifiers9p(q.childPlan),ProtocolP!Clearance9p(q.childPlan),expected)
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.stage="PChildWork"]
 [] q.stage="PChildWork" ->
   LET objects==IF q.moves THEN ItemInspectionMovedObjectsT11(q.objects,"SideADiscard") ELSE q.objects
       a==IAT11(q) itemInspection==IF q.moves THEN ItemInspectionEndedT11(a,"Moved") ELSE a
       ability==ProtocolP!FinishedAbility9p(q.child.ability,q.childPlan)
       p==[q.child EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]
       plan==ProtocolP!FinishedPlan9p(q.childPlan) ledger==[q.ledger EXCEPT !.instances[201].status="Complete"]
       beforeSnapshot==PCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"InstructionBefore",q.ledger.lastCheckpoint)
       afterSnapshot==PCurrentSnapshot(q,objects,ledger,q.ledger.lastSnapshot.id+1000,"InstructionAfter",q.ledger.lastCheckpoint)
   IN /\ RecordConditionalExecutionUse96(q.ledger,q.ledger,q.child,q.childPlan,
        [tag |-> "ConditionalEffectExecution",instruction |-> InstructionWindowRef93(q.childPlan),abilityInstance |-> q.child.id,
         source |-> q.child.ability.source,partIds |-> {1}],q.uses,q.uses,q.turnUses,q.turnUses,2,{})
      /\ CarryConditionalInstruction96(q.ledger,ledger,ledger,q.stack,q.stack,q.child,p,q.childPlan,plan,
        ProtocolP!Step9p(q.childPlan),beforeSnapshot,afterSnapshot)
      /\ IF q.moves THEN
         /\ CardBatchTransfer8(q.objects,objects,{1},[id \in {1} |-> 2],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>])
         /\ ItemInspectionMovementOutcome7(a,itemInspection,objects,TRUE,{ItemInspectionEndEvent7(a)})
         ELSE objects=q.objects /\ itemInspection=a
      /\ qT11'=[IWithItemInspectionT11(q,itemInspection) EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.objects=objects,
        !.work=Append(@,"CostReaction"),!.rawEvents=IF q.moves THEN Append(@,{ItemInspectionEndEvent7(a)}) ELSE @,!.stage="PChildCPOpen"]
 [] q.stage="PChildCPOpen" -> POpenCP("Instruction",ConditionalInstructionCaller96(q.child),"PChildCPDone","ChildFinal")
 [] q.stage="PChildCPDone" ->
   LET p==[q.child EXCEPT !.phase="Complete",!.checkpoint=q.currentCP]
       receipt==[tag |-> "ConditionalInstructionCheckpoint",id |-> q.currentCP,abilityInstance |-> q.child.id,
        transactionId |-> q.child.transaction,source |-> q.child.ability.source,instruction |-> q.childPlan.id,index |-> 1,
        complete |-> TRUE,allNewerChainsComplete |-> TRUE]
   IN /\ ResumeConditionalInstructionAfterCheckpoint103(PFrame(q),q.ledger,q.stack,q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stage="PChildReturn"]
 [] q.stage="PChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE] w==WindowTop9(q.stack)
       receipt==ProtocolP!Return9p(w,q.child.checkpoint)
   IN /\ FinishConditionalProcedure96(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.childReturned=TRUE,!.stage="PReceive"]
 [] q.stage="PPass" ->
   LET w==WindowTop9(q.stack) after==PassPriorityFrame9(w)
       snapshot==PCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"Pass",q.ledger.lastCheckpoint)
   IN /\ PassConditionalPriority96(q.ledger,q.ledger,q.ledger,q.stack,ReplaceWindowTop9(q.stack,after),w.priority,EmptyT11,snapshot,snapshot)
      /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,after),!.stage=IF after.open THEN "PReceive" ELSE "PCostReturn"]
 [] q.stage="PCostReturn" ->
   LET f==q.frames[q.costCP] returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] rest==SubSeq(q.stack,1,Len(q.stack)-1)
   IN /\ ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,f.caller)
      /\ qT11'=[PSetFrame(q,returned) EXCEPT !.stack=rest,!.wallet.checkpointDue=FALSE,!.currentCP=q.costCP,!.stage="PCostResume",
        !.checkpointHistory=Append(@,[id |-> f.id,role |-> "Cost",caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
 [] q.stage="PCostResume" ->
   LET p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP] IN
   /\ ResumePaidAfterCheckpoint103(q.frames[q.costCP],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stage="PTargets"]
 [] q.stage="PTargets" ->
   LET p==q.paid plan==ItemInspectionPaidPlanT11(p) targets==IF 1 \in DOMAIN q.objects THEN {1} ELSE {}
       afterPlan==[plan EXCEPT !.targets=targets,!.announced=TRUE,!.phase="Imminent"]
       imminent==[p EXCEPT !.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.phase="Imminent",!.checkpoint=0]
   IN /\ EnterPaidInstruction95(q.stack,p,imminent,plan,afterPlan,PTargets(plan,targets),ItemInspectionPaidEntryT11(plan,p.checkpoint))
      /\ qT11'=[q EXCEPT !.paid=imminent,!.plan=afterPlan,!.announcement=[objects |-> q.objects,targets |-> targets,
        instruction |-> InstructionWindowRef93(afterPlan),costCheckpoint |-> q.costCP,child |-> q.child,turn |-> q.flow.turn.id],!.stage="PBegin"]
 [] q.stage="PBegin" ->
   LET p==[q.paid EXCEPT !.ability.phase="Resolving",!.phase="Resolve"] plan==[q.plan EXCEPT !.phase="Resolving"] IN
   /\ ResolvePaidWithoutInterrupt95(q.stack,q.paid,p,q.plan,plan,ItemInspectionPaidNoModifiersT11(q.plan),ItemInspectionPaidInterruptReturnT11(q.plan))
   /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.stage="PBody"]
 [] q.stage="PBody" ->
   LET plan==q.plan after==[plan EXCEPT !.completedSteps=Append(@,"MidEffect"),!.cursor=2] IN
   /\ q.announcement.objects=q.objects /\ plan.targets=q.announcement.targets
   /\ CarryPaidInstruction95(q.stack,q.paid,q.paid,plan,after,ProtocolP!Step9p(plan))
   /\ qT11'=[q EXCEPT !.plan=after,!.work=Append(@,"MidEffect"),!.stage="PTail"]
 [] q.stage="PTail" ->
   LET plan==ProtocolP!FinishedPlan9p(q.plan) ability==ProtocolP!FinishedAbility9p(q.paid.ability,q.plan)
       p==[q.paid EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]
   IN /\ CarryPaidInstruction95(q.stack,q.paid,p,q.plan,plan,ProtocolP!Step9p(q.plan))
      /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.work=Append(@,"MidTail"),!.stage="PFinalOpen"]
 [] q.stage="PFinalOpen" -> POpenCP("Instruction",PaidCheckpointCaller96(q.paid),"PFinalDone","PaidFinal")
 [] q.stage="PFinalDone" ->
   LET p==[q.paid EXCEPT !.phase="Complete",!.checkpoint=q.currentCP] IN
   /\ ResumePaidAfterCheckpoint103(PFrame(q),q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.currentCP,TRUE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stage="PFinish"]
 [] q.stage="PFinish" ->
   LET a==IAT11(q) itemInspection==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE]
       paid==[q.paid EXCEPT !.ability.returned=TRUE,!.phase="Returned"] w==WindowTop9(q.stack)
   IN /\ FinishPaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),q.paid,paid,PReturn(q),a,itemInspection)
      /\ qT11'=[IWithItemInspectionT11(q,itemInspection) EXCEPT !.paid=paid,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.paidReturned=TRUE,!.stage="Window"]
 [] OTHER -> FALSE
PWork ==
 /\ UNCHANGED guideCaseT11
 /\ IF qT11.stage="Window" /\ qT11.windowRole="Mid" THEN PMidWindow
    ELSE IF qT11.stage \in {"PMidReady","PPay","PCostOpen","PCP","PReceive","PChildReady","PSelect","PChildBegin","PChildWork",
      "PChildCPOpen","PChildCPDone","PChildReturn","PPass","PCostReturn","PCostResume","PTargets","PBegin","PBody","PTail","PFinalOpen","PFinalDone","PFinish"}
      THEN PProtocolWork ELSE IConnectedStepT11
PSpec == PInit /\ [][PWork]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(PWork)
PEventuallyReturns == <>qT11.done
PSourceIndexChecks(q) ==
 IF q.turnUses=EmptyT11 THEN TRUE ELSE
 LET row==[turnId |-> q.flow.turn.id,ability |-> 200,source |-> PChildDefinition.syntax.source,useId |-> 2]
     same==[q EXCEPT !.turnUses=PJoin(@,[id \in {2} |-> row])]
     flagged==[PChildDefinition.syntax EXCEPT !.units=Append(@,TextUnit93(99,"AbilityFlag","OncePerTurn",FALSE,0))]
 IN /\ PChildTurnUses(q)=EmptyT11
    /\ PChildTurnUses(same)=[id \in {2} |-> row]
    /\ OncePerTurnAllowed93(flagged,q.flow.turn.id,PChildTurnUses(q))
    /\ ~OncePerTurnAllowed93(flagged,q.flow.turn.id,PChildTurnUses(same))
PGuardChecks(q) ==
 /\ (Len(q.stack)=3 =>
    LET p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP] IN
    /\ (WindowTop9(q.stack).open => ~ConditionalCheckpointDrained96(q.ledger,q.stack,q.costCP))
    /\ ~ResumePaidAfterCheckpoint103(q.frames[q.costCP],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE)))
 /\ (q.stage="PCostResume" =>
    LET f==q.frames[q.costCP] p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP]
        receipt==ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE) IN
    /\ ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103([f EXCEPT !.caller.transactionId=2501],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,[q.paid EXCEPT !.transaction=2501],p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,[receipt EXCEPT !.id=1]))
 /\ (q.stage="PCostReturn" =>
    LET f==q.frames[q.costCP] returned==[f EXCEPT !.phase="Returned",!.returned=TRUE]
        rest==SubSeq(q.stack,1,Len(q.stack)-1) IN
    /\ ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,f.caller)
    /\ ~ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,[f.caller EXCEPT !.transactionId=2501])
    /\ ~ReturnCheckpointAfterReaction103(f,returned,q.ledger,ReplaceWindowTop9(q.stack,[WindowTop9(q.stack) EXCEPT !.id=901]),rest,f.caller))
 /\ (q.stage="PFinish" =>
    LET a==IAT11(q) itemInspection==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE]
        paid==[q.paid EXCEPT !.ability.returned=TRUE,!.phase="Returned"]
        stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
    /\ FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,PReturn(q),a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[PReturn(q) EXCEPT !.finalCheckpointId=1],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[PReturn(q) EXCEPT !.childrenReturned=FALSE],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[PReturn(q) EXCEPT !.transactionId=2501],a,itemInspection))
 /\ (q.stage="InspectionResume" =>
    /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].objects=IF q.moves THEN PObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="TraversalResume" =>
    /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].objects=IF q.moves THEN PObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="ActionResume" =>
    /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].objects=IF q.moves THEN PObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
PRecognitionChecks(q) ==
 IF q.costCP=0 THEN TRUE ELSE
 LET f==q.frames[q.costCP] IN
 IF f.recognition.id=0 THEN TRUE ELSE
 LET e==f.recognition.occurrences[1] i==q.ledger.instances[201] IN
 /\ e.actualEvent=q.useEvents[1] /\ e.source=q.paid.ability.source /\ e.transaction=q.paid.transaction
 /\ e.abilityInstance=q.paid.id /\ e.turnId=q.flow.turn.id /\ e.traversal.id=q.control.traversal.id
 /\ e.structure=TimingRef9("ItemInspection",IAT11(q).id) /\ e.actor="SideB"
 /\ i.checkpointId=q.costCP /\ i.occurrence=e.id /\ i.definitionCopy=PChildDefinition /\ i.member.windowId=q.childWindow
PCheckpointEventChecks(q) ==
 /\ DOMAIN q.checkpointEvents=DOMAIN q.frames
 /\ q.registry.cleanupIds={id \in DOMAIN q.frames : "ProcedureCode88eda145024f" \in q.frames[id].done}
 /\ \A id \in DOMAIN q.checkpointEvents :
   LET e==q.checkpointEvents[id] IN
   /\ e.id=id /\ e.caller=q.frames[id].caller /\ e.complete
   /\ (e.tag="InstructionFinished" =>
       /\ e.finishedPlan.phase="Complete" /\ e.finishedPlan.completedSteps=e.finishedPlan.steps
       /\ e.instructionRef=InstructionWindowRef93(e.finishedPlan) /\ e.instructionRef.id=e.caller.instruction
       /\ e.instruction=(IF e.instructionRef.id=710 THEN "AbilityInstruction710" ELSE "AbilityInstruction700"))
   /\ (e.tag="CostPaid" => e.transactionId=q.paid.transaction /\ e.nativePayment=q.native /\ e.useEvent=PUse(q.paid))
PExpectedTrace(q) == IF q.moves THEN SelectSeq(IntegrationOracleTrace11,LAMBDA step : step \notin {"ProcedureCode546db7cc4546","ProcedureCode662478499367"}) ELSE IntegrationOracleTrace11
PConnectedSafety ==
 LET q==qT11 IN
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal) /\ PriorityStackValid9(q.stack)
 /\ IReturnGuardChecksT11(q) /\ IActionWindowOrderT11(q) /\ PGuardChecks(q) /\ PCheckpointEventChecks(q) /\ PRecognitionChecks(q)
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(PExpectedTrace(q),1,Len(q.trace))
 /\ IEventNamesT11(q) \cap IntegrationOracleAbsent11={}
 /\ \A id \in DOMAIN q.control.itemInspections : ItemInspectionProcedureValid7(q.control.itemInspections[id],q.objects)
 /\ \A id \in DOMAIN q.control.siteInspections : InspectionProcedureValid7(q.control.siteInspections[id])
 /\ (q.action.status="Nested" => q.waitTraversal.handle=q.action.nested /\ q.waitTraversal.id=q.control.traversal.id /\ q.stack[1].busy=IActionOptionT11 /\ q.stack[1].open)
 /\ ("ItemInspection" \in q.consumed => IAT11(q).returned /\ q.paidReturned)
 /\ ("Inspection" \in q.consumed => IBT11(q).returned)
 /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done => q.trace=PExpectedTrace(q) /\ (\A name \in IntegrationOracleEvents11 : IEventCountT11(q,name)=1) /\ q.returnOrder=IntegrationOracleReturnOrder11 /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"} /\ q.action.status="Complete" /\
    q.actionPointWorld.actionPoints["SideB"]=1 /\ q.actionPointWorld.spent["SideB"]=1 /\ Len(q.stack)=1 /\ WindowTop9(q.stack).kind="NeutralValue00001" /\ WindowTop9(q.stack).stage="Ready")
PPaidSafety ==
 LET q==qT11 IN
 /\ PSourceIndexChecks(q)
 /\ q.amount \in {0,1} /\ q.moves \in BOOLEAN /\ DOMAIN q.objects \in {{1},{2}}
 /\ (q.paid#EmptyT11 /\ q.paid.costPaid =>
     /\ IAT11(q).midUsed /\ q.paid.ability.detached /\ q.paid.turnId=q.flow.turn.id
     /\ q.uses=ItemInspectionPaidUsesT11(q.paid) /\ q.turnUses=PTurnUses(q.paid) /\ q.useEvents= <<PUse(q.paid)>>
     /\ Cardinality(DOMAIN q.wallet.obj)=3-q.amount)
 /\ (q.costCP>0 => PNativeCommitted(q))
 /\ (Len(q.stack)=3 => q.paid.phase="CostCheckpoint" /\ q.stack[2].kind="MidItemInspection" /\ q.stack[2].stage="Resolving" /\ IAT11(q).midResolving)
 /\ (q.childReturned => q.child.phase="Returned" /\ q.child.ability.returned /\ q.ledger.instances[201].status="Complete" /\ q.work# <<>>)
 /\ (q.announcement#EmptyT11 =>
     /\ q.childReturned /\ q.announcement.child=q.child /\ q.announcement.objects=q.objects
     /\ q.announcement.targets=(IF q.moves THEN {} ELSE {1}) /\ 2 \notin q.announcement.targets
     /\ q.announcement.instruction.id=q.plan.id /\ q.announcement.turn=q.flow.turn.id
     /\ CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack))
 /\ (DOMAIN q.objects={2} => q.moves /\ IAT11(q).complete /\ IAT11(q).completionReason="Moved")
 /\ (q.paidReturned => q.work= <<"CostReaction","MidEffect","MidTail">> /\ q.paid.phase="Returned" /\ q.plan.phase="Complete" /\
       q.frames[q.paid.checkpoint].returned /\ q.frames[q.paid.checkpoint].done=CheckpointStageSet103 /\ IAT11(q).midDone /\ ~IAT11(q).midResolving)
 /\ \A row \in {q.checkpointHistory[i] : i \in 1..Len(q.checkpointHistory)} : row.done=CheckpointStageSet103
 /\ (q.done => q.paidReturned /\ q.childReturned /\ DOMAIN q.frames=1..7 /\ Len(q.checkpointHistory)=7 /\
       \A id \in DOMAIN q.frames : q.frames[id].returned /\ q.frames[id].done=CheckpointStageSet103)
=============================================================================