---------------------- MODULE ActionCompositionMC ----------------------
EXTENDS ActionAdapters
CONSTANTS AScenario,AMutation
                                                                                           
AInitial(scenario) ==
 LET permissions==A2Permissions(scenario)
     basis==BasisSA(0,ACatalog,AObjects,permissions)
     seed==NewConditionalLedger96(PInitialSnapshot)
     snapshot==ConditionalSnapshotFromRegistrySA(ACatalog,basis,seed,PInitialSnapshot)
 IN AJoin([IInitialT11 EXCEPT !.objects=AObjects],
 [scenario |-> scenario,actionPhaseId |-> 4000,catalog |-> ACatalog,abilityRegistry |-> ACatalog,abilityRevision |-> 0,
  rulePermissions |-> permissions,ledger |-> NewConditionalLedger96(snapshot),registry |-> NewLingeringRegistry910,
  uses |-> EmptyT11,turnUses |-> EmptyT11,useIndex |-> EmptyT11,procedures |-> EmptyT11,
  nativeCompletion |-> EmptyT11,completionEvent |-> EmptyT11,completionOccurrence |-> EmptyT11,completionEvents |-> EmptyT11,completionCommitCount |-> 0,
  stepEvents |-> EmptyT11,stepCP |-> [role \in AStepRoles |-> 0],activeStepRole |-> "NoValue",stepReturnReceipts |-> EmptyT11,
  stepConsumed |-> {},stepContinuations |-> EmptyT11,stepOpenRecords |-> EmptyT11,closedWindows |-> EmptyT11,poppedWindows |-> EmptyT11,
  lifecycle |-> <<>>,frameRoles |-> EmptyT11,reactionContext |-> EmptyT11,reactionOwner |-> EmptyT11,noUseChildren |-> {},issuedEvents |-> {},
  native |-> EmptyT11,nativeEvents |-> EmptyT11,nativeCommitCount |-> 0,costEvent |-> EmptyT11,costOccurrence |-> EmptyT11,
  child |-> EmptyT11,childPlan |-> EmptyT11,childReturned |-> FALSE,childWindow |-> 20,work |-> <<>>,noUseCount |-> 0,
  frames |-> EmptyT11,sites |-> {},checkpointEvents |-> EmptyT11,currentCP |-> 0,costCP |-> 0,
  cpResume |-> "NoValue",cpRole |-> "NoValue",checkpointHistory |-> <<>>,basisHistory |-> EmptyT11,recognitionHistory |-> EmptyT11,
  captures |-> [key \in {<<snapshot.id,snapshot.point>>} |-> [basis |-> MinimalCaptureSA(basis),snapshot |-> snapshot]],
  issuedWorlds |-> {1},nextWorld |-> 2001,nextEvent |-> 2])
AInit == guideCaseT11=0 /\ AScenario \in {"empty","cost-reaction","completion-reaction"} /\ qT11=AInitial(AScenario)
AFrame(q) == q.frames[q.currentCP]
ASetFrame(q,f) == [q EXCEPT !.frames[f.id]=f]
ACurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,BasisSA(q.abilityRevision,q.abilityRegistry,objects,q.rulePermissions),ledger,ATemplate(q,id,point,checkpoint))
AAdmitSnapshot(q,objects,ledger,view) == objects=q.objects /\ AAdmit(q,ledger,view)
ALexemes(q) == [key \in DOMAIN ADefinitions(q) |-> RLex(ADefinitions(q)[key])]
ALegal(selected) == selected={}
ALegality(w,option,transaction) == [LegalityT11(w,option) EXCEPT !.transactionId=transaction]
AChildTurnUses(q) == FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",q.reactionContext.definition.syntax.source)
ACPData(q,f) ==
 LET b==ASnapshot(q,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="ActionCost" THEN [id \in {1} |-> q.costOccurrence]
    ELSE IF q.cpRole="AF" THEN [id \in {q.completionOccurrence.id} |-> q.completionOccurrence]
    ELSE IF AMutation="remint-cost-occurrence" /\ q.childReturned /\ q.cpRole="ChildPriority"
    THEN [id \in {2} |-> [q.costOccurrence EXCEPT !.id=2]] ELSE EmptyT11,caller |-> f.caller]
AAdmitOccurrences(q,cp) ==
 /\ ANativeCommitted(q) /\ q.nativeCommitCount=1 /\ DOMAIN q.nativeEvents={1}
 /\ cp.occurrences=(IF cp.id=q.costCP THEN [id \in {1} |-> q.costOccurrence]
      ELSE IF cp.id=q.stepCP["AF"] THEN [id \in {q.completionOccurrence.id} |-> q.completionOccurrence] ELSE EmptyT11)
 /\ (cp.id=q.stepCP["AF"] => ACompletionCommitted(q))
 /\ q.costOccurrence.id=1 /\ q.costOccurrence.nativeOperation=q.native /\ q.costOccurrence.actualEvent=q.costEvent
AOpenCheckpoint(kind,originalCaller,resume,role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 worldId==q.nextWorld
     caller==IF role="ActionCost" /\ AMutation="wrong-cost-caller" THEN [originalCaller EXCEPT !.transactionId=201] ELSE originalCaller
     event==CASE kind="Cost" -> [q.costEvent EXCEPT !.caller=caller]
        [] kind="SchemaAtom126" -> [id |-> q.nextEvent,caller |-> caller,complete |-> WindowTop9(q.stack).stage="NeedCheckpoint",
             tag |-> "PriorityAboutToBeReceived",player |-> WindowTop9(q.stack).priority]
        [] OTHER -> [id |-> q.nextEvent,caller |-> caller,complete |-> q.childPlan.phase="Complete",
             tag |-> "InstructionFinished",origin |-> "Ability",instruction |-> IF q.reactionContext.instanceId=301 THEN "AbilityInstruction720" ELSE "AbilityInstruction721",
             instructionRef |-> InstructionWindowRef93(q.childPlan),finishedPlan |-> q.childPlan]
     site==[kind |-> kind,caller |-> caller,eventId |-> event.id,snapshotId |-> worldId,inside |-> AInside(q)]
     frame==NewCheckpoint103(id,caller,worldId,AInside(q)) frames==AJoin(q.frames,[k \in {id} |-> frame])
 IN /\ id<=32 /\ event.id<=64 /\ worldId<=2256 /\ worldId \notin q.issuedWorlds
    /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,frame,id,site,event,AInside(q))
    /\ (kind="Cost" => ANativeCommitted(q) /\ q.actionPointWorld.checkpointDue /\ q.nativeCommitCount=1)
    /\ (kind="SchemaAtom126" => originalCaller=ConditionalPriorityCaller96(WindowTop9(q.stack)))
    /\ (kind="Instruction" => originalCaller=ConditionalInstructionCaller96(q.child) /\ q.childPlan.phase="Complete")
    /\ qT11'=[q EXCEPT !.frames=frames,!.frameRoles=AJoin(@,[k \in {id} |-> role]),!.sites=@ \cup {CheckpointSiteKey103(site)},!.currentCP=id,
       !.checkpointEvents=AJoin(@,[k \in {id} |-> event]),!.basisHistory=AJoin(@,[k \in {id} |-> MinimalCaptureSA(ABasis(q))]),
       !.costCP=IF role="ActionCost" THEN id ELSE @,!.cpResume=resume,!.cpRole=role,!.stage="ACP",
       !.issuedWorlds=@ \cup {worldId},!.nextWorld=@+1,!.nextEvent=IF kind="Cost" THEN @ ELSE @+1,!.issuedEvents=@ \cup {event.id}]
