Cortex.Wire.AdmissionArtifact.Primitive

proofs

On this page

Overview
Primitive Graph Steps

Imports

import Cortex.Wire.AdmissionArtifact.Boundary

Overview

Primitive graph-step rows for decoded Wire admission artifacts.

The declarations here mirror the Haskell primitive admission trace: empty, node, binding-reference, overlay, and connect rows plus their local validator obligations and row-level projection lemmas.

              namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIR

Primitive Graph Steps

Primitive graph-admission step recorded by Haskell lowering.

inductive PrimitiveGraphStep where
  | empty
  | node
      (node : NodeId)
      (entries exits : List AdmissionBoundaryPort)
  | bindingRef (binding : BindingName)
  | overlay
      (leftNodes rightNodes : List NodeId)
      (leftBindings rightBindings : List BindingName)
  | connect
      (leftExits rightEntries : List AdmissionBoundaryPort)
      (matchedPairs : List AdmissionConnection)
      (unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort)
  deriving Repr

namespace PrimitiveGraphStep

Primitive node boundary rows are owned by the node row that serializes them.

def NodeFrontiersOwned
    (node : NodeId)
    (entries exits : List AdmissionBoundaryPort) :
    Prop :=
  (∀ entry, entry ∈ entries → entry.node = node) ∧
    (∀ exit, exit ∈ exits → exit.node = node)

Primitive node frontier rows do not duplicate boundary identities.

def NodeFrontiersLinear
    (entries exits : List AdmissionBoundaryPort) :
    Prop :=
  (entries.map AdmissionBoundaryPort.key).Nodup ∧
    (exits.map AdmissionBoundaryPort.key).Nodup

Primitive overlay side ledgers are duplicate-free before they are merged.

def OverlayLedgersUnique
    (leftNodes rightNodes : List NodeId)
    (leftBindings rightBindings : List BindingName) :
    Prop :=
  leftNodes.Nodup ∧ rightNodes.Nodup ∧ leftBindings.Nodup ∧ rightBindings.Nodup

Primitive overlay rows must keep left/right node and binding ledgers disjoint.

def OverlayLedgersDisjoint
    (leftNodes rightNodes : List NodeId)
    (leftBindings rightBindings : List BindingName) :
    Prop :=
  (∀ node, node ∈ leftNodes → node ∈ rightNodes → False) ∧
    (∀ binding, binding ∈ leftBindings → binding ∈ rightBindings → False)

Matched primitive connect rows cannot reuse an output endpoint or input endpoint.

def ConnectPairsLinear (matchedPairs : List AdmissionConnection) : Prop :=
  (matchedPairs.map AdmissionConnection.fromKey).Nodup ∧
    (matchedPairs.map AdmissionConnection.toKey).Nodup

Serialized primitive connect frontiers do not contain duplicate endpoint keys.

def ConnectFrontiersLinear
    (leftExits rightEntries : List AdmissionBoundaryPort) :
    Prop :=
  (leftExits.map AdmissionBoundaryPort.key).Nodup ∧
    (rightEntries.map AdmissionBoundaryPort.key).Nodup

Matched and unmatched primitive connect rows partition the serialized frontiers exactly.

def ConnectFrontierPartition
    (leftExits rightEntries : List AdmissionBoundaryPort)
    (matchedPairs : List AdmissionConnection)
    (unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort) :
    Prop :=
  ((matchedPairs.map AdmissionConnection.fromKey) ++
      (unmatchedLeftExits.map AdmissionBoundaryPort.key)).Perm
    (leftExits.map AdmissionBoundaryPort.key) ∧
  ((matchedPairs.map AdmissionConnection.toKey) ++
      (unmatchedRightEntries.map AdmissionBoundaryPort.key)).Perm
    (rightEntries.map AdmissionBoundaryPort.key)

Every compatible left/right frontier pair is present in the matched-pair ledger.

def ConnectMatchesAllCompatible
    (leftExits rightEntries : List AdmissionBoundaryPort)
    (matchedPairs : List AdmissionConnection) :
    Prop :=
  ∀ leftExit, leftExit ∈ leftExits →
    ∀ rightEntry, rightEntry ∈ rightEntries →
      leftExit.CompatibleWith rightEntry →
        ∃ pair, pair ∈ matchedPairs ∧
          pair.fromPort = leftExit ∧ pair.toPort = rightEntry

Primitive connect rows carry structurally valid frontiers and contraction rows.

def ConnectRowsValid
    (leftExits rightEntries : List AdmissionBoundaryPort)
    (matchedPairs : List AdmissionConnection)
    (unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort) :
    Prop :=
  BoundaryPortsValid leftExits ∧
    BoundaryPortsValid rightEntries ∧
    ConnectionsValid matchedPairs ∧
    BoundaryPortsValid unmatchedLeftExits ∧
    BoundaryPortsValid unmatchedRightEntries

Top-level raw connections projected from this primitive trace row.

def rawConnections : PrimitiveGraphStep → List AdmissionRawConnection
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries _exits => []
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries =>
      matchedPairs.map AdmissionRawConnection.ofAdmissionConnection

Boundary contractions serialized by this primitive trace row.