AActionPay ==
 LET q==qT11 after==IActionPointAfterT11(q.actionPointWorld) a==NewAction5(30,"SideB",BasicActionKey5("SideB","SchemaAtom138"))
     payment==[before |-> q.actionPointWorld,after |-> after,window |-> WindowTop9(q.stack).id,option |-> IActionOptionT11,transaction |-> 200]
     native==[operationId |-> 1,command |-> IActionPointCommandT11,before |-> q.actionPointWorld,after |-> after,payment |-> payment,actionId |-> a.id,turnId |-> q.flow.turn.id]
     committed==[q EXCEPT !.actionPointWorld=after,!.payment=payment,!.action=a,!.native=native]
     snapshot==ASnapshot(committed,q.ledger,q.nextWorld,"ActionPaymentOccurrence",q.ledger.lastCheckpoint)
     event==[id |-> 1,tag |-> "CostPaid",caller |-> ACostCaller(committed),transactionId |-> 200,
       operationId |-> 1,nativePayment |-> native,complete |-> ANativeCommitted(committed)]
     occurrence==[id |-> 1,kind |-> "ActionActionPointCostPaid",object |-> 0,actor |-> "SideB",side |-> "SideB",
       snapshot |-> snapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACostDefinition),
       actualEvent |-> event,nativeOperation |-> native,turnId |-> q.flow.turn.id]
 IN /\ AReservation(q) /\ BasicActionLocalGate5("SideB","SchemaAtom138",FALSE)
    /\ q.nativeCommitCount=0 /\ q.native=EmptyT11 /\ q.nextWorld \notin q.issuedWorlds
    /\ BasicAction5("SideB","SchemaAtom138").effect="SchemaAtom138" /\ BasicAction5("SideB","SchemaAtom138").actionPoints=1 /\ BasicAction5("SideB","SchemaAtom138").resourceUnits=0
    /\ ActionStart5(q.flow.turn,"SideB",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,AReservation(q),TRUE,q.action.status="Idle",a.id,a.key,a)
    /\ AAdmit(committed,q.ledger,snapshot)
    /\ qT11'=[committed EXCEPT !.costEvent=event,!.costOccurrence=occurrence,!.nativeEvents=[id \in {1} |-> event],
       !.nativeCommitCount=1,!.issuedEvents=@ \cup {1},!.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,!.stage="ActionCostDrain"]
    /\ IntegrationActionPointsT11!DoActionPoints(IActionPointCommandT11)
AEffects ==
 LET q==qT11 after==[q.action EXCEPT !.status="Effects"] IN
 /\ AActionPaid(q) /\ ActionEffectsBegin5(q.action,after,AActionPaid(q))
 /\ qT11'=[q EXCEPT !.action=after,!.trace=Append(@,"ProcedureCode989abc27e0c6"),!.revision=@+1,!.stage="TraversalStart"]
ACPNext(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"]
ALife(q,tag,role,cp,depth) == [tag |-> tag,role |-> role,checkpointId |-> cp,step |-> q.flow.step,
 stackDepth |-> depth,revision |-> q.revision,windowId |-> IF role="AE" /\ "AE" \in DOMAIN q.closedWindows THEN q.closedWindows["AE"].id ELSE q.NeutralValue00003.opened.id]
ACompleteAction ==
 LET q==qT11 after==[q.action EXCEPT !.status="Complete"] raw==[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]
     completed==IRecordT11([q EXCEPT !.action=after],"5.7.1f:return",{raw},"TurnAdvance")
     native==[operationId |-> 2,before |-> q.action,after |-> after,windowId |-> WindowTop9(q.stack).id,
       turnId |-> q.flow.turn.id,phaseId |-> q.actionPhaseId,rawIndex |-> Len(q.rawEvents)+1]
     event==[id |-> q.nextEvent,tag |-> "OriginalActionCompletes",rawEvent |-> raw,nativeCompletion |-> native]
     snapshot==ASnapshot(completed,q.ledger,q.nextWorld,"ActionCompletionOccurrence",q.ledger.lastCheckpoint)
     occurrence==[id |-> event.id,kind |-> "OriginalActionCompletes",object |-> 0,actor |-> "SideB",side |-> "SideB",snapshot |-> snapshot,
       scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACompletionDefinition),actualEvent |-> event,nativeCompletion |-> native]
     source==[kind |-> "NativeActionComplete",native |-> native,event |-> event]
     siteEvent==AStepEvent(completed,"AF",event.id,q.NeutralValue00003.opened.id,source,ActionReadyToContinue5(after))
     events==IF AMutation="repeated-completion-publication" THEN [id \in {event.id,event.id+1} |-> [event EXCEPT !.id=id]] ELSE [id \in {event.id} |-> event]
 IN /\ q.completionCommitCount=0 /\ "AF" \notin DOMAIN q.stepEvents
    /\ q.nextEvent \notin q.issuedEvents /\ q.nextWorld \notin q.issuedWorlds
    /\ ActionComplete5(q.action,after,"SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete)
    /\ AAdmit(completed,q.ledger,snapshot)
    /\ qT11'=[completed EXCEPT !.stage="ActionWindowReturn",!.nativeCompletion=native,!.completionEvent=event,!.completionOccurrence=occurrence,
       !.completionEvents=events,!.completionCommitCount=1,!.stepEvents=AJoin(@,[role \in {"AF"} |-> siteEvent]),
       !.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,
       !.issuedEvents=@ \cup DOMAIN events,!.nextEvent=@+IF AMutation="repeated-completion-publication" THEN 2 ELSE 1,
       !.lifecycle=Append(@,ALife(q,"ActionComplete","AF",0,Len(q.stack)))]
AOpenStep(role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 world==q.nextWorld original==q.stepEvents[role]
     caller==IF role="AF" /\ AMutation="wrong-af-caller" THEN [original.caller EXCEPT !.step="ProcedureCodea439ce381bba"]
       ELSE IF role="AE" /\ AMutation="wrong-ae-window" THEN [original.caller EXCEPT !.windowId=@+1] ELSE original.caller
     event==[original EXCEPT !.caller=caller]
     site==[kind |-> "Instruction",caller |-> caller,eventId |-> event.id,snapshotId |-> world,inside |-> AInside(q)]
     f==NewCheckpoint103(id,caller,world,AInside(q)) frames==AJoin(q.frames,[key \in {id} |-> f])
 IN /\ role \in DOMAIN q.stepEvents /\ q.stepCP[role]=0 /\ APlacement(q,role)
    /\ id<=32 /\ world<=2256 /\ world \notin q.issuedWorlds /\ event.id \in q.issuedEvents
    /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,f,id,site,event,AInside(q))
    /\ qT11'=[q EXCEPT !.frames=frames,!.frameRoles=AJoin(@,[key \in {id} |-> role]),!.sites=@ \cup {CheckpointSiteKey103(site)},
       !.checkpointEvents=AJoin(@,[key \in {id} |-> event]),!.basisHistory=AJoin(@,[key \in {id} |-> MinimalCaptureSA(ABasis(q))]),
       !.stepCP[role]=id,!.activeStepRole=role,!.currentCP=id,!.cpRole=role,!.cpResume="AStepReturn",!.stage="ACP",
       !.issuedWorlds=@ \cup {world},!.nextWorld=@+1,
       !.stepOpenRecords=AJoin(@,[key \in {role} |-> [checkpointId |-> id,stack |-> q.stack,flow |-> q.flow,event |-> event]]),
       !.lifecycle=Append(@,ALife(q,"StepOpen",role,id,0))]
AStepReturn ==
 LET q==qT11 role==q.activeStepRole f==q.frames[q.stepCP[role]]
     drain==[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(q.control.traversal)]
 IN /\ role \notin DOMAIN q.stepReturnReceipts /\ role \notin q.stepConsumed /\ AStepDrained(q,role,f)
    /\ qT11'=[q EXCEPT !.drains=Append(@,drain),!.revision=@+1,!.stage=AStepStage(role),
       !.stepReturnReceipts=AJoin(@,[key \in {role} |-> AStepReceipt(q,role,f,q.revision+1)]),
       !.lifecycle=Append(@,ALife(q,"StepReturn",role,f.id,0))]