def matchedConnections : PrimitiveGraphStep → List AdmissionConnection
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries _exits => []
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries =>
      matchedPairs

Top-level node summary rows projected from this primitive trace row.

def nodeRows : PrimitiveGraphStep → List NodeId
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node nodeId _entries _exits => [nodeId]
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries _matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries => []

Top-level binding-ref summary rows projected from this primitive trace row.

def bindingRows : PrimitiveGraphStep → List BindingName
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries _exits => []
  | PrimitiveGraphStep.bindingRef binding => [binding]
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries _matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries => []

Primitive node entry boundary keys projected from this trace row.

def nodeEntryKeys : PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node entries _exits =>
      entries.map AdmissionBoundaryPort.key
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries _matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries => []

Primitive node exit boundary keys projected from this trace row.

def nodeExitKeys : PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries exits =>
      exits.map AdmissionBoundaryPort.key
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries _matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries => []

Input boundary keys consumed by primitive connect rows.

def consumedEntryKeys : PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries _exits => []
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries =>
      matchedPairs.map AdmissionConnection.toKey

Output boundary keys consumed by primitive connect rows.

def consumedExitKeys : PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | PrimitiveGraphStep.empty => []
  | PrimitiveGraphStep.node _node _entries _exits => []
  | PrimitiveGraphStep.bindingRef _binding => []
  | PrimitiveGraphStep.overlay _leftNodes _rightNodes _leftBindings _rightBindings => []
  | PrimitiveGraphStep.connect _leftExits _rightEntries matchedPairs
      _unmatchedLeftExits _unmatchedRightEntries =>
      matchedPairs.map AdmissionConnection.fromKey

Top-level raw connections projected from a list of primitive trace rows.

def rawConnectionsList : List PrimitiveGraphStep → List AdmissionRawConnection
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.rawConnections ++ rawConnectionsList primitiveSteps

Boundary contractions projected from a list of primitive trace rows.

def matchedConnectionsList : List PrimitiveGraphStep → List AdmissionConnection
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.matchedConnections ++ matchedConnectionsList primitiveSteps

Primitive raw connections are exactly the raw projection of matched contractions.

theorem rawConnectionsList_eq_map_matchedConnectionsList
    (primitiveSteps : List PrimitiveGraphStep) :
    rawConnectionsList primitiveSteps =
      (matchedConnectionsList primitiveSteps).map
        AdmissionRawConnection.ofAdmissionConnection := byprimitiveSteps:List PrimitiveGraphStep⊢ rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)
  induction primitiveSteps with
  | nil =>nil⊢ rawConnectionsList [] = List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList [])
      rflAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)⊢ rawConnectionsList (primitiveStep :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList (primitiveStep :: primitiveSteps))
      cases primitiveStep with
      | empty =>cons.emptyprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)⊢ rawConnectionsList (empty :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList (empty :: primitiveSteps))
          simp [rawConnectionsList, matchedConnectionsList, rawConnections,
            matchedConnections, ih]All goals completed! 🐙
      | node node entries exits =>cons.nodeprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)node:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPort⊢ rawConnectionsList (PrimitiveGraphStep.node node entries exits :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection
    (matchedConnectionsList (PrimitiveGraphStep.node node entries exits :: primitiveSteps))
          simp [rawConnectionsList, matchedConnectionsList, rawConnections,
            matchedConnections, ih]All goals completed! 🐙
      | bindingRef binding =>cons.bindingRefprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)binding:BindingName⊢ rawConnectionsList (bindingRef binding :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList (bindingRef binding :: primitiveSteps))
          simp [rawConnectionsList, matchedConnectionsList, rawConnections,
            matchedConnections, ih]All goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlayprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)leftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingName⊢ rawConnectionsList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection
    (matchedConnectionsList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps))
          simp [rawConnectionsList, matchedConnectionsList, rawConnections,
            matchedConnections, ih]All goals completed! 🐙
      | connect leftExits rightEntries matchedPairs unmatchedLeftExits
          unmatchedRightEntries =>cons.connectprimitiveSteps:List PrimitiveGraphStepih:rawConnectionsList primitiveSteps =
  List.map AdmissionRawConnection.ofAdmissionConnection (matchedConnectionsList primitiveSteps)leftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPort⊢ rawConnectionsList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps) =
  List.map AdmissionRawConnection.ofAdmissionConnection
    (matchedConnectionsList
      (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps))
          simp [rawConnectionsList, matchedConnectionsList, rawConnections,
            matchedConnections, ih, List.map_append]All goals completed! 🐙

Top-level node summary rows projected from a list of primitive trace rows.

def nodeRowsList : List PrimitiveGraphStep → List NodeId
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.nodeRows ++ nodeRowsList primitiveSteps

Top-level binding-ref summary rows projected from a list of primitive trace rows.

def bindingRowsList : List PrimitiveGraphStep → List BindingName
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.bindingRows ++ bindingRowsList primitiveSteps

Primitive node rows contribute their node identity to the primitive node-row ledger.