AAdvanceStep(role) ==
 LET q==qT11 f==q.frames[q.stepCP[role]]
     suppliedFrame==IF AMutation="unreturned-" \o AStepLower(role) THEN [f EXCEPT !.returned=FALSE,!.phase="Completed"] ELSE f
     suppliedFlow==IF role="AG" /\ AMutation="stale-ag-flow" THEN [q.flow EXCEPT !.step="ProcedureCode989abc27e0c6"] ELSE q.flow
     after==[q.flow EXCEPT !.step=CASE role="AF" -> "ProcedureCodea439ce381bba" [] role="AG" -> "ProcedureCode484be3e50aa9" [] OTHER -> "ProcedureCode989abc27e0c6",!.decision="NoValue"]
     proof==ARequireStep(q,role,suppliedFrame,suppliedFlow)
     next==[q EXCEPT !.flow=after,!.stepConsumed=@ \cup {role},
       !.stepContinuations=AJoin(@,[key \in {role} |-> [before |-> q.flow,after |-> after,receipt |-> q.stepReturnReceipts[role]]]),
       !.lifecycle=Append(@,ALife(q,"StepConsume",role,f.id,0)),!.stage=IF role="AF" THEN "Drain" ELSE IF role="AG" THEN "OpenPR" ELSE "LatchNew"]
     g==IRecordT11(next,"ProcedureCodea439ce381bba",{},"TurnLoop")
     source==[kind |-> "NativeStepAdvance",before |-> q.flow,after |-> after,from |-> role,checkpointId |-> f.id]
     event==AStepEvent(g,"AG",q.nextEvent,q.NeutralValue00003.opened.id,source,after.step="ProcedureCodea439ce381bba" /\ "AF" \in next.stepConsumed)
 IN /\ proof /\ SideBStepAdvance5(q.flow,after,proof)
    /\ qT11'=IF role="AF" THEN [g EXCEPT !.stepEvents=AJoin(@,[key \in {"AG"} |-> event]),!.issuedEvents=@ \cup {event.id},!.nextEvent=@+1]
      ELSE next
AWindowWork ==
 LET q==qT11 w==WindowTop9(q.stack) IN
 IF q.windowRole="TurnPR" /\ w.kind="Paid" /\ w.stage="Ready" THEN
   LET passed==PassPriorityFrame9(w) IN
   /\ PassPriority9(q.stack,ReplaceWindowTop9(q.stack,passed),w.priority,EmptyT11)
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,passed),
       !.closedWindows=IF ~passed.open THEN AJoin(@,[key \in {"AE"} |-> passed]) ELSE @,
       !.lifecycle=IF ~passed.open THEN Append(@,[ALife(q,"TurnPRClose","AE",0,Len(q.stack)) EXCEPT !.windowId=passed.id]) ELSE @]
 ELSE IF q.windowRole="TurnPR" /\ w.stage="Closed" THEN
   LET rest==SubSeq(q.stack,1,Len(q.stack)-1) next==IRecordT11([q EXCEPT !.stack=rest],"ProcedureCode484be3e50aa9",{},"TurnContinue")
       source==[kind |-> "NativeTurnPRPop",window |-> w,afterStack |-> rest,flow |-> q.flow]
       event==AStepEvent(next,"AE",q.nextEvent,w.id,source,~w.open /\ w.stage="Closed" /\ q.flow.step="ProcedureCode484be3e50aa9")
   IN /\ w=q.closedWindows["AE"] /\ "AE" \notin DOMAIN q.stepEvents /\ q.nextEvent \notin q.issuedEvents
      /\ PopClosedPriorityWindow9(q.stack,rest)
      /\ qT11'=[next EXCEPT !.stepEvents=AJoin(@,[key \in {"AE"} |-> event]),!.poppedWindows=AJoin(@,[key \in {"AE"} |-> w]),
         !.issuedEvents=@ \cup {event.id},!.nextEvent=@+1,!.lifecycle=Append(@,ALife(q,"TurnPRPop","AE",0,Len(rest)))]
 ELSE IWindowStepT11
ABypassReaction ==
 LET q==qT11 f==AFrame(q) returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] world==AWorld(q,f) IN
 /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
 /\ qT11'=[ASetFrame(q,returned) EXCEPT !.stage="AStepReturn"]
ACheckpointWork ==
 LET q==qT11 f==AFrame(q) next==ACPNext(f) world==AWorld(q,f) IN
 CASE f.point="ProcedureCodee605a78f5d5e" ->
   LET cp==ACPData(q,f)
       keys=={[definition |-> key,occurrence |-> id] : key \in {k \in DOMAIN ADefinitions(q) :
         ConditionalActive96(ADefinitions(q)[k],cp.processingSnapshot)},id \in DOMAIN cp.occurrences}
       eligible=={k \in keys : TriggerPattern96(ADefinitions(q)[k.definition],cp.occurrences[k.occurrence])}
       allocation==[k \in IF AMutation="omit-cost-recognition" /\ q.cpRole="ActionCost" THEN {} ELSE eligible |->
          IF k.definition=ConditionalKey96(ACostDefinition) THEN 301 ELSE 302]
       bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> AInstanceWindow(allocation[k]),group |-> 4]]
       conditions==[k \in DOMAIN ADefinitions(q) |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> ADefinitions(q)[k].syntax.id,source |-> ADefinitions(q)[k].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 |-> ADefinitions(q),lexemes |-> ALexemes(q),conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]
   IN /\ AAdmitOccurrences(q,cp)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,cp.beginSnapshot)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,cp.processingSnapshot)
      /\ x.definitions=ConditionalDefinitionsSA(q.abilityRegistry)
      /\ RecognizeCheckpoint103(f,after,q.ledger,ledger,q.stack,q.stack,x)
      /\ qT11'=[ASetFrame(q,after) EXCEPT !.ledger=ledger,
        !.recognitionHistory=AJoin(@,[id \in {cp.id} |-> cp]),
        !.captures=AJoin(AAddCapture(q,cp.beginSnapshot),[captureKey \in {<<cp.processingSnapshot.id,cp.processingSnapshot.point>>} |-> ACapture(q,cp.processingSnapshot)])]
 [] 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==ASnapshot(q,q.ledger,f.snapshotId,"CleanupCurrent",f.id)
   IN /\ AWorldBound(q,f,world)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ 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'=[ASetFrame(q,next) EXCEPT !.registry=registry]
 [] f.point="ProcedureCodeb681cc249a04" ->
   /\ CheckpointVictory103(f,next,q.objects,[id \in DOMAIN q.objects |-> 0],f.snapshotId)
   /\ qT11'=ASetFrame(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,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodea488e1ba6ca3" ->
   /\ CheckpointIllegalRetire103(f,next,q.objects,q.objects,{},ALegal,[id \in DOMAIN q.objects |-> "SideA"],q.flow.turn.owner,
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],[applies |-> FALSE],"NoValue",{},EmptyT11,DOMAIN q.objects,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} ->
   /\ CheckpointHostedCleanup103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,
        EmptyT11,EmptyT11,DOMAIN q.objects,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode2d73b20aa788" ->
   /\ CheckpointAuxiliarySiteCleanup103(f,next,[s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],q.objects,EmptyT11,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode2d6279f9d639" ->
   /\ CheckpointPositionCleanup103(f,next,q.layout,q.layout,q.control.traversal.position,EmptyT11,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode7f181ce21011" ->
   /\ CheckpointRootAdmissions103(f,next,q.capacity,q.capacity,AInspection(q),q.objects,EmptyT11,0,q.ledger.stepSerial,{},IF IInsideInspectionT11(q) THEN "SideB" ELSE "NoValue",f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodeda83a77a1f12" ->
   /\ CheckpointRestoreDiscard103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,APrinted,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode0811ebc5f40e" ->
   /\ CheckpointReturnDiscardCounters103(f,next,q.objects,q.objects,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodeb74d673a0fc6" ->
   IF DOMAIN f.recognized={} THEN
     LET returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] IN
     /\ AWorldBound(q,f,world)
     /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
     /\ qT11'=[ASetFrame(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==AReactionSite(q) context==AReactionContext(q,f)
         opening==AJoin(IOpeningT11(context.windowId,"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(context.windowId,"Reaction",site,members,4,NoTimingRef9,[id |-> 0],0)
         after==[f EXCEPT !.phase="Reaction",!.windowId=context.windowId]
     IN /\ AWorldBound(q,f,world)
        /\ OpenCheckpointReaction103(f,after,q.ledger,q.stack,Append(q.stack,window),site,opening,q.usedWindows)
        /\ qT11'=[ASetFrame(q,after) EXCEPT !.stack=Append(@,window),!.usedWindows=@ \cup {context.windowId},!.childWindow=context.windowId,!.reactionContext=context,!.childReturned=FALSE,!.child=EmptyT11,!.childPlan=EmptyT11,
          !.reactionOwner=[id |-> f.id,role |-> q.cpRole,resume |-> q.cpResume],!.stage="AReceive"]
 [] OTHER -> FALSE
ATargets(plan,targets) == [ProtocolP!Targets9p(plan) EXCEPT !.targets=targets]
AReadyCP(q) == [ProtocolP!PriorityCP9p(WindowTop9(q.stack),q.currentCP) EXCEPT
 !.complete=CheckpointDrained103(AFrame(q),q.ledger,q.stack),!.reactionsDrained=CheckpointDrained103(AFrame(q),q.ledger,q.stack)]
AProtocolWork ==
 LET q==qT11 IN
 CASE q.stage="AReceive" -> AOpenCheckpoint("SchemaAtom126",ConditionalPriorityCaller96(WindowTop9(q.stack)),"AChildReady","ChildPriority")
 [] q.stage="AChildReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(AFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),AReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage=IF q.childReturned THEN "APass" ELSE "ASelect"]
 [] q.stage="ASelect" ->
   LET w==WindowTop9(q.stack) context==q.reactionContext id==context.instanceId d==context.definition
       option==PriorityOption9(70,"Conditional","SideB",d.syntax.id,id,d.syntax.source,0,{})
       busy==StartPriorityOptionFrame9(w,option,context.transaction) p==OpenConditionalProcedure96(id,d,w,option,context.transaction,"Rule")
       plan==OpenInstruction93(context.instructionId,"Ability",id,d.syntax.source,"Rule",1,"NoValue",<<context.work>>,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[q.reactionContext.instanceId].status="Imminent"]
   IN /\ q.nextWorld \notin q.issuedWorlds /\ q.nextWorld<=2256
      /\ AAdmitSnapshot(q,q.objects,q.ledger,ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint))
      /\ BeginConditionalResolution96(q.ledger,ledger,q.stack,ReplaceWindowTop9(q.stack,busy),p,imminent,d,
        ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint),id,option,ALegality(w,option,context.transaction),EmptyT11,plan,announced,
        ATargets(plan,{}),ProtocolP!Entry9p(plan,0),AChildTurnUses(q),
        [tag |-> "AbilityRestrictions",ability |-> d.syntax.id,source |-> d.syntax.source,results |-> EmptyT11])
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.stack=ReplaceWindowTop9(@,busy),!.child=imminent,!.childPlan=announced,!.captures=AAddCapture(q,ASnapshot(q,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint)),!.issuedWorlds=@ \cup {q.nextWorld},!.nextWorld=@+1,!.stage="AChildBegin"]
 [] q.stage="AChildBegin" ->
   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[q.reactionContext.instanceId].status="Resolving",!.instances[q.reactionContext.instanceId].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="AChildWork"]
 [] q.stage="AChildWork" ->
   LET 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[q.reactionContext.instanceId].status="Complete"]
       beforeId==IF AMutation="reuse-world-id" THEN q.costOccurrence.snapshot.id ELSE q.nextWorld
       beforeSnapshot==ASnapshot(q,q.ledger,beforeId,"InstructionBefore",q.ledger.lastCheckpoint)
       afterSnapshot==ASnapshot(q,ledger,q.nextWorld+1,"InstructionAfter",q.ledger.lastCheckpoint)
       captures==AJoin(AAddCapture(q,beforeSnapshot),[key \in {<<afterSnapshot.id,afterSnapshot.point>>} |-> ACapture(q,afterSnapshot)])
       step==[ProtocolP!Step9p(q.childPlan) EXCEPT !.complete=AMutation#"blocked-child-carry"]
       publishedCaptures==IF AMutation="history-rewrite" THEN [captures EXCEPT ![<<1,PInitialSnapshot.point>>].basis.revision=1] ELSE captures
   IN /\ AAdmit(q,q.ledger,beforeSnapshot) /\ AAdmit(q,ledger,afterSnapshot)
      /\ 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,step,beforeSnapshot,afterSnapshot)
      /\ beforeId \notin q.issuedWorlds /\ q.nextWorld+1 \notin q.issuedWorlds /\ q.nextWorld+1<=2256
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.noUseCount=@+1,!.noUseChildren=@ \cup {q.child.id},
        !.captures=publishedCaptures,!.issuedWorlds=@ \cup {q.nextWorld,q.nextWorld+1},!.nextWorld=@+2,
        !.work=Append(@,q.reactionContext.work),!.stage="AChildCPOpen"]
 [] q.stage="AChildCPOpen" -> AOpenCheckpoint("Instruction",ConditionalInstructionCaller96(q.child),"AChildCPDone","ChildFinal")
 [] q.stage="AChildCPDone" ->
   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 |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack),
        allNewerChainsComplete |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack)]
   IN /\ ResumeConditionalInstructionAfterCheckpoint103(AFrame(q),q.ledger,q.stack,q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stage="AChildReturn"]
 [] q.stage="AChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE] w==WindowTop9(q.stack)
       receipt==AChildReturnReceipt(q)
   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="AReceive"]
 [] q.stage="APass" ->
   LET w==WindowTop9(q.stack) after==PassPriorityFrame9(w)
       snapshot==ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Pass",q.ledger.lastCheckpoint)
   IN /\ q.nextWorld \notin q.issuedWorlds /\ q.nextWorld<=2256
      /\ AAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ PassConditionalPriority96(q.ledger,q.ledger,q.ledger,q.stack,ReplaceWindowTop9(q.stack,after),w.priority,EmptyT11,snapshot,snapshot)
      /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,after),!.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,!.stage=IF after.open THEN "AReceive" ELSE "AReactionReturn"]
 [] q.stage="AReactionReturn" ->
   LET f==q.frames[q.reactionOwner.id] 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,IF AMutation="wrong-reaction-return" THEN [f.caller EXCEPT !.transactionId=201] ELSE f.caller)
      /\ qT11'=[ASetFrame(q,returned) EXCEPT !.stack=rest,!.currentCP=q.reactionOwner.id,!.cpRole=q.reactionOwner.role,!.cpResume=q.reactionOwner.resume,!.stage=q.reactionOwner.resume,
        !.checkpointHistory=Append(@,[id |-> f.id,role |-> q.reactionOwner.role,caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
 [] q.stage="ACostResume" ->
   /\ AActionCostDrained(q,ACostCaller(q)) /\ q.actionPointWorld=q.payment.after
   /\ qT11'=[q EXCEPT !.actionPointWorld.checkpointDue=FALSE,!.costDrained=TRUE,!.currentCP=q.costCP,!.stage="ActionEffects",
       !.native=IF AMutation="native-payment-rewrite" THEN [@ EXCEPT !.before.actionPoints["SideB"]=3] ELSE @,
       !.nativeEvents=IF AMutation="sticky-payment-alias" THEN AJoin(@,[id \in {2} |-> [q.costEvent EXCEPT !.id=2]]) ELSE @]
 [] OTHER -> FALSE
AOuterStep ==
 LET q==qT11 c==q.control IN
 /\ UNCHANGED guideCaseT11
 /\ CASE q.stage="LatchStart" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],TRUE)
        /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenAction"]
   [] q.stage="OpenAction" -> IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"StartAction","ActionPay")
   [] q.stage="Window" -> AWindowWork
   [] q.stage="ActionPay" -> AActionPay
   [] q.stage="ActionCostDrain" -> AOpenCheckpoint("Cost",ACostCaller(q),"ACostResume","ActionCost")
   [] q.stage="ActionEffects" -> AEffects
   [] q.stage="TraversalStart" ->
        LET after==[q.action EXCEPT !.status="Nested",!.nested="Traversal7"] traversal==OpenTraversal6(7,1000,ITraversalCallerT11(q.action)) IN
        /\ ActionNestedBegin5(q.action,after,"Traversal7")
        /\ qT11'=[q EXCEPT !.action=after,!.waitTraversal=[id |-> traversal.id,handle |-> "Traversal7",action |-> q.action.id],!.control=TraversalControlT11(traversal),!.stage="TraversalWork"]
   [] q.stage="TraversalWork" -> ITraversalWorkT11
   [] q.stage="TraversalAdvance" -> ITraversalAdvanceT11
   [] q.stage="InspectionWork" -> IInspectionWorkT11
   [] q.stage="InspectionAdvance" -> IInspectionAdvanceT11
   [] q.stage="ItemInspectionWork" -> IItemInspectionWorkT11
   [] q.stage="ItemInspectionAdvance" -> IItemInspectionAdvanceT11
   [] q.stage="Drain" ->
        qT11'=[q EXCEPT !.drains=Append(@,[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(c.traversal)]),!.revision=@+1,!.stage=q.resume]
   [] q.stage="ItemInspectionReturn" ->
        LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] next==IWithItemInspectionT11(q,after) IN
        /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
        /\ qT11'=IRecordReturnT11(next,"ItemInspection",after,IBT11(q).id,"InspectionResume")
   [] q.stage="InspectionResume" ->
        LET b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
        /\ IItemInspectionReturnReadyT11(q) /\ FinishInspectionItemInspectionInstruction7(b,after,IItemInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([IWithInspectionT11(q,after) EXCEPT !.consumed=@ \cup {"ItemInspection"}],"7.5.5:return",{},"InspectionAdvance")
   [] q.stage="InspectionReturn" ->
        LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] next==IWithInspectionT11(q,after) IN
        /\ ReturnInspectionToCaller7(b,after,TRUE,IInspectionCallerT11(c.traversal))
        /\ qT11'=IRecordReturnT11(next,"Inspection",after,c.traversal.id,"TraversalResume")
   [] q.stage="TraversalResume" ->
        LET after==[c EXCEPT !.siteInspectionFinished=TRUE] IN
        /\ IInspectionReturnReadyT11(q) /\ FinishRulesInspectionInstruction6(c,after,IInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([q EXCEPT !.control=after,!.consumed=@ \cup {"Inspection"}],"6.9.5b:return",{},"TraversalAdvance")
   [] q.stage="TraversalReturn" ->
        LET after==[c EXCEPT !.returned=TRUE] next==[q EXCEPT !.control=after] IN
        /\ ReturnTraversalToCaller6(c,after,TRUE,ITraversalCallerT11(q.action))
        /\ qT11'=IRecordReturnT11(next,"SchemaAtom138",after,q.action.id,"ActionResume")
   [] q.stage="ActionResume" ->
        LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
        /\ ITraversalReturnReadyT11(q) /\ ActionNestedReturn5(q.action,after,q.waitTraversal.handle,ITraversalReturnReadyT11(q))
        /\ qT11'=[q EXCEPT !.action=after,!.consumed=@ \cup {"SchemaAtom138"},!.stage="ActionComplete"]
   [] q.stage="ActionComplete" -> ACompleteAction
   [] q.stage="ActionWindowReturn" ->
        LET w==WindowTop9(q.stack) closed==CompletePriorityOptionFrame9(w) IN
        /\ CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,closed),AActionReturn(q))
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,closed),!.closedWindows=AJoin(@,[role \in {"AF"} |-> closed]),
           !.lifecycle=Append(@,ALife(q,"ActionClose","AF",0,1)),!.returnOrder=Append(@,"NeutralValue00001"),!.stage="PopAction"]
   [] q.stage="PopAction" ->
        /\ PopClosedPriorityWindow9(q.stack,<<>>) /\ WindowTop9(q.stack)=q.closedWindows["AF"]
        /\ qT11'=[q EXCEPT !.poppedWindows=AJoin(@,[role \in {"AF"} |-> WindowTop9(q.stack)]),!.stack= <<>>,
           !.lifecycle=Append(@,ALife(q,"ActionPop","AF",0,0)),!.stage="Drain"]
   [] q.stage="TurnAdvance" -> AAdvanceStep("AF")
   [] q.stage="TurnLoop" -> AAdvanceStep("AG")
   [] q.stage="OpenPR" -> IOpenWindowT11("Paid",ITurnSiteT11(q),"TurnPR","TurnContinue")
   [] q.stage="TurnContinue" -> AAdvanceStep("AE")
   [] q.stage="LatchNew" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],ALatchAfterSteps(q)) /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenNewAction"]
   [] q.stage="OpenNewAction" ->
        /\ q.stack= <<>> /\ ActionReadyToContinue5(q.action) /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"}
        /\ IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"NewAction","Done")
   [] q.stage="Done" -> UNCHANGED qT11