theorem nodeRowsList_mem_of_node_mem
    {primitiveSteps : List PrimitiveGraphStep}
    {node : NodeId}
    {entries exits : List AdmissionBoundaryPort}
    (hStep : PrimitiveGraphStep.node node entries exits ∈ primitiveSteps) :
    node ∈ nodeRowsList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStepnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ node ∈ nodeRowsList primitiveSteps
  induction primitiveSteps with
  | nil =>nilnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈ []⊢ node ∈ nodeRowsList []
      cases hStepAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveStepshStep:PrimitiveGraphStep.node node entries exits ∈ primitiveStep :: primitiveSteps⊢ node ∈ nodeRowsList (primitiveStep :: primitiveSteps)
      simp [nodeRowsList] at hStep ⊢consnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveStepshStep:PrimitiveGraphStep.node node entries exits = primitiveStep ∨ PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ node ∈ primitiveStep.nodeRows ∨ node ∈ nodeRowsList primitiveSteps
      cases hStep with
      | inl hHead =>cons.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveStepshHead:PrimitiveGraphStep.node node entries exits = primitiveStep⊢ node ∈ primitiveStep.nodeRows ∨ node ∈ nodeRowsList primitiveSteps
          cases hHeadcons.inl.reflnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveSteps⊢ node ∈ (PrimitiveGraphStep.node node entries exits).nodeRows ∨ node ∈ nodeRowsList primitiveSteps
          exact Or.inl (bynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveSteps⊢ node ∈ (PrimitiveGraphStep.node node entries exits).nodeRows simp [nodeRows]All goals completed! 🐙)
      | inr hTail =>cons.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps → node ∈ nodeRowsList primitiveStepshTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ node ∈ primitiveStep.nodeRows ∨ node ∈ nodeRowsList primitiveSteps
          exact Or.inr (ih hTail)All goals completed! 🐙

Duplicate-free primitive node ledgers make node frontier rows unique.