AReturnGuardChecks(q) ==
 /\ (q.stage="ItemInspectionReturn" =>
       LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] IN
       /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,FALSE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,TRUE, <<"InspectionItemInspection",21>>))
 /\ (q.stage="InspectionResume" =>
       LET a==IAT11(q) b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
       /\ IItemInspectionReturnReadyT11(q)
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].parent=21])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].revision=q.revision-1])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].frame=[a EXCEPT !.returned=FALSE]])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"ItemInspection"}])
       /\ ItemInspectionProcedureValid7([a EXCEPT !.id=78],q.objects) /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.id=78])
       /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.caller= <<"InspectionItemInspection",21>>])
       /\ ~FinishInspectionItemInspectionInstruction7(b,after,FALSE)
       /\ ~ReturnItemInspectionToCaller7(a,a,TRUE,InspectionItemInspectionCaller7(b)))
 /\ (q.stage="InspectionReturn" =>
       LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] IN
       /\ ~ReturnInspectionToCaller7(b,after,FALSE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnInspectionToCaller7(b,after,TRUE, <<"TraversalInspectionInstruction",8,"ProcedureCoded75d879e00ff">>))
 /\ (q.stage="TraversalResume" =>
       /\ IInspectionReturnReadyT11(q)
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].revision=q.revision-1])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].frame.choices= <<>>])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"Inspection"}])
       /\ ~ReturnInspectionToCaller7(IBT11(q),IBT11(q),TRUE,IInspectionCallerT11(q.control.traversal)))
 /\ (q.stage="TraversalReturn" =>
       LET c==q.control after==[c EXCEPT !.returned=TRUE] IN
       /\ ~ReturnTraversalToCaller6(c,after,FALSE,ITraversalCallerT11(q.action))
       /\ ~ReturnTraversalToCaller6(c,after,TRUE, <<"BasicTraversalAction",31>>)
       /\ ~CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))),AActionReturn(q)))
 /\ (q.stage="ActionResume" =>
       LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
       /\ ITraversalReturnReadyT11(q)
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].revision=q.revision-1])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].frame.itemInspections[77].returned=FALSE])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.consumed=@ \cup {"SchemaAtom138"}])
       /\ ~ActionNestedReturn5(q.action,after,"SiblingTraversal",TRUE)
       /\ ~ActionNestedReturn5(q.action,after,q.waitTraversal.handle,FALSE)
       /\ ~ReturnTraversalToCaller6(q.control,q.control,TRUE,ITraversalCallerT11(q.action)))
 /\ (q.stage="ItemInspectionWork" /\ "ItemInspection" \notin DOMAIN q.receipts =>
       /\ ~IItemInspectionReturnReadyT11(q)
       /\ ~ReturnInspectionToCaller7(IBT11(q),[IBT11(q) EXCEPT !.returned=TRUE],TRUE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnTraversalToCaller6(q.control,[q.control EXCEPT !.returned=TRUE],TRUE,ITraversalCallerT11(q.action))
       /\ ~ReturnItemInspectionToCaller7(IAT11(q),[IAT11(q) EXCEPT !.returned=TRUE],TRUE,InspectionItemInspectionCaller7(IBT11(q))))
 /\ (q.stage="OpenNewAction" =>
       LET site==ITurnSiteT11(q) oldId==q.NeutralValue00003.opened.id w==NewPriorityWindow9(oldId,"NeutralValue00001",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0) IN
       /\ ~OpenPriorityWindow9(q.stack,Append(q.stack,w),oldId,"NeutralValue00001",site,EmptyT11,IOpeningT11(oldId,"NeutralValue00001",site),q.usedWindows)
       /\ q.action.status="Complete" /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"})
 /\ (q.stage \in {"ActionComplete","ActionWindowReturn"} =>
       LET after==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
       /\ (CompletePriorityOption9(q.stack,after,AActionReturn(q)) = (q.stage="ActionWindowReturn"))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.action.status="Effects"]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.control.returned=FALSE]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.consumed=@ \ {"SchemaAtom138"}]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.costDrained=FALSE])))