theorem node_frontiers_eq_of_nodeRowsList_nodup
    {primitiveSteps : List PrimitiveGraphStep}
    (hUnique : (nodeRowsList primitiveSteps).Nodup)
    {node : NodeId}
    {entries₁ exits₁ entries₂ exits₂ : List AdmissionBoundaryPort}
    (hLeft : PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps)
    (hRight : PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps) :
    entries₁ = entries₂ ∧ exits₁ = exits₂ := byprimitiveSteps:List PrimitiveGraphStephUnique:(nodeRowsList primitiveSteps).Nodupnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPorthLeft:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRight:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
  induction primitiveSteps with
  | nil =>nilnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPorthUnique:(nodeRowsList []).NoduphLeft:PrimitiveGraphStep.node node entries₁ exits₁ ∈ []hRight:PrimitiveGraphStep.node node entries₂ exits₂ ∈ []⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
      cases hLeftAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphLeft:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStep :: primitiveStepshRight:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStep :: primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
      simp at hLeft hRightconsnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphLeft:PrimitiveGraphStep.node node entries₁ exits₁ = primitiveStep ∨
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRight:PrimitiveGraphStep.node node entries₂ exits₂ = primitiveStep ∨
  PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
      cases hLeft with
      | inl hLeftHead =>cons.inlnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphRight:PrimitiveGraphStep.node node entries₂ exits₂ = primitiveStep ∨
  PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshLeftHead:PrimitiveGraphStep.node node entries₁ exits₁ = primitiveStep⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
          cases hLeftHeadcons.inl.reflnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRight:PrimitiveGraphStep.node node entries₂ exits₂ = PrimitiveGraphStep.node node entries₁ exits₁ ∨
  PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
          cases hRight with
          | inl hRightHead =>cons.inl.refl.inlnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRightHead:PrimitiveGraphStep.node node entries₂ exits₂ = PrimitiveGraphStep.node node entries₁ exits₁⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              cases hRightHeadcons.inl.refl.inl.reflnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStephUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).Nodupih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps → entries₁ = entries₁ ∧ exits₁ = exits₁⊢ entries₁ = entries₁ ∧ exits₁ = exits₁
              exact ⟨rfl, rfl⟩All goals completed! 🐙
          | inr hRightTail =>cons.inl.refl.inrnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              have hRightNode :=
                nodeRowsList_mem_of_node_mem hRightTailcons.inl.refl.inrnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshRightNode:node ∈ nodeRowsList primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              have hNoTail : node ∉ nodeRowsList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStephUnique:(nodeRowsList primitiveSteps).Nodupnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPorthLeft:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRight:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
                have hUniqueHead := hUniquenode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshRightNode:node ∈ nodeRowsList primitiveStepshUniqueHead:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).Nodup⊢ node ∉ nodeRowsList primitiveSteps
                simp [nodeRowsList, nodeRows] at hUniqueHeadnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₁ exits₁ :: primitiveSteps)).NoduphRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshRightNode:node ∈ nodeRowsList primitiveStepshUniqueHead:node ∉ nodeRowsList primitiveSteps ∧ (nodeRowsList primitiveSteps).Nodup⊢ node ∉ nodeRowsList primitiveSteps
                exact hUniqueHead.leftAll goals completed! 🐙
              exact False.elim (hNoTail hRightNode)All goals completed! 🐙
      | inr hLeftTail =>cons.inrnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphRight:PrimitiveGraphStep.node node entries₂ exits₂ = primitiveStep ∨
  PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
          cases hRight with
          | inl hRightHead =>cons.inr.inlnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightHead:PrimitiveGraphStep.node node entries₂ exits₂ = primitiveStep⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              cases hRightHeadcons.inr.inl.reflnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₂ exits₂ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              have hLeftNode :=
                nodeRowsList_mem_of_node_mem hLeftTailcons.inr.inl.reflnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₂ exits₂ :: primitiveSteps)).NoduphLeftNode:node ∈ nodeRowsList primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              have hNoTail : node ∉ nodeRowsList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStephUnique:(nodeRowsList primitiveSteps).Nodupnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPorthLeft:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRight:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
                have hUniqueHead := hUniquenode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₂ exits₂ :: primitiveSteps)).NoduphLeftNode:node ∈ nodeRowsList primitiveStepshUniqueHead:(nodeRowsList (PrimitiveGraphStep.node node entries₂ exits₂ :: primitiveSteps)).Nodup⊢ node ∉ nodeRowsList primitiveSteps
                simp [nodeRowsList, nodeRows] at hUniqueHeadnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshUnique:(nodeRowsList (PrimitiveGraphStep.node node entries₂ exits₂ :: primitiveSteps)).NoduphLeftNode:node ∈ nodeRowsList primitiveStepshUniqueHead:node ∉ nodeRowsList primitiveSteps ∧ (nodeRowsList primitiveSteps).Nodup⊢ node ∉ nodeRowsList primitiveSteps
                exact hUniqueHead.leftAll goals completed! 🐙
              exact False.elim (hNoTail hLeftNode)All goals completed! 🐙
          | inr hRightTail =>cons.inr.inrnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hUnique:(nodeRowsList (primitiveStep :: primitiveSteps)).NoduphLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              cases primitiveStepcons.inr.inr.emptynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshUnique:(nodeRowsList (empty :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.nodenode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsnode✝:NodeIdentries✝:List AdmissionBoundaryPortexits✝:List AdmissionBoundaryPorthUnique:(nodeRowsList (PrimitiveGraphStep.node node✝ entries✝ exits✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.bindingRefnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsbinding✝:BindingNamehUnique:(nodeRowsList (bindingRef binding✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.overlaynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftNodes✝:List NodeIdrightNodes✝:List NodeIdleftBindings✝:List BindingNamerightBindings✝:List BindingNamehUnique:(nodeRowsList (overlay leftNodes✝ rightNodes✝ leftBindings✝ rightBindings✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.connectnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftExits✝:List AdmissionBoundaryPortrightEntries✝:List AdmissionBoundaryPortmatchedPairs✝:List AdmissionConnectionunmatchedLeftExits✝:List AdmissionBoundaryPortunmatchedRightEntries✝:List AdmissionBoundaryPorthUnique:(nodeRowsList
    (connect leftExits✝ rightEntries✝ matchedPairs✝ unmatchedLeftExits✝ unmatchedRightEntries✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ <;>cons.inr.inr.emptynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshUnique:(nodeRowsList (empty :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.nodenode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsnode✝:NodeIdentries✝:List AdmissionBoundaryPortexits✝:List AdmissionBoundaryPorthUnique:(nodeRowsList (PrimitiveGraphStep.node node✝ entries✝ exits✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.bindingRefnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsbinding✝:BindingNamehUnique:(nodeRowsList (bindingRef binding✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.overlaynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftNodes✝:List NodeIdrightNodes✝:List NodeIdleftBindings✝:List BindingNamerightBindings✝:List BindingNamehUnique:(nodeRowsList (overlay leftNodes✝ rightNodes✝ leftBindings✝ rightBindings✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂cons.inr.inr.connectnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftExits✝:List AdmissionBoundaryPortrightEntries✝:List AdmissionBoundaryPortmatchedPairs✝:List AdmissionConnectionunmatchedLeftExits✝:List AdmissionBoundaryPortunmatchedRightEntries✝:List AdmissionBoundaryPorthUnique:(nodeRowsList
    (connect leftExits✝ rightEntries✝ matchedPairs✝ unmatchedLeftExits✝ unmatchedRightEntries✝ :: primitiveSteps)).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ simp [nodeRowsList, nodeRows] at hUniquecons.inr.inr.connectnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftExits✝:List AdmissionBoundaryPortrightEntries✝:List AdmissionBoundaryPortmatchedPairs✝:List AdmissionConnectionunmatchedLeftExits✝:List AdmissionBoundaryPortunmatchedRightEntries✝:List AdmissionBoundaryPorthUnique:(nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂
              ·cons.inr.inr.emptynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepshUnique:(nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ exact ih hUnique hLeftTail hRightTailAll goals completed! 🐙
              ·cons.inr.inr.nodenode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsnode✝:NodeIdentries✝:List AdmissionBoundaryPortexits✝:List AdmissionBoundaryPorthUnique:node✝ ∉ nodeRowsList primitiveSteps ∧ (nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ exact ih hUnique.right hLeftTail hRightTailAll goals completed! 🐙
              ·cons.inr.inr.bindingRefnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsbinding✝:BindingNamehUnique:(nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ exact ih hUnique hLeftTail hRightTailAll goals completed! 🐙
              ·cons.inr.inr.overlaynode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftNodes✝:List NodeIdrightNodes✝:List NodeIdleftBindings✝:List BindingNamerightBindings✝:List BindingNamehUnique:(nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ exact ih hUnique hLeftTail hRightTailAll goals completed! 🐙
              ·cons.inr.inr.connectnode:NodeIdentries₁:List AdmissionBoundaryPortexits₁:List AdmissionBoundaryPortentries₂:List AdmissionBoundaryPortexits₂:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:(nodeRowsList primitiveSteps).Nodup →
  PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveSteps →
    PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveSteps → entries₁ = entries₂ ∧ exits₁ = exits₂hLeftTail:PrimitiveGraphStep.node node entries₁ exits₁ ∈ primitiveStepshRightTail:PrimitiveGraphStep.node node entries₂ exits₂ ∈ primitiveStepsleftExits✝:List AdmissionBoundaryPortrightEntries✝:List AdmissionBoundaryPortmatchedPairs✝:List AdmissionConnectionunmatchedLeftExits✝:List AdmissionBoundaryPortunmatchedRightEntries✝:List AdmissionBoundaryPorthUnique:(nodeRowsList primitiveSteps).Nodup⊢ entries₁ = entries₂ ∧ exits₁ = exits₂ exact ih hUnique hLeftTail hRightTailAll goals completed! 🐙

Primitive node entry boundary keys projected from a list of trace rows.

def nodeEntryKeysList :
    List PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.nodeEntryKeys ++ nodeEntryKeysList primitiveSteps

Primitive node exit boundary keys projected from a list of trace rows.

def nodeExitKeysList :
    List PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.nodeExitKeys ++ nodeExitKeysList primitiveSteps

Input boundary keys consumed by a list of primitive connect rows.

def consumedEntryKeysList :
    List PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.consumedEntryKeys ++ consumedEntryKeysList primitiveSteps

Output boundary keys consumed by a list of primitive connect rows.

def consumedExitKeysList :
    List PrimitiveGraphStep → List (NodeId × FieldLabel × ContractId)
  | [] => []
  | primitiveStep :: primitiveSteps =>
      primitiveStep.consumedExitKeys ++ consumedExitKeysList primitiveSteps

Matched connection rows contribute their target keys to consumed entry keys.

theorem matchedConnectionsList_toKey_mem_consumedEntryKeysList
    {connection : AdmissionConnection}
    {primitiveSteps : List PrimitiveGraphStep}
    (hConnection :
      connection ∈ matchedConnectionsList primitiveSteps) :
    connection.toKey ∈ consumedEntryKeysList primitiveSteps := byconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStephConnection:connection ∈ matchedConnectionsList primitiveSteps⊢ connection.toKey ∈ consumedEntryKeysList primitiveSteps
  induction primitiveSteps with
  | nil =>nilconnection:AdmissionConnectionhConnection:connection ∈ matchedConnectionsList []⊢ connection.toKey ∈ consumedEntryKeysList []
      cases hConnectionAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consconnection:AdmissionConnectionprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepshConnection:connection ∈ matchedConnectionsList (primitiveStep :: primitiveSteps)⊢ connection.toKey ∈ consumedEntryKeysList (primitiveStep :: primitiveSteps)
      cases primitiveStep with
      | empty =>cons.emptyconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepshConnection:connection ∈ matchedConnectionsList (empty :: primitiveSteps)⊢ connection.toKey ∈ consumedEntryKeysList (empty :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | node node entries exits =>cons.nodeconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthConnection:connection ∈ matchedConnectionsList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)⊢ connection.toKey ∈ consumedEntryKeysList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | bindingRef binding =>cons.bindingRefconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsbinding:BindingNamehConnection:connection ∈ matchedConnectionsList (bindingRef binding :: primitiveSteps)⊢ connection.toKey ∈ consumedEntryKeysList (bindingRef binding :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlayconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehConnection:connection ∈ matchedConnectionsList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)⊢ connection.toKey ∈ consumedEntryKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | connect leftExits rightEntries matchedPairs unmatchedLeftExits
          unmatchedRightEntries =>cons.connectconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthConnection:connection ∈
  matchedConnectionsList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)⊢ connection.toKey ∈
  consumedEntryKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections, consumedEntryKeysList,
            consumedEntryKeys] at hConnection ⊢cons.connectconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthConnection:connection ∈ matchedPairs ∨ connection ∈ matchedConnectionsList primitiveSteps⊢ (∃ a ∈ matchedPairs, a.toKey = connection.toKey) ∨ connection.toKey ∈ consumedEntryKeysList primitiveSteps
          cases hConnection with
          | inl hPair =>cons.connect.inlconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthPair:connection ∈ matchedPairs⊢ (∃ a ∈ matchedPairs, a.toKey = connection.toKey) ∨ connection.toKey ∈ consumedEntryKeysList primitiveSteps
              exact Or.inl ⟨connection, hPair, rfl⟩All goals completed! 🐙
          | inr hRest =>cons.connect.inrconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.toKey ∈ consumedEntryKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthRest:connection ∈ matchedConnectionsList primitiveSteps⊢ (∃ a ∈ matchedPairs, a.toKey = connection.toKey) ∨ connection.toKey ∈ consumedEntryKeysList primitiveSteps
              exact Or.inr (ih hRest)All goals completed! 🐙

Matched connection rows contribute their source keys to consumed exit keys.

theorem matchedConnectionsList_fromKey_mem_consumedExitKeysList
    {connection : AdmissionConnection}
    {primitiveSteps : List PrimitiveGraphStep}
    (hConnection :
      connection ∈ matchedConnectionsList primitiveSteps) :
    connection.fromKey ∈ consumedExitKeysList primitiveSteps := byconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStephConnection:connection ∈ matchedConnectionsList primitiveSteps⊢ connection.fromKey ∈ consumedExitKeysList primitiveSteps
  induction primitiveSteps with
  | nil =>nilconnection:AdmissionConnectionhConnection:connection ∈ matchedConnectionsList []⊢ connection.fromKey ∈ consumedExitKeysList []
      cases hConnectionAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consconnection:AdmissionConnectionprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepshConnection:connection ∈ matchedConnectionsList (primitiveStep :: primitiveSteps)⊢ connection.fromKey ∈ consumedExitKeysList (primitiveStep :: primitiveSteps)
      cases primitiveStep with
      | empty =>cons.emptyconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepshConnection:connection ∈ matchedConnectionsList (empty :: primitiveSteps)⊢ connection.fromKey ∈ consumedExitKeysList (empty :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | node node entries exits =>cons.nodeconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthConnection:connection ∈ matchedConnectionsList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)⊢ connection.fromKey ∈ consumedExitKeysList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | bindingRef binding =>cons.bindingRefconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsbinding:BindingNamehConnection:connection ∈ matchedConnectionsList (bindingRef binding :: primitiveSteps)⊢ connection.fromKey ∈ consumedExitKeysList (bindingRef binding :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlayconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehConnection:connection ∈ matchedConnectionsList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)⊢ connection.fromKey ∈ consumedExitKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          exact ih hConnectionAll goals completed! 🐙
      | connect leftExits rightEntries matchedPairs unmatchedLeftExits
          unmatchedRightEntries =>cons.connectconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthConnection:connection ∈
  matchedConnectionsList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)⊢ connection.fromKey ∈
  consumedExitKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections, consumedExitKeysList,
            consumedExitKeys] at hConnection ⊢cons.connectconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthConnection:connection ∈ matchedPairs ∨ connection ∈ matchedConnectionsList primitiveSteps⊢ (∃ a ∈ matchedPairs, a.fromKey = connection.fromKey) ∨ connection.fromKey ∈ consumedExitKeysList primitiveSteps
          cases hConnection with
          | inl hPair =>cons.connect.inlconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthPair:connection ∈ matchedPairs⊢ (∃ a ∈ matchedPairs, a.fromKey = connection.fromKey) ∨ connection.fromKey ∈ consumedExitKeysList primitiveSteps
              exact Or.inl ⟨connection, hPair, rfl⟩All goals completed! 🐙
          | inr hRest =>cons.connect.inrconnection:AdmissionConnectionprimitiveSteps:List PrimitiveGraphStepih:connection ∈ matchedConnectionsList primitiveSteps → connection.fromKey ∈ consumedExitKeysList primitiveStepsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthRest:connection ∈ matchedConnectionsList primitiveSteps⊢ (∃ a ∈ matchedPairs, a.fromKey = connection.fromKey) ∨ connection.fromKey ∈ consumedExitKeysList primitiveSteps
              exact Or.inr (ih hRest)All goals completed! 🐙

Matched pairs from a primitive connect row appear in the global matched-pair ledger.

theorem matchedConnectionsList_mem_of_connect_mem
    {primitiveSteps : List PrimitiveGraphStep}
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    {pair : AdmissionConnection}
    (hStep :
      PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
        primitiveSteps)
    (hPair : pair ∈ matchedPairs) :
    pair ∈ matchedConnectionsList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStepleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveStepshPair:pair ∈ matchedPairs⊢ pair ∈ matchedConnectionsList primitiveSteps
  induction primitiveSteps with
  | nil =>nilleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairshStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ []⊢ pair ∈ matchedConnectionsList []
      cases hStepAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepshStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveStep :: primitiveSteps⊢ pair ∈ matchedConnectionsList (primitiveStep :: primitiveSteps)
      cases primitiveStep with
      | empty =>cons.emptyleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepshStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ empty :: primitiveSteps⊢ pair ∈ matchedConnectionsList (empty :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections] at hStep ⊢cons.emptyleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepshStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedConnectionsList primitiveSteps
          exact ih hStepAll goals completed! 🐙
      | node node entries exits =>cons.nodeleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  PrimitiveGraphStep.node node entries exits :: primitiveSteps⊢ pair ∈ matchedConnectionsList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections] at hStep ⊢cons.nodeleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedConnectionsList primitiveSteps
          exact ih hStepAll goals completed! 🐙
      | bindingRef binding =>cons.bindingRefleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsbinding:BindingNamehStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  bindingRef binding :: primitiveSteps⊢ pair ∈ matchedConnectionsList (bindingRef binding :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections] at hStep ⊢cons.bindingRefleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsbinding:BindingNamehStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedConnectionsList primitiveSteps
          exact ih hStepAll goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlayleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps⊢ pair ∈ matchedConnectionsList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections] at hStep ⊢cons.overlayleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedConnectionsList primitiveSteps
          exact ih hStepAll goals completed! 🐙
      | connect leftExits' rightEntries' matchedPairs' unmatchedLeftExits'
          unmatchedRightEntries' =>cons.connectleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftExits':List AdmissionBoundaryPortrightEntries':List AdmissionBoundaryPortmatchedPairs':List AdmissionConnectionunmatchedLeftExits':List AdmissionBoundaryPortunmatchedRightEntries':List AdmissionBoundaryPorthStep:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  connect leftExits' rightEntries' matchedPairs' unmatchedLeftExits' unmatchedRightEntries' :: primitiveSteps⊢ pair ∈
  matchedConnectionsList
    (connect leftExits' rightEntries' matchedPairs' unmatchedLeftExits' unmatchedRightEntries' :: primitiveSteps)
          simp [matchedConnectionsList, matchedConnections] at hStep ⊢cons.connectleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftExits':List AdmissionBoundaryPortrightEntries':List AdmissionBoundaryPortmatchedPairs':List AdmissionConnectionunmatchedLeftExits':List AdmissionBoundaryPortunmatchedRightEntries':List AdmissionBoundaryPorthStep:leftExits = leftExits' ∧
    rightEntries = rightEntries' ∧
      matchedPairs = matchedPairs' ∧
        unmatchedLeftExits = unmatchedLeftExits' ∧ unmatchedRightEntries = unmatchedRightEntries' ∨
  connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedPairs' ∨ pair ∈ matchedConnectionsList primitiveSteps
          cases hStep with
          | inl hHead =>cons.connect.inlleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftExits':List AdmissionBoundaryPortrightEntries':List AdmissionBoundaryPortmatchedPairs':List AdmissionConnectionunmatchedLeftExits':List AdmissionBoundaryPortunmatchedRightEntries':List AdmissionBoundaryPorthHead:leftExits = leftExits' ∧
  rightEntries = rightEntries' ∧
    matchedPairs = matchedPairs' ∧
      unmatchedLeftExits = unmatchedLeftExits' ∧ unmatchedRightEntries = unmatchedRightEntries'⊢ pair ∈ matchedPairs' ∨ pair ∈ matchedConnectionsList primitiveSteps
              rcases hHead with ⟨rfl, rfl, rfl, rfl, rfl⟩cons.connect.inlleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveSteps⊢ pair ∈ matchedPairs ∨ pair ∈ matchedConnectionsList primitiveSteps
              exact Or.inl hPairAll goals completed! 🐙
          | inr hTail =>cons.connect.inrleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortpair:AdmissionConnectionhPair:pair ∈ matchedPairsprimitiveSteps:List PrimitiveGraphStepih:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps →
  pair ∈ matchedConnectionsList primitiveStepsleftExits':List AdmissionBoundaryPortrightEntries':List AdmissionBoundaryPortmatchedPairs':List AdmissionConnectionunmatchedLeftExits':List AdmissionBoundaryPortunmatchedRightEntries':List AdmissionBoundaryPorthTail:connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈ primitiveSteps⊢ pair ∈ matchedPairs' ∨ pair ∈ matchedConnectionsList primitiveSteps
              exact Or.inr (ih hTail)All goals completed! 🐙

Validator obligations for a serialized primitive node row.

structure NodeValid
    (nodeId : NodeId)
    (entries exits : List AdmissionBoundaryPort) : Prop where
  nodeValid : nodeId.Valid
  entriesValid : BoundaryPortsValid entries
  exitsValid : BoundaryPortsValid exits
  frontiersOwned : NodeFrontiersOwned nodeId entries exits
  frontiersLinear : NodeFrontiersLinear entries exits

Validator obligations for a serialized primitive overlay row.

structure OverlayValid
    (leftNodeIds rightNodeIds : List NodeId)
    (leftBindings rightBindings : List BindingName) : Prop where
  leftNodesValid : ∀ node, node ∈ leftNodeIds → node.Valid
  rightNodesValid : ∀ node, node ∈ rightNodeIds → node.Valid
  leftBindingsValid : ∀ binding, binding ∈ leftBindings → binding.Valid
  rightBindingsValid : ∀ binding, binding ∈ rightBindings → binding.Valid
  ledgersUnique : OverlayLedgersUnique leftNodeIds rightNodeIds leftBindings rightBindings
  ledgersDisjoint : OverlayLedgersDisjoint leftNodeIds rightNodeIds leftBindings rightBindings

Validator obligations for a serialized primitive connect row.

structure ConnectValid
    (leftExits rightEntries : List AdmissionBoundaryPort)
    (matchedPairs : List AdmissionConnection)
    (unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort) : Prop where
  pairsDrawnFromFrontiers :
    ∀ pair, pair ∈ matchedPairs → pair.fromPort ∈ leftExits ∧ pair.toPort ∈ rightEntries
  unmatchedLeftDrawnFromFrontier :
    ∀ boundary, boundary ∈ unmatchedLeftExits → boundary ∈ leftExits
  unmatchedRightDrawnFromFrontier :
    ∀ boundary, boundary ∈ unmatchedRightEntries → boundary ∈ rightEntries
  pairsLinear : ConnectPairsLinear matchedPairs
  frontiersLinear : ConnectFrontiersLinear leftExits rightEntries
  matchesAllCompatible : ConnectMatchesAllCompatible leftExits rightEntries matchedPairs
  frontierPartition :
    ConnectFrontierPartition
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries
  rowsValid :
    ConnectRowsValid
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries

Row-level validator obligation for primitive graph steps.

The primitive artifact is still a trace row, not a CertifiedGraph. For connect, the local check is that every matched pair and every unmatched endpoint is drawn from the frontiers serialized in the same row, and that the matched/unmatched rows partition each frontier exactly.

def Valid : PrimitiveGraphStep → Prop
  | .empty => True
  | .node nodeId entries exits =>
      NodeValid nodeId entries exits
  | PrimitiveGraphStep.bindingRef binding => binding.Valid
  | PrimitiveGraphStep.overlay leftNodeIds rightNodeIds leftBindings rightBindings =>
      OverlayValid leftNodeIds rightNodeIds leftBindings rightBindings
  | PrimitiveGraphStep.connect
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries =>
      ConnectValid leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries

Primitive graph-step rows mention only nodes and binding references in the top-level summary.

def DomainClosed
    (nodes : List NodeId)
    (bindingRefs : List BindingName) :
    PrimitiveGraphStep → Prop
  | .empty => True
  | .node nodeId entries exits =>
      nodeId ∈ nodes ∧
      BoundaryPortsClosed nodes entries ∧
      BoundaryPortsClosed nodes exits
  | PrimitiveGraphStep.bindingRef binding => binding ∈ bindingRefs
  | PrimitiveGraphStep.overlay leftNodeIds rightNodeIds leftBindings rightBindings =>
      (∀ node, node ∈ leftNodeIds → node ∈ nodes) ∧
      (∀ node, node ∈ rightNodeIds → node ∈ nodes) ∧
      (∀ binding, binding ∈ leftBindings → binding ∈ bindingRefs) ∧
      (∀ binding, binding ∈ rightBindings → binding ∈ bindingRefs)
  | PrimitiveGraphStep.connect
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries =>
      BoundaryPortsClosed nodes leftExits ∧
      BoundaryPortsClosed nodes rightEntries ∧
      ConnectionsClosed nodes matchedPairs ∧
      BoundaryPortsClosed nodes unmatchedLeftExits ∧
      BoundaryPortsClosed nodes unmatchedRightEntries

Valid primitive overlay rows expose left/right ledger disjointness.

theorem valid_overlay_ledgersDisjoint
    {leftNodes rightNodes : List NodeId}
    {leftBindings rightBindings : List BindingName}
    (hValid :
      (PrimitiveGraphStep.overlay
        leftNodes rightNodes leftBindings rightBindings).Valid) :
    OverlayLedgersDisjoint leftNodes rightNodes leftBindings rightBindings :=
  hValid.ledgersDisjoint

Valid primitive overlay rows expose duplicate-free side ledgers.

theorem valid_overlay_ledgersUnique
    {leftNodes rightNodes : List NodeId}
    {leftBindings rightBindings : List BindingName}
    (hValid :
      (PrimitiveGraphStep.overlay
        leftNodes rightNodes leftBindings rightBindings).Valid) :
    OverlayLedgersUnique leftNodes rightNodes leftBindings rightBindings :=
  hValid.ledgersUnique

Valid primitive connect rows expose left/right frontier membership for each match.

theorem valid_connect_pair_mem
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid)
    {pair : AdmissionConnection}
    (hPair : pair ∈ matchedPairs) :
    pair.fromPort ∈ leftExits ∧ pair.toPort ∈ rightEntries :=
  hValid.pairsDrawnFromFrontiers pair hPair

Valid primitive connect rows do not reuse matched output or input endpoints.

theorem valid_connect_pairsLinear
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid) :
    ConnectPairsLinear matchedPairs :=
  hValid.pairsLinear

Valid primitive connect rows expose duplicate-free serialized frontiers.

theorem valid_connect_frontiersLinear
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid) :
    ConnectFrontiersLinear leftExits rightEntries :=
  hValid.frontiersLinear

Valid primitive connect rows expose exact matched/unmatched frontier partitioning.

theorem valid_connect_frontierPartition
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid) :
    ConnectFrontierPartition
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :=
  hValid.frontierPartition

Valid primitive connect rows match every compatible left/right frontier pair.

theorem valid_connect_matchesAllCompatible
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid) :
    ConnectMatchesAllCompatible leftExits rightEntries matchedPairs :=
  hValid.matchesAllCompatible

Valid primitive connect rows expose structural validity of serialized row endpoints.

theorem valid_connect_rowsValid
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hValid :
      (PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries).Valid) :
    ConnectRowsValid
      leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :=
  hValid.rowsValid

end PrimitiveGraphStepend AdmissionArtifactend Cortex.Wire