AOuterSafety ==
 LET q==qT11 IN
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal)
 /\ AReturnGuardChecks(q)
 /\ IActionWindowOrderT11(q)
 /\ \A i \in 1..Len(q.windowHistory) : IWindowClassT11(q.windowHistory[i])=IntegrationOracleWindowClasses11[q.windowHistory[i].at] /\ ~PaidWindowOptions9(q.windowHistory[i].site).score
 /\ (q.action.status#"Complete" => \A i \in 1..Len(q.windowHistory) : q.windowHistory[i].at#"5.7.1f:new")
 /\ q.objects=AObjects /\ ANativeProjection(q.objects)=IInitialT11.objects /\ q.fund=0 /\ q.bank=0
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(IntegrationOracleTrace11,1,Len(q.trace))
 /\ IEventNamesT11(q) \cap IntegrationOracleAbsent11={}
 /\ \A i \in 1..Len(q.stack) : PriorityWindowValid9(q.stack[i])
 /\ \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.action.status="Nested" => Len(q.stack)>0 /\ q.stack[1].kind="NeutralValue00001" /\ q.stack[1].open
       /\ q.stack[1].stage="Resolving" /\ q.stack[1].busy=IActionOptionT11)
 /\ ("ItemInspection" \in q.consumed => IAT11(q).returned)
 /\ ("Inspection" \in q.consumed => IBT11(q).returned)
 /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done =>
       /\ q.trace=IntegrationOracleTrace11 /\ q.returnOrder=IntegrationOracleReturnOrder11
       /\ q.actionPointWorld.actionPoints["SideB"]=IntegrationOracleEndActionPoints11 /\ q.actionPointWorld.spent["SideB"]=1
       /\ q.action.status="Complete" /\ q.control.returned /\ q.control.traversal.complete /\ q.control.traversal.successful /\ ~q.control.traversal.unsuccessful
       /\ InspectionCentralChoices7(IBT11(q))=IntegrationOracleCentralChoices11
       /\ Cardinality(ActualItemInspectionesInInspection7(q.itemInspectionHistory,20))=IntegrationOracleActualItemInspectiones11
       /\ \A name \in IntegrationOracleEvents11 : IEventCountT11(q,name)=1
       /\ Len(q.stack)=1 /\ WindowTop9(q.stack).kind="NeutralValue00001" /\ WindowTop9(q.stack).stage="Ready" /\ WindowTop9(q.stack).priority="SideB"
       /\ WindowTop9(q.stack).id#q.NeutralValue00003.opened.id /\ WindowTop9(q.stack).busy=NoPriorityOption9
       /\ ~CanPassPriority9(WindowTop9(q.stack),EmptyT11))
AWork ==
 /\ UNCHANGED guideCaseT11
 /\ IF (qT11.stage="ActionWindowReturn" /\ AMutation="early-af-open") \/ (qT11.stage="PopAction" /\ AMutation="af-before-pop") THEN AOpenStep("AF")
    ELSE IF qT11.stage="TurnAdvance" /\ AMutation="duplicate-step-return" THEN AStepReturn
    ELSE IF qT11.stage="Drain" /\ qT11.lastWork="ProcedureCodea439ce381bba" /\ AMutation="duplicate-af" THEN AAdvanceStep("AF")
    ELSE IF qT11.stage="OpenPR" /\ AMutation="duplicate-ag" THEN AAdvanceStep("AG")
    ELSE IF qT11.stage="LatchNew" /\ AMutation="duplicate-ae" THEN AAdvanceStep("AE")
    ELSE IF qT11.stage="Drain" /\ qT11.lastWork \in {"5.7.1f:return","ProcedureCodea439ce381bba","ProcedureCode484be3e50aa9"}
       THEN AOpenStep(CASE qT11.lastWork="5.7.1f:return" -> "AF" [] qT11.lastWork="ProcedureCodea439ce381bba" -> "AG" [] OTHER -> "AE")
    ELSE IF qT11.stage="AStepReturn" THEN AStepReturn
    ELSE IF qT11.stage="ACP" THEN
       IF qT11.cpRole="ActionCost" /\ AFrame(qT11).point="ProcedureCode88eda145024f" /\ AMutation="skip-cost-stage"
       THEN CheckpointVictory103(AFrame(qT11),ACPNext(AFrame(qT11)),qT11.objects,[id \in DOMAIN qT11.objects |-> 0],AFrame(qT11).snapshotId) /\ UNCHANGED qT11
       ELSE IF qT11.cpRole="ActionCost" /\ AFrame(qT11).point="ProcedureCode88eda145024f" /\ AMutation="early-action-effects" THEN AEffects
       ELSE IF qT11.cpRole="AF" /\ AFrame(qT11).point="ProcedureCodeb74d673a0fc6" /\ AMutation="post-step-child-bypass"
         THEN ABypassReaction
       ELSE IF qT11.cpRole="AF" /\ AFrame(qT11).point="ProcedureCodeb74d673a0fc6" /\ AMutation="advance-with-pending-completion-child" THEN AAdvanceStep("AF")
       ELSE ACheckpointWork
    ELSE IF qT11.stage \in {"AReceive","AChildReady","ASelect","AChildBegin","AChildWork","AChildCPOpen","AChildCPDone","AChildReturn","APass","AReactionReturn","ACostResume"}
       THEN AProtocolWork ELSE AOuterStep
AHistoryFrame(before,after) ==
 /\ ACaptureFrame(before,after) /\ before.issuedWorlds \subseteq after.issuedWorlds
 /\ DOMAIN before.recognitionHistory \subseteq DOMAIN after.recognitionHistory
 /\ \A id \in DOMAIN before.recognitionHistory : before.recognitionHistory[id]=after.recognitionHistory[id]
 /\ before.issuedEvents \subseteq after.issuedEvents
 /\ \A field \in {"stepEvents","stepReturnReceipts","stepContinuations","closedWindows","poppedWindows"} :
      /\ DOMAIN before[field] \subseteq DOMAIN after[field]
      /\ \A key \in DOMAIN before[field] : before[field][key]=after[field][key]
 /\ (before.completionCommitCount>0 => before.nativeCompletion=after.nativeCompletion /\ before.completionEvent=after.completionEvent /\ before.completionOccurrence=after.completionOccurrence)
ANext == AWork /\ AHistoryFrame(qT11,qT11')
ASpec == AInit /\ [][ANext]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ANext)
AEventuallyReturns == <>qT11.done
ASourceSafety ==
 LET q==qT11 IN
 /\ q.catalog=ACatalog /\ q.abilityRegistry=q.catalog /\ q.abilityRevision=0
 /\ q.rulePermissions=A2Permissions(q.scenario)
 /\ q.actionPhaseId=4000 /\ q.flow.turn.id=2 /\ q.flow.turn.phase="NeutralValue00001"
 /\ BasisValidSA(q.catalog,ABasis(q)) /\ LedgerDomainSA(q.ledger)
 /\ q.uses=EmptyT11 /\ q.turnUses=EmptyT11 /\ q.useIndex=EmptyT11 /\ q.procedures=EmptyT11
 /\ UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
 /\ q.objects=AObjects /\ ANativeProjection(q.objects)=ANativeObjects
AActionPaymentSafety ==
 LET q==qT11 IN
 /\ q.nativeCommitCount \in {0,1}
 /\ IF q.nativeCommitCount=0 THEN q.native=EmptyT11 /\ q.nativeEvents=EmptyT11 ELSE
      /\ ANativeCommitted(q) /\ DOMAIN q.nativeEvents={1} /\ q.nativeEvents[1]=q.costEvent
      /\ q.costEvent.id=1 /\ q.costEvent.operationId=1 /\ q.costEvent.nativePayment=q.native
      /\ q.costOccurrence.id=1 /\ q.costOccurrence.actualEvent=q.costEvent /\ q.costOccurrence.nativeOperation=q.native
      /\ q.actionPointWorld=(IF q.costDrained THEN [q.payment.after EXCEPT !.checkpointDue=FALSE] ELSE q.payment.after)
      /\ (q.costDrained => AActionCostDrained(q,ACostCaller(q)))
ACheckpointSafety ==
 LET q==qT11 IN
 /\ DOMAIN q.checkpointEvents=DOMAIN q.frames /\ DOMAIN q.basisHistory=DOMAIN q.frames
 /\ q.registry.cleanupIds={id \in DOMAIN q.frames : "ProcedureCode88eda145024f" \in q.frames[id].done}
 /\ (q.costCP>0 => q.frames[q.costCP].caller=ACostCaller(q))
 /\ \A id \in DOMAIN q.recognitionHistory :
     LET cp==q.recognitionHistory[id] IN
     /\ cp.beginSnapshot.id=cp.processingSnapshot.id /\ cp.id=id /\ cp.caller=q.frames[id].caller
     /\ cp.beginSnapshot.objects=q.basisHistory[id].objects
     /\ IF id=q.costCP THEN cp.occurrences=[k \in {1} |-> q.costOccurrence]
         ELSE IF id=q.stepCP["AF"] THEN cp.occurrences=[k \in {q.completionOccurrence.id} |-> q.completionOccurrence] ELSE cp.occurrences=EmptyT11
 /\ (q.done =>
     /\ DOMAIN q.frames=(IF q.scenario="empty" THEN 1..4 ELSE 1..8)
     /\ \A id \in DOMAIN q.frames : q.frames[id].returned /\ q.frames[id].done=CheckpointStageSet103 /\ q.frames[id].owed= <<>>
     /\ (IF q.scenario="empty" THEN q.child=EmptyT11 /\ q.ledger.instances=EmptyT11 /\ q.noUseCount=0 /\ q.work= <<>>
          ELSE q.childReturned /\ q.child.phase="Returned" /\ q.child.ability.returned /\ q.ledger.instances[q.reactionContext.instanceId].status="Complete" /\ ~q.ledger.instances[q.reactionContext.instanceId].used /\ q.noUseCount=1 /\ q.work= <<IF q.scenario="cost-reaction" THEN "ActionCostReaction" ELSE "ActionCompletionReaction">>))
AInstanceCapture(i) == [member |-> i.member,definition |-> i.definition,definitionCopy |-> i.definitionCopy,
 activationEpoch |-> i.activationEpoch,checkpointId |-> i.checkpointId,occurrence |-> i.occurrence,hadSnapshot |-> i.hadSnapshot]
AHistorySafety ==
 LET q==qT11 IN
 /\ \A key \in DOMAIN q.captures :
    /\ q.captures[key].basis=MinimalCaptureSA(ABasis(q)) /\ q.captures[key].snapshot.id \in q.issuedWorlds
    /\ key= <<q.captures[key].snapshot.id,q.captures[key].snapshot.point>>
 /\ DOMAIN q.ledger.instances \subseteq {301,302}
 /\ \A id \in DOMAIN q.ledger.instances :
     LET instance==q.ledger.instances[id] cp==q.recognitionHistory[instance.checkpointId]
         original==NewConditionalInstance96(id,AInstanceDefinition(id),cp,instance.occurrence,AInstanceWindow(id),4) IN
     /\ AInstanceCapture(q.ledger.instances[id])=AInstanceCapture(original)
 /\ (q.child#EmptyT11 => ConditionalProcedureBound96(q.ledger,q.child) /\ q.child.definition=q.reactionContext.definition)
 /\ (q.costCP>0 => \A id \in DOMAIN q.frames : q.frames[id].snapshotId \in q.issuedWorlds)
ACompletionSafety ==
 LET q==qT11 IN
 /\ q.completionCommitCount \in {0,1}
 /\ (q.completionCommitCount=0 => q.completionEvents=EmptyT11 /\ q.nativeCompletion=EmptyT11)
 /\ (q.completionCommitCount=1 => ACompletionCommitted(q) /\ DOMAIN q.completionEvents={q.completionEvent.id} /\ q.completionEvents[q.completionEvent.id]=q.completionEvent)
 /\ (q.done => q.completionCommitCount=1)
AStepSafety ==
 LET q==qT11 IN
 /\ DOMAIN q.stepEvents \subseteq AStepRoles /\ q.stepConsumed \subseteq DOMAIN q.stepReturnReceipts
 /\ \A role \in {r \in AStepRoles : q.stepCP[r]>0} :
      /\ q.frames[q.stepCP[role]].caller=AStepCaller(q,role,AStepWindow(q,role))
      /\ q.stepOpenRecords[role].stack= <<>> /\ q.stepOpenRecords[role].flow.step=AStepName(role)
      /\ q.checkpointEvents[q.stepCP[role]].origin="TimingStep" /\ q.checkpointEvents[q.stepCP[role]].instruction=AStepName(role)
 /\ \A role \in DOMAIN q.stepContinuations :
      /\ role \in q.stepConsumed /\ q.stepContinuations[role].receipt=q.stepReturnReceipts[role]
      /\ q.stepContinuations[role].before.step=AStepName(role)
 /\ (q.stage \in {"ActionWindowReturn","PopAction"} => q.stepCP["AF"]=0)
 /\ \A row \in {q.lifecycle[i] : i \in 1..Len(q.lifecycle)} :
      /\ (row.tag \in {"TurnPRClose","TurnPRPop"} => "AE" \in DOMAIN q.closedWindows /\ row.windowId=q.closedWindows["AE"].id)
      /\ (row.tag \in {"StepOpen","StepReturn","StepConsume"} => row.windowId=AStepWindow(q,row.role))
 /\ ("AF" \in DOMAIN q.poppedWindows => q.poppedWindows["AF"]=q.closedWindows["AF"] /\ ~q.poppedWindows["AF"].open /\ q.poppedWindows["AF"].kind="NeutralValue00001")
 /\ ("AE" \in DOMAIN q.poppedWindows => q.poppedWindows["AE"]=q.closedWindows["AE"] /\ ~q.poppedWindows["AE"].open /\ q.poppedWindows["AE"].kind="Paid")
 /\ (q.done => \A role \in AStepRoles : \A tag \in {"StepOpen","StepReturn","StepConsume"} :
      Cardinality({i \in 1..Len(q.lifecycle) : q.lifecycle[i].role=role /\ q.lifecycle[i].tag=tag})=1)
 /\ (q.done => q.stepConsumed=AStepRoles /\ DOMAIN q.stepReturnReceipts=AStepRoles /\ DOMAIN q.stepContinuations=AStepRoles)
AObservedRole(q) ==
 IF q.stage \in {"ActionWindowReturn","PopAction","TurnAdvance"} \/ (q.stage="Drain" /\ q.lastWork="ProcedureCodea439ce381bba") THEN "AF"
 ELSE IF q.stage \in {"TurnLoop","OpenPR"} THEN "AG"
 ELSE IF q.stage \in {"TurnContinue","LatchNew"} THEN "AE" ELSE q.activeStepRole
ASpecimen0139(q) ==
 IF q.stage="PopAction" THEN "af-closed-before-pop"
 ELSE IF q.stage="ActionWindowReturn" THEN "af-before-pop"
 ELSE IF q.stage="AStepReturn" THEN "step-return-ready"
 ELSE IF q.stage \in {"TurnAdvance","TurnLoop","TurnContinue"} THEN "step-before-advance"
 ELSE IF (q.stage="Drain" /\ q.lastWork="ProcedureCodea439ce381bba") \/ q.stage \in {"OpenPR","LatchNew"} THEN "step-after-consume"
 ELSE IF q.stage="ACP" /\ q.cpRole="AF" /\ AFrame(q).point="ProcedureCodeb74d673a0fc6" /\ DOMAIN AFrame(q).recognized#{} THEN "af-reaction-pending"
 ELSE IF q.stage="ACP" /\ q.cpRole="ActionCost" THEN "cost-frame-open"
 ELSE IF q.stage="ACostResume" THEN "cost-returned"
 ELSE IF q.stage="ACP" /\ q.cpRole="ChildPriority" /\ q.childReturned /\ AFrame(q).point="ProcedureCodee605a78f5d5e" THEN "post-child-reception"
 ELSE IF q.stage="AChildWork" THEN "child-instruction"
 ELSE IF q.stage="AReactionReturn" THEN "reaction-return" ELSE "other"
AObservedChild(q) == IF q.reactionContext#EmptyT11 THEN q.reactionContext.instanceId ELSE IF 302 \in DOMAIN q.ledger.instances THEN 302 ELSE 301
AObservation(q) == [tag |-> "ActionStage",scenario |-> q.scenario,stage |-> q.stage,NeutralValue00012 |-> ASpecimen0139(q),done |-> q.done,
 paymentCommitted |-> ANativeCommitted(q),completionCommitted |-> ACompletionCommitted(q),nativeCommitCount |-> q.nativeCommitCount,
 nativeOperationId |-> IF q.native=EmptyT11 THEN 0 ELSE q.native.operationId,completionCommitCount |-> q.completionCommitCount,
 checkpointDue |-> q.actionPointWorld.checkpointDue,costDrained |-> q.costDrained,cpRole |-> q.cpRole,currentCP |-> q.currentCP,costCP |-> q.costCP,
 point |-> IF q.currentCP=0 THEN "NoValue" ELSE AFrame(q).point,phase |-> IF q.currentCP=0 THEN "NoValue" ELSE AFrame(q).phase,
 childStatus |-> IF AObservedChild(q) \in DOMAIN q.ledger.instances THEN q.ledger.instances[AObservedChild(q)].status ELSE "Absent",
 childPhase |-> IF q.child=EmptyT11 THEN "NoValue" ELSE q.child.phase,childReturned |-> q.childReturned,noUseCount |-> q.noUseCount,
 useCount |-> Cardinality(DOMAIN q.uses),indexCount |-> Cardinality(DOMAIN q.useIndex),actionStatus |-> q.action.status,
 controlActive |-> ConditionalActive96(ACostDefinition,ASnapshot(q,q.ledger,q.nextWorld,"ObservedCurrent",q.ledger.lastCheckpoint)),
 completionControlActive |-> ConditionalActive96(ACompletionDefinition,ASnapshot(q,q.ledger,q.nextWorld,"ObservedCurrent",q.ledger.lastCheckpoint)),
 stepRole |-> AObservedRole(q),stepWasConsumed |-> AObservedRole(q) \in q.stepConsumed,
 stepReceiptPublished |-> AObservedRole(q) \in DOMAIN q.stepReturnReceipts,stepCP |-> q.stepCP,stepConsumed |-> q.stepConsumed,
 stepEvents |-> q.stepEvents,stepReturnReceipts |-> q.stepReturnReceipts,stepContinuations |-> q.stepContinuations,
 closedWindows |-> q.closedWindows,poppedWindows |-> q.poppedWindows,lifecycle |-> q.lifecycle,
 stackDepth |-> Len(q.stack),stack |-> q.stack,topKind |-> IF Len(q.stack)=0 THEN "NoValue" ELSE WindowTop9(q.stack).kind,
 topOpen |-> IF Len(q.stack)=0 THEN FALSE ELSE WindowTop9(q.stack).open,currentFlow |-> q.flow,
 objects |-> ANativeProjection(q.objects),actionPoints |-> q.actionPointWorld.actionPoints,spent |-> q.actionPointWorld.spent,
 frames |-> [id \in DOMAIN q.frames |-> [caller |-> q.frames[id].caller,done |-> q.frames[id].done,point |-> q.frames[id].point,phase |-> q.frames[id].phase,returned |-> q.frames[id].returned]],
 returnOrder |-> q.returnOrder,consumed |-> q.consumed,work |-> q.work]
ACompletion(q) == [tag |-> "ActionCompletion",scenario |-> q.scenario,trace |-> q.trace,objects |-> ANativeProjection(q.objects),
 enrichedObjects |-> q.objects,actionPointWorld |-> q.actionPointWorld,payment |-> q.payment,native |-> q.native,nativeCommitCount |-> q.nativeCommitCount,
 nativeEvents |-> q.nativeEvents,costEvent |-> q.costEvent,costOccurrence |-> q.costOccurrence,
 nativeCompletion |-> q.nativeCompletion,completionEvent |-> q.completionEvent,completionOccurrence |-> q.completionOccurrence,completionEvents |-> q.completionEvents,
 completionCommitCount |-> q.completionCommitCount,stepEvents |-> q.stepEvents,stepCP |-> q.stepCP,stepConsumed |-> q.stepConsumed,
 stepReturnReceipts |-> q.stepReturnReceipts,stepContinuations |-> q.stepContinuations,stepOpenRecords |-> q.stepOpenRecords,
 closedWindows |-> q.closedWindows,poppedWindows |-> q.poppedWindows,lifecycle |-> q.lifecycle,
 returnOrder |-> q.returnOrder,consumed |-> q.consumed,rawEvents |-> q.rawEvents,windowHistory |-> q.windowHistory,drains |-> q.drains,
 finalAction |-> q.action,finalWindow |-> WindowTop9(q.stack),frames |-> q.frames,frameRoles |-> q.frameRoles,recognitionHistory |-> q.recognitionHistory,
 uses |-> q.uses,turnUses |-> q.turnUses,useIndex |-> q.useIndex,procedures |-> q.procedures,
 child |-> q.child,childPlan |-> q.childPlan,childReturned |-> q.childReturned,instances |-> q.ledger.instances,
 reactionOwner |-> q.reactionOwner,reactionContext |-> q.reactionContext,noUseCount |-> q.noUseCount,work |-> q.work,
 checkpointHistory |-> q.checkpointHistory,captures |-> q.captures,issuedWorlds |-> q.issuedWorlds,issuedEvents |-> q.issuedEvents]
=============================================================================