Cortex.Wire.Planner.Construction

proofs

On this page

Overview
Context
Theorem Split
Runtime-Style Node Namespacing
Relation Endpoint Closure
Anchor Membership
Constructed Planned Delta

Imports

import Cortex.Wire.Planner
import Mathlib.Data.List.Basic

Overview

Runtime-shaped construction for Wire rewrite admission.

Context

Cortex.Wire.Planner names the proof contract established by executable planning. This module moves one step closer to the runtime: it defines a concrete namespaced-node model, constructs a proof-side planned delta from the relation-level planner model, and proves that the constructed delta supplies the bulk of RuntimePlannerConstruction.

The theorem surface remains denotational. The constructed graph topology is a non-extractable Graph representative for the finite planned relation; correctness is stated as denote topology = plannedFinalRelation ..., not raw AST equality. The executable runtime computes its own topology and must establish denotational equality to this representative.

Theorem Split

The page first records relation endpoint-closure lemmas needed to realize planned relations as graphs. It then defines runtime-style namespaced node ids and finally constructs planned deltas whose topology, diff sets, definitions, entry/exit sets, and costs are definitionally tied to the planner model.

namespace Cortex.Wireopen Cortex.Graph

Runtime-Style Node Namespacing

RuntimeNodeId models executable node ids as namespace segments.

The Haskell runtime serializes the same shape as colon-delimited Text. Keeping segments structured in Lean makes delimiter-freedom explicit: a local inserted id is a single non-empty segment containing no reserved delimiter, and namespacing appends that segment below the anchor path. Fixed-anchor injectivity is the only namespace theorem carried by the policy; disjointness across different anchors is established by per-rewrite freshness against the current topology.

structure RuntimeNodeId where

Namespace path segments.

  segments : List String
  deriving DecidableEq, Repr

namespace RuntimeNodeId

Runtime namespace delimiter mirrored from the Haskell NodeId encoding.

def namespaceDelimiter : Char :=
  ':'

segmentAllowed segment mirrors the executable local-node syntax check.

def segmentAllowed (segment : String) : Prop :=
  segment.isEmpty = false ∧ segment.contains namespaceDelimiter = false

A local inserted node id is one non-empty segment with no namespace delimiter.

def localAllowed (node : RuntimeNodeId) : Prop :=
  ∃ segment, node.segments = [segment] ∧ segmentAllowed segment

Namespace a local inserted node under an anchor.

def namespaceNode (anchor localNode : RuntimeNodeId) : RuntimeNodeId :=
  { segments := anchor.segments ++ localNode.segments }

Fixed-anchor namespacing is injective.

theorem namespaceNode_injective (anchor : RuntimeNodeId) :
    Function.Injective (namespaceNode anchor) := byanchor:RuntimeNodeId⊢ Function.Injective anchor.namespaceNode
  intro left rightanchor:RuntimeNodeIdleft:RuntimeNodeIdright:RuntimeNodeId⊢ anchor.namespaceNode left = anchor.namespaceNode right → left = right hNamespacedanchor:RuntimeNodeIdleft:RuntimeNodeIdright:RuntimeNodeIdhNamespaced:anchor.namespaceNode left = anchor.namespaceNode right⊢ left = right
  cases left with
  | mk leftSegments =>mkanchor:RuntimeNodeIdright:RuntimeNodeIdleftSegments:List StringhNamespaced:anchor.namespaceNode { segments := leftSegments } = anchor.namespaceNode right⊢ { segments := leftSegments } = right
      cases right with
      | mk rightSegments =>mk.mkanchor:RuntimeNodeIdleftSegments:List StringrightSegments:List StringhNamespaced:anchor.namespaceNode { segments := leftSegments } = anchor.namespaceNode { segments := rightSegments }⊢ { segments := leftSegments } = { segments := rightSegments }
          cases anchor with
          | mk anchorSegments =>mk.mk.mkleftSegments:List StringrightSegments:List StringanchorSegments:List StringhNamespaced:{ segments := anchorSegments }.namespaceNode { segments := leftSegments } =
  { segments := anchorSegments }.namespaceNode { segments := rightSegments }⊢ { segments := leftSegments } = { segments := rightSegments }
              have hSegments :
                  anchorSegments ++ leftSegments = anchorSegments ++ rightSegments :=
                congrArg RuntimeNodeId.segments hNamespacedmk.mk.mkleftSegments:List StringrightSegments:List StringanchorSegments:List StringhNamespaced:{ segments := anchorSegments }.namespaceNode { segments := leftSegments } =
  { segments := anchorSegments }.namespaceNode { segments := rightSegments }hSegments:anchorSegments ++ leftSegments = anchorSegments ++ rightSegments⊢ { segments := leftSegments } = { segments := rightSegments }
              have hLocalSegments : leftSegments = rightSegments :=
                List.append_right_injective anchorSegments hSegmentsmk.mk.mkleftSegments:List StringrightSegments:List StringanchorSegments:List StringhNamespaced:{ segments := anchorSegments }.namespaceNode { segments := leftSegments } =
  { segments := anchorSegments }.namespaceNode { segments := rightSegments }hSegments:anchorSegments ++ leftSegments = anchorSegments ++ rightSegmentshLocalSegments:leftSegments = rightSegments⊢ { segments := leftSegments } = { segments := rightSegments }
              cases hLocalSegmentsmk.mk.mk.reflleftSegments:List StringanchorSegments:List StringhNamespaced:{ segments := anchorSegments }.namespaceNode { segments := leftSegments } =
  { segments := anchorSegments }.namespaceNode { segments := leftSegments }hSegments:anchorSegments ++ leftSegments = anchorSegments ++ leftSegments⊢ { segments := leftSegments } = { segments := leftSegments }
              rflAll goals completed! 🐙

The concrete runtime namespace policy for structured node ids.

def namespacePolicy : RuntimeNamespacePolicy RuntimeNodeId :=
  { namespaceNode := namespaceNode
    localAllowed := localAllowed
    namespaceNode_injective := namespaceNode_injective }

end RuntimeNodeId

Relation Endpoint Closure

section EndpointClosurevariable {node : Type}variable [DecidableEq node]

Relation overlay preserves endpoint closure.

theorem relation_edgeEndpoints_overlay
    {left right : Relation node}
    (hLeft : Relation.EdgeEndpointsInVertices left)
    (hRight : Relation.EdgeEndpointsInVertices right) :
    Relation.EdgeEndpointsInVertices (Relation.overlay left right) := bynode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.overlay right).EdgeEndpointsInVertices
  intro edge hEdgenode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ (left.overlay right).edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices
  simp only [Relation.overlay, Finset.mem_union] at hEdge ⊢node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ left.edges ∨ edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)
  rcases hEdge with hEdge | hEdgeinlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ left.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)
  ·inlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ left.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) exact ⟨Or.inl (hLeft edge hEdge).1, Or.inl (hLeft edge hEdge).2⟩All goals completed! 🐙
  ·inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) exact ⟨Or.inr (hRight edge hEdge).1, Or.inr (hRight edge hEdge).2⟩All goals completed! 🐙

Relation connect preserves endpoint closure.

theorem relation_edgeEndpoints_connect
    {left right : Relation node}
    (hLeft : Relation.EdgeEndpointsInVertices left)
    (hRight : Relation.EdgeEndpointsInVertices right) :
    Relation.EdgeEndpointsInVertices (Relation.connect left right) := bynode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.connect right).EdgeEndpointsInVertices
  intro edge hEdgenode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ (left.connect right).edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
  simp only [Relation.connect, Relation.cross, Finset.mem_union, Finset.mem_product] at hEdge ⊢node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:(edge ∈ left.edges ∨ edge ∈ right.edges) ∨ edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)
  rcases hEdge with hOldEdge | hCrossinlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehOldEdge:edge ∈ left.edges ∨ edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehCross:edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)
  ·inlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehOldEdge:edge ∈ left.edges ∨ edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) rcases hOldEdge with hEdge | hEdgeinl.inlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ left.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)inl.inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices)
    ·inl.inlnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ left.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) exact ⟨Or.inl (hLeft edge hEdge).1, Or.inl (hLeft edge hEdge).2⟩All goals completed! 🐙
    ·inl.inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ right.edges⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) exact ⟨Or.inr (hRight edge hEdge).1, Or.inr (hRight edge hEdge).2⟩All goals completed! 🐙
  ·inrnode:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodehLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:node × nodehCross:edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ (edge.1 ∈ left.vertices ∨ edge.1 ∈ right.vertices) ∧ (edge.2 ∈ left.vertices ∨ edge.2 ∈ right.vertices) exact ⟨Or.inl hCross.1, Or.inr hCross.2⟩All goals completed! 🐙

Denotations of graph expressions are endpoint-closed relations.

theorem denote_edgeEndpointsInVertices (g : Graph node) :
    Relation.EdgeEndpointsInVertices (denote g) := bynode:Typeinst✝:DecidableEq nodeg:Graph node⊢ (denote g).EdgeEndpointsInVertices
  induction g with
  | empty =>emptynode:Typeinst✝:DecidableEq node⊢ (denote Graph.empty).EdgeEndpointsInVertices
      intro edge hEdgeemptynode:Typeinst✝:DecidableEq nodeedge:node × nodehEdge:edge ∈ (denote Graph.empty).edges⊢ edge.1 ∈ (denote Graph.empty).vertices ∧ edge.2 ∈ (denote Graph.empty).vertices
      simp only [denote_empty, Relation.empty, Finset.notMem_empty] at hEdgeAll goals completed! 🐙
  | vertex vertex =>vertexnode:Typeinst✝:DecidableEq nodevertex:node⊢ (denote (Graph.vertex vertex)).EdgeEndpointsInVertices
      intro edge hEdgevertexnode:Typeinst✝:DecidableEq nodevertex:nodeedge:node × nodehEdge:edge ∈ (denote (Graph.vertex vertex)).edges⊢ edge.1 ∈ (denote (Graph.vertex vertex)).vertices ∧ edge.2 ∈ (denote (Graph.vertex vertex)).vertices
      simp only [denote_vertex, Relation.vertex, Finset.notMem_empty] at hEdgeAll goals completed! 🐙
  | overlay left right left_ih right_ih =>overlaynode:Typeinst✝:DecidableEq nodeleft:Graph noderight:Graph nodeleft_ih:(denote left).EdgeEndpointsInVerticesright_ih:(denote right).EdgeEndpointsInVertices⊢ (denote (left.overlay right)).EdgeEndpointsInVertices
      rw [denote_overlay]overlaynode:Typeinst✝:DecidableEq nodeleft:Graph noderight:Graph nodeleft_ih:(denote left).EdgeEndpointsInVerticesright_ih:(denote right).EdgeEndpointsInVertices⊢ ((denote left).overlay (denote right)).EdgeEndpointsInVertices
      exact relation_edgeEndpoints_overlay left_ih right_ihAll goals completed! 🐙
  | connect left right left_ih right_ih =>connectnode:Typeinst✝:DecidableEq nodeleft:Graph noderight:Graph nodeleft_ih:(denote left).EdgeEndpointsInVerticesright_ih:(denote right).EdgeEndpointsInVertices⊢ (denote (left.connect right)).EdgeEndpointsInVertices
      rw [denote_connect]connectnode:Typeinst✝:DecidableEq nodeleft:Graph noderight:Graph nodeleft_ih:(denote left).EdgeEndpointsInVerticesright_ih:(denote right).EdgeEndpointsInVertices⊢ ((denote left).connect (denote right)).EdgeEndpointsInVertices
      exact relation_edgeEndpoints_connect left_ih right_ihAll goals completed! 🐙

Removing one vertex and its incident edges preserves endpoint closure.

theorem relation_edgeEndpoints_removeVertex
    {relation : Relation node}
    {vertex : node}
    (hRelation : Relation.EdgeEndpointsInVertices relation) :
    Relation.EdgeEndpointsInVertices (removeVertexFromRelation relation vertex) := bynode:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVertices⊢ (removeVertexFromRelation relation vertex).EdgeEndpointsInVertices
  intro edge hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ (removeVertexFromRelation relation vertex).edges⊢ edge.1 ∈ (removeVertexFromRelation relation vertex).vertices ∧
  edge.2 ∈ (removeVertexFromRelation relation vertex).vertices
  simp only [removeVertexFromRelation, Finset.mem_filter, Finset.mem_erase] at hEdge ⊢node:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ relation.edges ∧ edge.1 ≠ vertex ∧ edge.2 ≠ vertex⊢ (edge.1 ≠ vertex ∧ edge.1 ∈ relation.vertices) ∧ edge.2 ≠ vertex ∧ edge.2 ∈ relation.vertices
  rcases hEdge with ⟨hOldEdge, hSourceNe, hTargetNe⟩node:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVerticesedge:node × nodehOldEdge:edge ∈ relation.edgeshSourceNe:edge.1 ≠ vertexhTargetNe:edge.2 ≠ vertex⊢ (edge.1 ≠ vertex ∧ edge.1 ∈ relation.vertices) ∧ edge.2 ≠ vertex ∧ edge.2 ∈ relation.vertices
  exact ⟨⟨hSourceNe, (hRelation edge hOldEdge).1⟩, ⟨hTargetNe, (hRelation edge hOldEdge).2⟩⟩All goals completed! 🐙

Removing outgoing edges preserves endpoint closure.

theorem relation_edgeEndpoints_removeOutgoing
    {relation : Relation node}
    {vertex : node}
    (hRelation : Relation.EdgeEndpointsInVertices relation) :
    Relation.EdgeEndpointsInVertices (removeOutgoingFromRelation relation vertex) := bynode:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVertices⊢ (removeOutgoingFromRelation relation vertex).EdgeEndpointsInVertices
  intro edge hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ (removeOutgoingFromRelation relation vertex).edges⊢ edge.1 ∈ (removeOutgoingFromRelation relation vertex).vertices ∧
  edge.2 ∈ (removeOutgoingFromRelation relation vertex).vertices
  simp only [removeOutgoingFromRelation, Finset.mem_filter] at hEdge ⊢node:Typeinst✝:DecidableEq noderelation:Relation nodevertex:nodehRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ relation.edges ∧ edge.1 ≠ vertex⊢ edge.1 ∈ relation.vertices ∧ edge.2 ∈ relation.vertices
  exact hRelation edge hEdge.1All goals completed! 🐙

Adding edges while also adding their endpoints preserves endpoint closure.

theorem relation_edgeEndpoints_addEdges
    {relation : Relation node}
    {edges : Finset (node × node)}
    (hRelation : Relation.EdgeEndpointsInVertices relation) :
    Relation.EdgeEndpointsInVertices (addEdgesToRelation relation edges) := bynode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVertices⊢ (addEdgesToRelation relation edges).EdgeEndpointsInVertices
  intro edge hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ (addEdgesToRelation relation edges).edges⊢ edge.1 ∈ (addEdgesToRelation relation edges).vertices ∧ edge.2 ∈ (addEdgesToRelation relation edges).vertices
  simp only [addEdgesToRelation, Finset.mem_union] at hEdge ⊢node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehEdge:edge ∈ relation.edges ∨ edge ∈ edges⊢ ((edge.1 ∈ relation.vertices ∨ edge.1 ∈ Finset.image Prod.fst edges) ∨ edge.1 ∈ Finset.image Prod.snd edges) ∧
  ((edge.2 ∈ relation.vertices ∨ edge.2 ∈ Finset.image Prod.fst edges) ∨ edge.2 ∈ Finset.image Prod.snd edges)
  rcases hEdge with hOldEdge | hAddedEdgeinlnode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehOldEdge:edge ∈ relation.edges⊢ ((edge.1 ∈ relation.vertices ∨ edge.1 ∈ Finset.image Prod.fst edges) ∨ edge.1 ∈ Finset.image Prod.snd edges) ∧
  ((edge.2 ∈ relation.vertices ∨ edge.2 ∈ Finset.image Prod.fst edges) ∨ edge.2 ∈ Finset.image Prod.snd edges)inrnode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehAddedEdge:edge ∈ edges⊢ ((edge.1 ∈ relation.vertices ∨ edge.1 ∈ Finset.image Prod.fst edges) ∨ edge.1 ∈ Finset.image Prod.snd edges) ∧
  ((edge.2 ∈ relation.vertices ∨ edge.2 ∈ Finset.image Prod.fst edges) ∨ edge.2 ∈ Finset.image Prod.snd edges)
  ·inlnode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehOldEdge:edge ∈ relation.edges⊢ ((edge.1 ∈ relation.vertices ∨ edge.1 ∈ Finset.image Prod.fst edges) ∨ edge.1 ∈ Finset.image Prod.snd edges) ∧
  ((edge.2 ∈ relation.vertices ∨ edge.2 ∈ Finset.image Prod.fst edges) ∨ edge.2 ∈ Finset.image Prod.snd edges) exact
      ⟨ Or.inl (Or.inl (hRelation edge hOldEdge).1)
      , Or.inl (Or.inl (hRelation edge hOldEdge).2)
      ⟩All goals completed! 🐙
  ·inrnode:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node × node)hRelation:relation.EdgeEndpointsInVerticesedge:node × nodehAddedEdge:edge ∈ edges⊢ ((edge.1 ∈ relation.vertices ∨ edge.1 ∈ Finset.image Prod.fst edges) ∨ edge.1 ∈ Finset.image Prod.snd edges) ∧
  ((edge.2 ∈ relation.vertices ∨ edge.2 ∈ Finset.image Prod.fst edges) ∨ edge.2 ∈ Finset.image Prod.snd edges) exact
      ⟨ Or.inl (Or.inr (Finset.mem_image.mpr ⟨edge, hAddedEdge, rfl⟩))
      , Or.inr (Finset.mem_image.mpr ⟨edge, hAddedEdge, rfl⟩)
      ⟩All goals completed! 🐙

The relation-level planner construction always produces an endpoint-closed relation.

theorem plannedFinalRelation_edgeEndpointsInVertices
    (context : Graph node)
    (rewrite : GraphRewrite node) :
    Relation.EdgeEndpointsInVertices (plannedFinalRelation context rewrite) := bynode:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite node⊢ (plannedFinalRelation context rewrite).EdgeEndpointsInVertices
  cases rewrite with
  | expandNode anchor mode spec =>expandNodenode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodemode:ExpansionModespec:SubgraphSpec node⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor mode spec)).EdgeEndpointsInVertices
      cases mode with
      | replaceNode =>expandNode.replaceNodenode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).EdgeEndpointsInVertices
          simp only
            [ plannedFinalRelation
            , GraphRewrite.anchor
            , GraphRewrite.spec
            , GraphRewrite.anchorDisposition
            ]expandNode.replaceNodenode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (addEdgesToRelation
    (addEdgesToRelation ((removeVertexFromRelation (denote context) anchor).overlay (denote spec.topology))
      (predecessorsOf (denote context) anchor ×ˢ spec.entryNodes))
    (spec.exitNodes ×ˢ successorsOf (denote context) anchor)).EdgeEndpointsInVertices
          exact
            relation_edgeEndpoints_addEdges
              (relation_edgeEndpoints_addEdges
                (relation_edgeEndpoints_overlay
                  (relation_edgeEndpoints_removeVertex (denote_edgeEndpointsInVertices context))
                  (denote_edgeEndpointsInVertices spec.topology)))All goals completed! 🐙
      | retainNodeAsEnvelope =>expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (plannedFinalRelation context
    (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).EdgeEndpointsInVertices
          simp only
            [ plannedFinalRelation
            , GraphRewrite.anchor
            , GraphRewrite.spec
            , GraphRewrite.anchorDisposition
            ]expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (addEdgesToRelation
    (addEdgesToRelation ((removeOutgoingFromRelation (denote context) anchor).overlay (denote spec.topology))
      ({anchor} ×ˢ spec.entryNodes))
    (spec.exitNodes ×ˢ successorsOf (denote context) anchor)).EdgeEndpointsInVertices
          exact
            relation_edgeEndpoints_addEdges
              (relation_edgeEndpoints_addEdges
                (relation_edgeEndpoints_overlay
                  (relation_edgeEndpoints_removeOutgoing (denote_edgeEndpointsInVertices context))
                  (denote_edgeEndpointsInVertices spec.topology)))All goals completed! 🐙
  | appendAfter anchor spec =>appendAfternode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).EdgeEndpointsInVertices
      simp only
        [ plannedFinalRelation
        , GraphRewrite.anchor
        , GraphRewrite.spec
        , GraphRewrite.anchorDisposition
        ]appendAfternode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec node⊢ (addEdgesToRelation
    (addEdgesToRelation ((removeOutgoingFromRelation (denote context) anchor).overlay (denote spec.topology))
      ({anchor} ×ˢ spec.entryNodes))
    (spec.exitNodes ×ˢ successorsOf (denote context) anchor)).EdgeEndpointsInVertices
      exact
        relation_edgeEndpoints_addEdges
          (relation_edgeEndpoints_addEdges
            (relation_edgeEndpoints_overlay
              (relation_edgeEndpoints_removeOutgoing (denote_edgeEndpointsInVertices context))
              (denote_edgeEndpointsInVertices spec.topology)))All goals completed! 🐙

end EndpointClosure

Anchor Membership

section AnchorMembershipvariable {node : Type}variable [DecidableEq node]

Acyclic source topologies have no direct self-loop at the rewrite anchor.

theorem anchor_noSelfLoop_of_acyclic
    {context : Graph node}
    {anchor : node}
    (hSourceAcyclic : Acyclic context) :
    (anchor, anchor) ∉ (denote context).edges := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodehSourceAcyclic:Acyclic context⊢ (anchor, anchor) ∉ (denote context).edges
  intro hLoopnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodehSourceAcyclic:Acyclic contexthLoop:(anchor, anchor) ∈ (denote context).edges⊢ False
  exact hSourceAcyclic anchor (GraphPath.direct hLoop)All goals completed! 🐙

Without a self-loop, an anchor is not its own direct predecessor.

theorem anchor_not_mem_predecessorsOf_of_noSelfLoop
    {relation : Relation node}
    {anchor : node}
    (hNoSelfLoop : (anchor, anchor) ∉ relation.edges) :
    anchor ∉ predecessorsOf relation anchor := bynode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edges⊢ anchor ∉ predecessorsOf relation anchor
  intro hPrednode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgeshPred:anchor ∈ predecessorsOf relation anchor⊢ False
  simp only [predecessorsOf, Finset.mem_image, Finset.mem_filter] at hPrednode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgeshPred:∃ a, (a ∈ relation.edges ∧ a.2 = anchor) ∧ a.1 = anchor⊢ False
  rcases hPred with ⟨edge, hEdge, hSource⟩node:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgesedge:node × nodehEdge:edge ∈ relation.edges ∧ edge.2 = anchorhSource:edge.1 = anchor⊢ False
  rcases edge with ⟨source, target⟩node:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodetarget:nodehEdge:(source, target) ∈ relation.edges ∧ (source, target).2 = anchorhSource:(source, target).1 = anchor⊢ False
  simp only at hSourcenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodetarget:nodehEdge:(source, target) ∈ relation.edges ∧ (source, target).2 = anchorhSource:source = anchor⊢ False
  subst sourcenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgestarget:nodehEdge:(anchor, target) ∈ relation.edges ∧ (anchor, target).2 = anchor⊢ False
  simp only at hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgestarget:nodehEdge:(anchor, target) ∈ relation.edges ∧ target = anchor⊢ False
  rw [hEdge.2] at hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgestarget:nodehEdge:(anchor, anchor) ∈ relation.edges ∧ anchor = anchor⊢ False
  exact hNoSelfLoop hEdge.1All goals completed! 🐙

Without a self-loop, an anchor is not its own direct successor.

theorem anchor_not_mem_successorsOf_of_noSelfLoop
    {relation : Relation node}
    {anchor : node}
    (hNoSelfLoop : (anchor, anchor) ∉ relation.edges) :
    anchor ∉ successorsOf relation anchor := bynode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edges⊢ anchor ∉ successorsOf relation anchor
  intro hSuccnode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgeshSucc:anchor ∈ successorsOf relation anchor⊢ False
  simp only [successorsOf, Finset.mem_image, Finset.mem_filter] at hSuccnode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgeshSucc:∃ a, (a ∈ relation.edges ∧ a.1 = anchor) ∧ a.2 = anchor⊢ False
  rcases hSucc with ⟨edge, hEdge, hTarget⟩node:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgesedge:node × nodehEdge:edge ∈ relation.edges ∧ edge.1 = anchorhTarget:edge.2 = anchor⊢ False
  rcases edge with ⟨source, target⟩node:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodetarget:nodehEdge:(source, target) ∈ relation.edges ∧ (source, target).1 = anchorhTarget:(source, target).2 = anchor⊢ False
  simp only at hTargetnode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodetarget:nodehEdge:(source, target) ∈ relation.edges ∧ (source, target).1 = anchorhTarget:target = anchor⊢ False
  subst targetnode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodehEdge:(source, anchor) ∈ relation.edges ∧ (source, anchor).1 = anchor⊢ False
  simp only at hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodehEdge:(source, anchor) ∈ relation.edges ∧ source = anchor⊢ False
  rw [hEdge.2] at hEdgenode:Typeinst✝:DecidableEq noderelation:Relation nodeanchor:nodehNoSelfLoop:(anchor, anchor) ∉ relation.edgessource:nodehEdge:(anchor, anchor) ∈ relation.edges ∧ anchor = anchor⊢ False
  exact hNoSelfLoop hEdge.1All goals completed! 🐙

Direct predecessors of a denoted graph node are vertices of the denoted graph.

theorem predecessorsOf_mem_vertices
    {context : Graph node}
    {target predecessor : node}
    (hPredecessor : predecessor ∈ predecessorsOf (denote context) target) :
    predecessor ∈ (denote context).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodepredecessor:nodehPredecessor:predecessor ∈ predecessorsOf (denote context) target⊢ predecessor ∈ (denote context).vertices
  simp only [predecessorsOf, Finset.mem_image, Finset.mem_filter] at hPredecessornode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodepredecessor:nodehPredecessor:∃ a, (a ∈ (denote context).edges ∧ a.2 = target) ∧ a.1 = predecessor⊢ predecessor ∈ (denote context).vertices
  rcases hPredecessor with ⟨edge, hEdge, hSource⟩node:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodepredecessor:nodeedge:node × nodehEdge:edge ∈ (denote context).edges ∧ edge.2 = targethSource:edge.1 = predecessor⊢ predecessor ∈ (denote context).vertices
  rcases edge with ⟨source, target⟩node:Typeinst✝:DecidableEq nodecontext:Graph nodetarget✝:nodepredecessor:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote context).edges ∧ (source, target).2 = target✝hSource:(source, target).1 = predecessor⊢ predecessor ∈ (denote context).vertices
  simp only at hSourcenode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget✝:nodepredecessor:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote context).edges ∧ (source, target).2 = target✝hSource:source = predecessor⊢ predecessor ∈ (denote context).vertices
  subst sourcenode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget✝:nodepredecessor:nodetarget:nodehEdge:(predecessor, target) ∈ (denote context).edges ∧ (predecessor, target).2 = target✝⊢ predecessor ∈ (denote context).vertices
  exact (denote_edgeEndpointsInVertices context (predecessor, target) hEdge.1).1All goals completed! 🐙

Direct successors of a denoted graph node are vertices of the denoted graph.

theorem successorsOf_mem_vertices
    {context : Graph node}
    {target successor : node}
    (hSuccessor : successor ∈ successorsOf (denote context) target) :
    successor ∈ (denote context).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodesuccessor:nodehSuccessor:successor ∈ successorsOf (denote context) target⊢ successor ∈ (denote context).vertices
  simp only [successorsOf, Finset.mem_image, Finset.mem_filter] at hSuccessornode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodesuccessor:nodehSuccessor:∃ a, (a ∈ (denote context).edges ∧ a.1 = target) ∧ a.2 = successor⊢ successor ∈ (denote context).vertices
  rcases hSuccessor with ⟨edge, hEdge, hTarget⟩node:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodesuccessor:nodeedge:node × nodehEdge:edge ∈ (denote context).edges ∧ edge.1 = targethTarget:edge.2 = successor⊢ successor ∈ (denote context).vertices
  rcases edge with ⟨source, target⟩node:Typeinst✝:DecidableEq nodecontext:Graph nodetarget✝:nodesuccessor:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote context).edges ∧ (source, target).1 = target✝hTarget:(source, target).2 = successor⊢ successor ∈ (denote context).vertices
  simp only at hTargetnode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget✝:nodesuccessor:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote context).edges ∧ (source, target).1 = target✝hTarget:target = successor⊢ successor ∈ (denote context).vertices
  subst targetnode:Typeinst✝:DecidableEq nodecontext:Graph nodetarget:nodesuccessor:nodesource:nodehEdge:(source, successor) ∈ (denote context).edges ∧ (source, successor).1 = target⊢ successor ∈ (denote context).vertices
  exact (denote_edgeEndpointsInVertices context (source, successor) hEdge.1).2All goals completed! 🐙

Replacement rewrites have exactly old-minus-anchor plus inserted final vertices.

theorem plannedFinalRelation_vertices_replace
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hNoSelfLoop : (anchor, anchor) ∉ (denote context).edges)
    (hEntryInside : NodesInside spec.entryNodes spec.topology)
    (hExitInside : NodesInside spec.exitNodes spec.topology) :
    (plannedFinalRelation context
      (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
        (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
  (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
  apply Finset.exthnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ ∀ (a : node),
  a ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices ↔
    a ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
  intro nodehnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices ↔
  node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
  constructorh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices →
  node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).verticesh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices →
  node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
  ·h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices →
  node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices intro hFinalh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices⊢ node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeVertexFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_erase
      , Finset.mem_image
      , Finset.mem_product
      ] at hFinal ⊢h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    rcases hFinal with (((hBaseOrInserted | hEntrySource) | hEntryTarget) | hExitSource) |
      hExitTargeth.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    ·h.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hBaseOrInserted with hBase | hInsertedh.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ≠ anchor ∧ node ∈ (denote context).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      ·h.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ≠ anchor ∧ node ∈ (denote context).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inl hBaseAll goals completed! 🐙
      ·h.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inr hInsertedAll goals completed! 🐙
    ·h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntrySource with ⟨edge, hEdge, hSource⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ predecessorsOf (denote context) anchor ∧ edge.2 ∈ spec.entryNodeshSource:edge.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨source, _entry⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:(source, _entry).1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSourceh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hPredecessor : node ∈ predecessorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
  (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
        simpa only [hSource] using hEdge.1All goals completed! 🐙
      have hNodeNeAnchor : node ≠ anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
  (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
        intro hNodeEqnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehPredecessor:node ∈ predecessorsOf (denote context) anchorhNodeEq:node = anchor⊢ False
        rw [hNodeEq] at hPredecessornode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehPredecessor:anchor ∈ predecessorsOf (denote context) anchorhNodeEq:node = anchor⊢ False
        exact anchor_not_mem_predecessorsOf_of_noSelfLoop hNoSelfLoop hPredecessorAll goals completed! 🐙
      exact Or.inl ⟨hNodeNeAnchor, predecessorsOf_mem_vertices hPredecessor⟩All goals completed! 🐙
    ·h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntryTarget with ⟨edge, hEdge, hEntry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ predecessorsOf (denote context) anchor ∧ edge.2 ∈ spec.entryNodeshEntry:edge.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_source, entry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:(_source, entry).2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hEntryh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hEntry]h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ entry ≠ anchor ∧ entry ∈ (denote context).vertices ∨ entry ∈ (denote spec.topology).vertices
      exact Or.inr (hEntryInside entry hEdge.2)All goals completed! 🐙
    ·h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitSource with ⟨edge, hEdge, hExit⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhExit:edge.1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨exit, _successor⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:(exit, _successor).1 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hExith.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hExit]h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ exit ≠ anchor ∧ exit ∈ (denote context).vertices ∨ exit ∈ (denote spec.topology).vertices
      exact Or.inr (hExitInside exit hEdge.1)All goals completed! 🐙
    ·h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitTarget with ⟨edge, hEdge, hSuccessor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhSuccessor:edge.2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_exit, successor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:(_exit, successor).2 = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSuccessorh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = node⊢ node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hSuccessorMem : node ∈ successorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
  (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
        simpa only [hSuccessor] using hEdge.2All goals completed! 🐙
      have hNodeNeAnchor : node ≠ anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices =
  (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices
        intro hNodeEqnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = nodehSuccessorMem:node ∈ successorsOf (denote context) anchorhNodeEq:node = anchor⊢ False
        rw [hNodeEq] at hSuccessorMemnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = nodehSuccessorMem:anchor ∈ successorsOf (denote context) anchorhNodeEq:node = anchor⊢ False
        exact anchor_not_mem_successorsOf_of_noSelfLoop hNoSelfLoop hSuccessorMemAll goals completed! 🐙
      exact Or.inl ⟨hNodeNeAnchor, successorsOf_mem_vertices hSuccessorMem⟩All goals completed! 🐙
  ·h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices →
  node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices intro hUnionh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ∈ (denote context).vertices.erase anchor ∪ (denote spec.topology).vertices⊢ node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeVertexFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_erase
      , Finset.mem_image
      , Finset.mem_product
      ] at hUnion ⊢h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ ((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    rcases hUnion with hBase | hInsertedh.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ≠ anchor ∧ node ∈ (denote context).vertices⊢ ((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = nodeh.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    ·h.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ≠ anchor ∧ node ∈ (denote context).vertices⊢ ((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inl hBase))))All goals completed! 🐙
    ·h.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ≠ anchor ∧ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inr hInserted))))All goals completed! 🐙

Retained-envelope rewrites have old plus inserted final vertices.

theorem plannedFinalRelation_vertices_retain
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hAnchorInTopology : anchor ∈ (denote context).vertices)
    (hEntryInside : NodesInside spec.entryNodes spec.topology)
    (hExitInside : NodesInside spec.exitNodes spec.topology) :
    (plannedFinalRelation context
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices =
        (denote context).vertices ∪ (denote spec.topology).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
  apply Finset.exthnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ ∀ (a : node),
  a ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices ↔
    a ∈ (denote context).vertices ∪ (denote spec.topology).vertices
  intro nodehnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈
    (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices ↔
  node ∈ (denote context).vertices ∪ (denote spec.topology).vertices
  constructorh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈
    (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices →
  node ∈ (denote context).vertices ∪ (denote spec.topology).verticesh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices →
  node ∈
    (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
  ·h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈
    (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices →
  node ∈ (denote context).vertices ∪ (denote spec.topology).vertices intro hFinalh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeOutgoingFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_singleton
      , Finset.mem_image
      , Finset.mem_product
      ] at hFinal ⊢h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    rcases hFinal with (((hBaseOrInserted | hEntrySource) | hEntryTarget) | hExitSource) |
      hExitTargeth.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    ·h.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hBaseOrInserted with hBase | hInsertedh.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      ·h.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inl hBaseAll goals completed! 🐙
      ·h.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inr hInsertedAll goals completed! 🐙
    ·h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntrySource with ⟨edge, hEdge, hSource⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 = anchor ∧ edge.2 ∈ spec.entryNodeshSource:edge.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨source, _entry⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:(source, _entry).1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSourceh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hSourceAnchor : source = anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
        simpa only [Finset.mem_singleton] using hEdge.1All goals completed! 🐙
      rw [← hSource]h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehSourceAnchor:source = anchor⊢ source ∈ (denote context).vertices ∨ source ∈ (denote spec.topology).vertices
      rw [hSourceAnchor]h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehSourceAnchor:source = anchor⊢ anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices
      exact Or.inl hAnchorInTopologyAll goals completed! 🐙
    ·h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntryTarget with ⟨edge, hEdge, hEntry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 = anchor ∧ edge.2 ∈ spec.entryNodeshEntry:edge.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_source, entry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:(_source, entry).2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hEntryh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hEntry]h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ entry ∈ (denote context).vertices ∨ entry ∈ (denote spec.topology).vertices
      exact Or.inr (hEntryInside entry hEdge.2)All goals completed! 🐙
    ·h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitSource with ⟨edge, hEdge, hExit⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhExit:edge.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨exit, _successor⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:(exit, _successor).1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hExith.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hExit]h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ exit ∈ (denote context).vertices ∨ exit ∈ (denote spec.topology).vertices
      exact Or.inr (hExitInside exit hEdge.1)All goals completed! 🐙
    ·h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitTarget with ⟨edge, hEdge, hSuccessor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhSuccessor:edge.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_exit, successor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:(_exit, successor).2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSuccessorh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hSuccessorMem : node ∈ successorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
        simpa only [hSuccessor] using hEdge.2All goals completed! 🐙
      exact Or.inl (successorsOf_mem_vertices hSuccessorMem)All goals completed! 🐙
  ·h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices →
  node ∈
    (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices intro hUnionh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ∈ (denote context).vertices ∪ (denote spec.topology).vertices⊢ node ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeOutgoingFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_singleton
      , Finset.mem_image
      , Finset.mem_product
      ] at hUnion ⊢h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    rcases hUnion with hBase | hInsertedh.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = nodeh.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    ·h.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inl hBase))))All goals completed! 🐙
    ·h.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inr hInserted))))All goals completed! 🐙

Append-after rewrites have old plus inserted final vertices.

theorem plannedFinalRelation_vertices_append
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hAnchorInTopology : anchor ∈ (denote context).vertices)
    (hEntryInside : NodesInside spec.entryNodes spec.topology)
    (hExitInside : NodesInside spec.exitNodes spec.topology) :
    (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices =
        (denote context).vertices ∪ (denote spec.topology).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
  apply Finset.exthnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ ∀ (a : node),
  a ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices ↔
    a ∈ (denote context).vertices ∪ (denote spec.topology).vertices
  intro nodehnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices ↔
  node ∈ (denote context).vertices ∪ (denote spec.topology).vertices
  constructorh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices →
  node ∈ (denote context).vertices ∪ (denote spec.topology).verticesh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices →
  node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices
  ·h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices →
  node ∈ (denote context).vertices ∪ (denote spec.topology).vertices intro hFinalh.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeOutgoingFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_singleton
      , Finset.mem_image
      , Finset.mem_product
      ] at hFinal ⊢h.mpnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hFinal:((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    rcases hFinal with (((hBaseOrInserted | hEntrySource) | hEntryTarget) | hExitSource) |
      hExitTargeth.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
    ·h.mp.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBaseOrInserted:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hBaseOrInserted with hBase | hInsertedh.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).verticesh.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      ·h.mp.inl.inl.inl.inl.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inl hBaseAll goals completed! 🐙
      ·h.mp.inl.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices exact Or.inr hInsertedAll goals completed! 🐙
    ·h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntrySource:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntrySource with ⟨edge, hEdge, hSource⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 = anchor ∧ edge.2 ∈ spec.entryNodeshSource:edge.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨source, _entry⟩h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:(source, _entry).1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSourceh.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hSourceAnchor : source = anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
        simpa only [Finset.mem_singleton] using hEdge.1All goals completed! 🐙
      rw [← hSource]h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehSourceAnchor:source = anchor⊢ source ∈ (denote context).vertices ∨ source ∈ (denote spec.topology).vertices
      rw [hSourceAnchor]h.mp.inl.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝source:node_entry:nodehEdge:(source, _entry).1 = anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = nodehSourceAnchor:source = anchor⊢ anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices
      exact Or.inl hAnchorInTopologyAll goals completed! 🐙
    ·h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hEntryTarget:∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hEntryTarget with ⟨edge, hEdge, hEntry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 = anchor ∧ edge.2 ∈ spec.entryNodeshEntry:edge.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_source, entry⟩h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:(_source, entry).2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hEntryh.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hEntry]h.mp.inl.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_source:nodeentry:nodehEdge:(_source, entry).1 = anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = node⊢ entry ∈ (denote context).vertices ∨ entry ∈ (denote spec.topology).vertices
      exact Or.inr (hEntryInside entry hEdge.2)All goals completed! 🐙
    ·h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitSource with ⟨edge, hEdge, hExit⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhExit:edge.1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨exit, _successor⟩h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:(exit, _successor).1 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hExith.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rw [← hExit]h.mp.inl.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝exit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = node⊢ exit ∈ (denote context).vertices ∨ exit ∈ (denote spec.topology).vertices
      exact Or.inr (hExitInside exit hEdge.1)All goals completed! 🐙
    ·h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices rcases hExitTarget with ⟨edge, hEdge, hSuccessor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝edge:node✝ × node✝hEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhSuccessor:edge.2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      rcases edge with ⟨_exit, successor⟩h.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:(_exit, successor).2 = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      simp only at hSuccessorh.mp.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = node⊢ node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices
      have hSuccessorMem : node ∈ successorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices =
  (denote context).vertices ∪ (denote spec.topology).vertices
        simpa only [hSuccessor] using hEdge.2All goals completed! 🐙
      exact Or.inl (successorsOf_mem_vertices hSuccessorMem)All goals completed! 🐙
  ·h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝⊢ node ∈ (denote context).vertices ∪ (denote spec.topology).vertices →
  node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices intro hUnionh.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ∈ (denote context).vertices ∪ (denote spec.topology).vertices⊢ node ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices
    simp only
      [ plannedFinalRelation
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      , removeOutgoingFromRelation
      , addEdgesToRelation
      , Relation.overlay
      , Finset.mem_union
      , Finset.mem_singleton
      , Finset.mem_image
      , Finset.mem_product
      ] at hUnion ⊢h.mprnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hUnion:node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    rcases hUnion with hBase | hInsertedh.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = nodeh.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node
    ·h.mpr.inlnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hBase:node ∈ (denote context).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inl hBase))))All goals completed! 🐙
    ·h.mpr.inrnode✝:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorInTopology:anchor ∈ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologynode:node✝hInserted:node ∈ (denote spec.topology).vertices⊢ ((((node ∈ (denote context).vertices ∨ node ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = node) ∨
      ∃ a, (a.1 = anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = node) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = node) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = node exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inr hInserted))))All goals completed! 🐙

A replacement rewrite removes the anchor when the old topology has no anchor self-loop.

theorem anchor_not_mem_plannedFinalRelation_replace
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hAnchorIn : anchor ∈ (denote context).vertices)
    (hNoSelfLoop : (anchor, anchor) ∉ (denote context).edges)
    (hFresh :
      ∀ mappedNode,
        mappedNode ∈ (denote spec.topology).vertices →
          mappedNode ∉ (denote context).vertices)
    (hEntryInside : NodesInside spec.entryNodes spec.topology)
    (hExitInside : NodesInside spec.exitNodes spec.topology) :
    anchor ∉
      (plannedFinalRelation context
        (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ anchor ∉ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
  intro hFinalnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhFinal:anchor ∈ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices⊢ False
  simp only
    [ plannedFinalRelation
    , GraphRewrite.anchor
    , GraphRewrite.spec
    , GraphRewrite.anchorDisposition
    , removeVertexFromRelation
    , addEdgesToRelation
    , Relation.overlay
    , Finset.mem_union
    , Finset.mem_erase
    , Finset.mem_image
    , Finset.mem_product
    ] at hFinalnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhFinal:((((anchor ≠ anchor ∧ anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices) ∨
        ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = anchor) ∨
      ∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = anchor) ∨
    ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = anchor) ∨
  ∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = anchor⊢ False
  rcases hFinal with (((hBaseOrInserted | hEntrySource) | hEntryTarget) | hExitSource) |
    hExitTargetinl.inl.inl.inlnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhBaseOrInserted:anchor ≠ anchor ∧ anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices⊢ Falseinl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhEntrySource:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = anchor⊢ Falseinl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhEntryTarget:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = anchor⊢ Falseinl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = anchor⊢ Falseinrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = anchor⊢ False
  ·inl.inl.inl.inlnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhBaseOrInserted:anchor ≠ anchor ∧ anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices⊢ False rcases hBaseOrInserted with hBase | hInsertedinl.inl.inl.inl.inlnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhBase:anchor ≠ anchor ∧ anchor ∈ (denote context).vertices⊢ Falseinl.inl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhInserted:anchor ∈ (denote spec.topology).vertices⊢ False
    ·inl.inl.inl.inl.inlnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhBase:anchor ≠ anchor ∧ anchor ∈ (denote context).vertices⊢ False exact hBase.1 rflAll goals completed! 🐙
    ·inl.inl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhInserted:anchor ∈ (denote spec.topology).vertices⊢ False exact hFresh anchor hInserted hAnchorInAll goals completed! 🐙
  ·inl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhEntrySource:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.1 = anchor⊢ False rcases hEntrySource with ⟨edge, hEdge, hSource⟩inl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyedge:node × nodehEdge:edge.1 ∈ predecessorsOf (denote context) anchor ∧ edge.2 ∈ spec.entryNodeshSource:edge.1 = anchor⊢ False
    rcases edge with ⟨source, _entry⟩inl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologysource:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:(source, _entry).1 = anchor⊢ False
    simp only at hSourceinl.inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologysource:node_entry:nodehEdge:(source, _entry).1 ∈ predecessorsOf (denote context) anchor ∧ (source, _entry).2 ∈ spec.entryNodeshSource:source = anchor⊢ False
    have hPred : anchor ∈ predecessorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ anchor ∉ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
      simpa only [hSource] using hEdge.1All goals completed! 🐙
    exact anchor_not_mem_predecessorsOf_of_noSelfLoop hNoSelfLoop hPredAll goals completed! 🐙
  ·inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhEntryTarget:∃ a, (a.1 ∈ predecessorsOf (denote context) anchor ∧ a.2 ∈ spec.entryNodes) ∧ a.2 = anchor⊢ False rcases hEntryTarget with ⟨edge, hEdge, hEntry⟩inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyedge:node × nodehEdge:edge.1 ∈ predecessorsOf (denote context) anchor ∧ edge.2 ∈ spec.entryNodeshEntry:edge.2 = anchor⊢ False
    rcases edge with ⟨_source, entry⟩inl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:(_source, entry).2 = anchor⊢ False
    simp only at hEntryinl.inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = anchor⊢ False
    have hEntryOld : entry ∈ (denote context).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ anchor ∉ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
      rw [hEntry]node:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology_source:nodeentry:nodehEdge:(_source, entry).1 ∈ predecessorsOf (denote context) anchor ∧ (_source, entry).2 ∈ spec.entryNodeshEntry:entry = anchor⊢ anchor ∈ (denote context).vertices
      exact hAnchorInAll goals completed! 🐙
    exact hFresh entry (hEntryInside entry hEdge.2) hEntryOldAll goals completed! 🐙
  ·inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhExitSource:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.1 = anchor⊢ False rcases hExitSource with ⟨edge, hEdge, hExit⟩inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyedge:node × nodehEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhExit:edge.1 = anchor⊢ False
    rcases edge with ⟨exit, _successor⟩inl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyexit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:(exit, _successor).1 = anchor⊢ False
    simp only at hExitinl.inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyexit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = anchor⊢ False
    have hExitOld : exit ∈ (denote context).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ anchor ∉ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
      rw [hExit]node:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyexit:node_successor:nodehEdge:(exit, _successor).1 ∈ spec.exitNodes ∧ (exit, _successor).2 ∈ successorsOf (denote context) anchorhExit:exit = anchor⊢ anchor ∈ (denote context).vertices
      exact hAnchorInAll goals completed! 🐙
    exact hFresh exit (hExitInside exit hEdge.1) hExitOldAll goals completed! 🐙
  ·inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyhExitTarget:∃ a, (a.1 ∈ spec.exitNodes ∧ a.2 ∈ successorsOf (denote context) anchor) ∧ a.2 = anchor⊢ False rcases hExitTarget with ⟨edge, hEdge, hSuccessor⟩inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topologyedge:node × nodehEdge:edge.1 ∈ spec.exitNodes ∧ edge.2 ∈ successorsOf (denote context) anchorhSuccessor:edge.2 = anchor⊢ False
    rcases edge with ⟨_exit, successor⟩inrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:(_exit, successor).2 = anchor⊢ False
    simp only at hSuccessorinrnode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology_exit:nodesuccessor:nodehEdge:(_exit, successor).1 ∈ spec.exitNodes ∧ (_exit, successor).2 ∈ successorsOf (denote context) anchorhSuccessor:successor = anchor⊢ False
    have hSucc : anchor ∈ successorsOf (denote context) anchor := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).verticeshNoSelfLoop:(anchor, anchor) ∉ (denote context).edgeshFresh:∀ mappedNode ∈ (denote spec.topology).vertices, mappedNode ∉ (denote context).verticeshEntryInside:NodesInside spec.entryNodes spec.topologyhExitInside:NodesInside spec.exitNodes spec.topology⊢ anchor ∉ (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
      simpa only [hSuccessor] using hEdge.2All goals completed! 🐙
    exact anchor_not_mem_successorsOf_of_noSelfLoop hNoSelfLoop hSuccAll goals completed! 🐙

A retained-envelope rewrite keeps the anchor in the planned final relation.

theorem anchor_mem_plannedFinalRelation_retain
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hAnchorIn : anchor ∈ (denote context).vertices) :
    anchor ∈
      (plannedFinalRelation context
        (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).vertices⊢ anchor ∈
  (plannedFinalRelation context (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
  simp only
    [ plannedFinalRelation
    , GraphRewrite.anchor
    , GraphRewrite.spec
    , GraphRewrite.anchorDisposition
    , removeOutgoingFromRelation
    , addEdgesToRelation
    , Relation.overlay
    , Finset.mem_union
    ]node:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).vertices⊢ ((((anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices) ∨
        anchor ∈ Finset.image Prod.fst ({anchor} ×ˢ spec.entryNodes)) ∨
      anchor ∈ Finset.image Prod.snd ({anchor} ×ˢ spec.entryNodes)) ∨
    anchor ∈ Finset.image Prod.fst (spec.exitNodes ×ˢ successorsOf (denote context) anchor)) ∨
  anchor ∈ Finset.image Prod.snd (spec.exitNodes ×ˢ successorsOf (denote context) anchor)
  exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inl hAnchorIn))))All goals completed! 🐙

An append-after rewrite keeps the anchor in the planned final relation.

theorem anchor_mem_plannedFinalRelation_append
    {context : Graph node}
    {anchor : node}
    {spec : SubgraphSpec node}
    (hAnchorIn : anchor ∈ (denote context).vertices) :
    anchor ∈
      (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices := bynode:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).vertices⊢ anchor ∈ (plannedFinalRelation context (GraphRewrite.appendAfter anchor spec)).vertices
  simp only
    [ plannedFinalRelation
    , GraphRewrite.anchor
    , GraphRewrite.spec
    , GraphRewrite.anchorDisposition
    , removeOutgoingFromRelation
    , addEdgesToRelation
    , Relation.overlay
    , Finset.mem_union
    ]node:Typeinst✝:DecidableEq nodecontext:Graph nodeanchor:nodespec:SubgraphSpec nodehAnchorIn:anchor ∈ (denote context).vertices⊢ ((((anchor ∈ (denote context).vertices ∨ anchor ∈ (denote spec.topology).vertices) ∨
        anchor ∈ Finset.image Prod.fst ({anchor} ×ˢ spec.entryNodes)) ∨
      anchor ∈ Finset.image Prod.snd ({anchor} ×ˢ spec.entryNodes)) ∨
    anchor ∈ Finset.image Prod.fst (spec.exitNodes ×ˢ successorsOf (denote context) anchor)) ∨
  anchor ∈ Finset.image Prod.snd (spec.exitNodes ×ˢ successorsOf (denote context) anchor)
  exact Or.inl (Or.inl (Or.inl (Or.inl (Or.inl hAnchorIn))))All goals completed! 🐙

end AnchorMembership

Constructed Planned Delta

section ConstructedDeltavariable {node : Type}variable [DecidableEq node]

Relation computed by the runtime-shaped planner after namespacing.

def constructedFinalRelation
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node) :
    Relation node :=
  plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite)

Graph representative for the constructed final relation.

noncomputable def constructedFinalTopology
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node) :
    Graph node :=
  graphOfRelation (constructedFinalRelation policy context rawRewrite)

The constructed final topology denotes the relation-level planner output.

theorem denote_constructedFinalTopology
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node) :
    denote (constructedFinalTopology policy context rawRewrite) =
      constructedFinalRelation policy context rawRewrite := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite node⊢ denote (constructedFinalTopology policy context rawRewrite) = constructedFinalRelation policy context rawRewrite
  unfold constructedFinalTopology constructedFinalRelationnode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite node⊢ denote (graphOfRelation (plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite))) =
  plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite)
  exact
    denote_graphOfRelation
      (plannedFinalRelation_edgeEndpointsInVertices
        context.topology
        (runtimePlannerRewrite policy rawRewrite))All goals completed! 🐙

Planned delta obtained by the runtime-shaped construction equations.

noncomputable def constructedPlannedRewriteDelta
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node)
    (insertedDepth : Nat) :
    PlannedRewriteDelta node :=
  let rewrite := runtimePlannerRewrite policy rawRewrite
  let finalRelation := constructedFinalRelation policy context rawRewrite
  let oldRelation := denote context.topology
  let newNodes := relationAddedNodes oldRelation finalRelation
  let addedEdges := relationAddedEdges oldRelation finalRelation
  { topology := constructedFinalTopology policy context rawRewrite
    definitions := plannedFinalDefinitions context rewrite
    newNodes := newNodes
    removedNodes := relationRemovedNodes oldRelation finalRelation
    addedEdges := addedEdges
    entryNodes := rewrite.spec.entryNodes
    exitNodes := rewrite.spec.exitNodes
    anchorNode := rawRewrite.anchor
    anchorDisposition := rewrite.anchorDisposition
    cost :=
      { addedNodes := newNodes.card
        addedEdges := addedEdges.card
        addedDepth :=
          match rewrite.anchorDisposition with
          | RewriteAnchorDisposition.removed => insertedDepth - 1
          | RewriteAnchorDisposition.retained => insertedDepth
        frontierDelta := rewrite.spec.entryNodes.card - 1
        rewriteOps := 1 } }

Constructed planned deltas preserve the Wire registry boundary from explicit admission of their relation-diff vertices and edges.

theorem constructedPlannedRewriteDelta_preserves_registryBoundary
    {executor config contract authority : Type}
    [DecidableEq contract]
    [DecidableEq (StagedExecutorNode executor config authority)]
    (registry : ExecutorRegistry executor config contract authority)
    {policy :
      RuntimeNamespacePolicy (StagedExecutorNode executor config authority)}
    {context :
      PlanningContext (StagedExecutorNode executor config authority)}
    {rawRewrite :
      GraphRewrite (StagedExecutorNode executor config authority)}
    {insertedDepth : Nat}
    (hBoundary : registryBoundary registry context.topology)
    (hDelta :
      RegistryBoundaryDeltaAdmitted
        registry
        (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)) :
    registryBoundary
      registry
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology := byexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ registryBoundary registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  refine
    registryBoundary_preserved_of_delta_admitted
      registry
      ?_
      hBoundary
      hDeltaexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ TopologyDiffMatches context (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
  refine
    { newNodes_eq := ?_
      removedNodes_eq := ?_
      addedEdges_eq := ?_ }refine_1executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes =
  relationAddedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)refine_2executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).removedNodes =
  relationRemovedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)refine_3executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges =
  relationAddedEdges (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)
  ·refine_1executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes =
  relationAddedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
      [ constructedPlannedRewriteDelta
      , constructedFinalRelation
      , denote_constructedFinalTopology
      ]All goals completed! 🐙
  ·refine_2executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).removedNodes =
  relationRemovedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
      [ constructedPlannedRewriteDelta
      , constructedFinalRelation
      , denote_constructedFinalTopology
      ]All goals completed! 🐙
  ·refine_3executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges =
  relationAddedEdges (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
      [ constructedPlannedRewriteDelta
      , constructedFinalRelation
      , denote_constructedFinalTopology
      ]All goals completed! 🐙

Constructed planned deltas provide the contractPreserved witness needed when the contract predicate is exactly registryBoundary registry.

theorem constructedPlannedRewriteDelta_registryBoundaryContractPreserved
    {executor config contract authority : Type}
    [DecidableEq contract]
    [DecidableEq (StagedExecutorNode executor config authority)]
    (registry : ExecutorRegistry executor config contract authority)
    {policy :
      RuntimeNamespacePolicy (StagedExecutorNode executor config authority)}
    {context :
      PlanningContext (StagedExecutorNode executor config authority)}
    {rawRewrite :
      GraphRewrite (StagedExecutorNode executor config authority)}
    {insertedDepth : Nat}
    (hDelta :
      RegistryBoundaryDeltaAdmitted
        registry
        (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)) :
    ∀ g,
      denote g = denote context.topology →
        registryBoundary registry g →
          registryBoundary
            registry
            (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology := byexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)⊢ ∀ (g : Graph (StagedExecutorNode executor config authority)),
  denote g = denote context.topology →
    registryBoundary registry g →
      registryBoundary registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  intro g hGraphEqexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)g:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topology⊢ registryBoundary registry g →
  registryBoundary registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology hBoundaryexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)g:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topologyhBoundary:registryBoundary registry g⊢ registryBoundary registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  have hContextBoundary : registryBoundary registry context.topology :=
    registryBoundary_of_graphEq hGraphEq hBoundaryexecutor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)rawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕhDelta:RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)g:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topologyhBoundary:registryBoundary registry ghContextBoundary:registryBoundary registry context.topology⊢ registryBoundary registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  exact
    constructedPlannedRewriteDelta_preserves_registryBoundary
      registry
      hContextBoundary
      hDeltaAll goals completed! 🐙

The constructed delta records anchor identity and derives anchor membership facts.

theorem constructedPlannedRewriteDelta_anchorMatches
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    (hDiscipline :
      NamespaceDiscipline
        policy.localAllowed
        (policy.namespaceNode rawRewrite.anchor)
        context
        rawRewrite.spec)
    (hAnchorInTopology : rawRewrite.anchor ∈ (denote context.topology).vertices)
    (hSourceAcyclic : Acyclic context.topology)
    (hRawSubgraphValid : rawRewrite.spec.Valid) :
    RuntimeAnchorMatches
      policy
      rawRewrite
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.Valid⊢ RuntimeAnchorMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
  have hAnchorNoSelfLoop :
      (rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges :=
    anchor_noSelfLoop_of_acyclic hSourceAcyclicnode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges⊢ RuntimeAnchorMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
  have hNamespacedValid : (runtimePlannerRewrite policy rawRewrite).spec.Valid := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.Valid⊢ RuntimeAnchorMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
    simp only [runtimePlannerRewrite, namespaceGraphRewrite_spec]node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges⊢ (namespaceSubgraphSpec (policy.namespaceNode rawRewrite.anchor) rawRewrite.spec).Valid
    exact
      namespaceSubgraphSpec_preserves_valid
        (policy.namespaceNode_injective rawRewrite.anchor)
        hRawSubgraphValidAll goals completed! 🐙
  have hFresh :
      ∀ mappedNode,
        mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices →
          mappedNode ∉ (denote context.topology).vertices := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.Valid⊢ RuntimeAnchorMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
    rw [runtimePlannerRewrite, namespaceGraphRewrite_spec]node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.Valid⊢ ∀
  mappedNode ∈
    (denote (namespaceSubgraphSpec (policy.namespaceNode rawRewrite.anchor) rawRewrite.spec).topology).vertices,
  mappedNode ∉ (denote context.topology).vertices
    exact namespaceSubgraphSpec_fresh_against_context hDisciplineAll goals completed! 🐙
  refine
    { anchorNode_eq := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).vertices⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorNode = rawRewrite.anchor
        simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
      anchorDisposition_eq := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).vertices⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition =
  (runtimePlannerRewrite policy rawRewrite).anchorDisposition
        simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
      removed_absent := ?_
      retained_present := ?_ }
  ·refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).vertices⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition =
    RewriteAnchorDisposition.removed →
  (runtimePlannerRewrite policy rawRewrite).anchor ∉
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology).vertices intro hRemovedrefine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition =
  RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∉
  (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology).vertices
    simp only [constructedPlannedRewriteDelta] at hRemoved ⊢refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy rawRewrite).anchorDisposition = RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∉
  (denote (constructedFinalTopology policy context rawRewrite)).vertices
    rw [denote_constructedFinalTopology]refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy rawRewrite).anchorDisposition = RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∉ (constructedFinalRelation policy context rawRewrite).vertices
    cases rawRewrite with
    | expandNode anchor mode spec =>refine_1.expandNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodemode:ExpansionModespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode (GraphRewrite.expandNode anchor mode spec).anchor) context
  (GraphRewrite.expandNode anchor mode spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor mode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor mode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor mode spec).anchor, (GraphRewrite.expandNode anchor mode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).anchorDisposition =
  RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).anchor ∉
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor mode spec)).vertices
        cases mode with
        | replaceNode =>refine_1.expandNode.replaceNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed
  (policy.namespaceNode (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) context
  (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote
        (runtimePlannerRewrite policy
              (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).anchorDisposition =
  RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).anchor ∉
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
            exact
              anchor_not_mem_plannedFinalRelation_replace
                hAnchorInTopology
                hAnchorNoSelfLoop
                hFresh
                hNamespacedValid.entryNodesInside
                hNamespacedValid.exitNodesInsideAll goals completed! 🐙
        | retainNodeAsEnvelope =>refine_1.expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed
  (policy.namespaceNode (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) context
  (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote
        (runtimePlannerRewrite policy
              (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).anchorDisposition =
  RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).anchor ∉
  (constructedFinalRelation policy context
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
            cases hRemovedAll goals completed! 🐙
    | appendAfter anchor spec =>refine_1.appendAfternode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode (GraphRewrite.appendAfter anchor spec).anchor) context
  (GraphRewrite.appendAfter anchor spec).spechAnchorInTopology:(GraphRewrite.appendAfter anchor spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.appendAfter anchor spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.appendAfter anchor spec).anchor, (GraphRewrite.appendAfter anchor spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRemoved:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).anchorDisposition =
  RewriteAnchorDisposition.removed⊢ (runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).anchor ∉
  (constructedFinalRelation policy context (GraphRewrite.appendAfter anchor spec)).vertices
        cases hRemovedAll goals completed! 🐙
  ·refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).vertices⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition =
    RewriteAnchorDisposition.retained →
  (runtimePlannerRewrite policy rawRewrite).anchor ∈
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology).vertices intro hRetainedrefine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition =
  RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∈
  (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology).vertices
    simp only [constructedPlannedRewriteDelta] at hRetained ⊢refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy rawRewrite).anchorDisposition = RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∈
  (denote (constructedFinalTopology policy context rawRewrite)).vertices
    rw [denote_constructedFinalTopology]refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spechAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshSourceAcyclic:Acyclic context.topologyhRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy rawRewrite).anchorDisposition = RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy rawRewrite).anchor ∈ (constructedFinalRelation policy context rawRewrite).vertices
    cases rawRewrite with
    | expandNode anchor mode spec =>refine_2.expandNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodemode:ExpansionModespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode (GraphRewrite.expandNode anchor mode spec).anchor) context
  (GraphRewrite.expandNode anchor mode spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor mode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor mode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor mode spec).anchor, (GraphRewrite.expandNode anchor mode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).anchorDisposition =
  RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).anchor ∈
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor mode spec)).vertices
        cases mode with
        | replaceNode =>refine_2.expandNode.replaceNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed
  (policy.namespaceNode (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) context
  (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote
        (runtimePlannerRewrite policy
              (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).anchorDisposition =
  RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).anchor ∈
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
            cases hRetainedAll goals completed! 🐙
        | retainNodeAsEnvelope =>refine_2.expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed
  (policy.namespaceNode (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) context
  (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spechAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.ValidhFresh:∀
  mappedNode ∈
    (denote
        (runtimePlannerRewrite policy
              (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).anchorDisposition =
  RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).anchor ∈
  (constructedFinalRelation policy context
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
            exact anchor_mem_plannedFinalRelation_retain hAnchorInTopologyAll goals completed! 🐙
    | appendAfter anchor spec =>refine_2.appendAfternode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSourceAcyclic:Acyclic context.topologyanchor:nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline policy.localAllowed (policy.namespaceNode (GraphRewrite.appendAfter anchor spec).anchor) context
  (GraphRewrite.appendAfter anchor spec).spechAnchorInTopology:(GraphRewrite.appendAfter anchor spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.appendAfter anchor spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.appendAfter anchor spec).anchor, (GraphRewrite.appendAfter anchor spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.ValidhFresh:∀ mappedNode ∈ (denote (runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.topology).vertices,
  mappedNode ∉ (denote context.topology).verticeshRetained:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).anchorDisposition =
  RewriteAnchorDisposition.retained⊢ (runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).anchor ∈
  (constructedFinalRelation policy context (GraphRewrite.appendAfter anchor spec)).vertices
        exact anchor_mem_plannedFinalRelation_append hAnchorInTopologyAll goals completed! 🐙

SourcePlanningContextValid is the invariant carried by materialized planner inputs.

structure SourcePlanningContextValid (context : PlanningContext node) : Prop where

The current materialized topology is already a DAG.

sourceAcyclic : Acyclic context.topology

Current stage definitions exactly cover the materialized topology.

definitionsCover : DefinitionCoverage context.topology context.definitions

Source context validity turns anchor membership into anchor-definition membership.

theorem SourcePlanningContextValid.anchorHasDefinition
    {context : PlanningContext node}
    {anchor : node}
    (hSource : SourcePlanningContextValid context)
    (hAnchorInTopology : anchor ∈ (denote context.topology).vertices) :
    anchor ∈ context.definitions := bynode:Typeinst✝:DecidableEq nodecontext:PlanningContext nodeanchor:nodehSource:SourcePlanningContextValid contexthAnchorInTopology:anchor ∈ (denote context.topology).vertices⊢ anchor ∈ context.definitions
  rw [hSource.definitionsCover]node:Typeinst✝:DecidableEq nodecontext:PlanningContext nodeanchor:nodehSource:SourcePlanningContextValid contexthAnchorInTopology:anchor ∈ (denote context.topology).vertices⊢ anchor ∈ (denote context.topology).vertices
  exact hAnchorInTopologyAll goals completed! 🐙

Concrete construction derives final definition coverage from source and subgraph coverage.

theorem constructedPlannedRewriteDelta_finalDefinitionsCover
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    (hSource : SourcePlanningContextValid context)
    (hAnchorInTopology : rawRewrite.anchor ∈ (denote context.topology).vertices)
    (hRawSubgraphValid : rawRewrite.spec.Valid) :
    DefinitionCoverage
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
  have hAnchorNoSelfLoop :
      (rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges :=
    anchor_noSelfLoop_of_acyclic hSource.sourceAcyclicnode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
  have hNamespacedValid : (runtimePlannerRewrite policy rawRewrite).spec.Valid := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
    simp only [runtimePlannerRewrite, namespaceGraphRewrite_spec]node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edges⊢ (namespaceSubgraphSpec (policy.namespaceNode rawRewrite.anchor) rawRewrite.spec).Valid
    exact
      namespaceSubgraphSpec_preserves_valid
        (policy.namespaceNode_injective rawRewrite.anchor)
        hRawSubgraphValidAll goals completed! 🐙
  unfold DefinitionCoveragenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.Valid⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions =
  (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology).vertices
  simp only [constructedPlannedRewriteDelta]node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.Valid⊢ plannedFinalDefinitions context (runtimePlannerRewrite policy rawRewrite) =
  (denote (constructedFinalTopology policy context rawRewrite)).vertices
  rw [denote_constructedFinalTopology]node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.ValidhAnchorNoSelfLoop:(rawRewrite.anchor, rawRewrite.anchor) ∉ (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy rawRewrite).spec.Valid⊢ plannedFinalDefinitions context (runtimePlannerRewrite policy rawRewrite) =
  (constructedFinalRelation policy context rawRewrite).vertices
  cases rawRewrite with
  | expandNode anchor mode spec =>expandNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodemode:ExpansionModespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.expandNode anchor mode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor mode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor mode spec).anchor, (GraphRewrite.expandNode anchor mode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)).spec.Valid⊢ plannedFinalDefinitions context (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor mode spec)) =
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor mode spec)).vertices
      cases mode with
      | replaceNode =>expandNode.replaceNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.Valid⊢ plannedFinalDefinitions context
    (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)) =
  (constructedFinalRelation policy context (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).vertices
          have hNamespacedDefinitions :
              DefinitionCoverage
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.definitionsCoverAll goals completed! 🐙
          have hNamespacedEntries :
              NodesInside
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.entryNodesInsideAll goals completed! 🐙
          have hNamespacedExits :
              NodesInside
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.exitNodesInsideAll goals completed! 🐙
          have hNoSelfLoop :
              (anchor, anchor) ∉ (denote context.topology).edges := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [GraphRewrite.anchor] using hAnchorNoSelfLoopAll goals completed! 🐙
          simp only
            [ constructedFinalRelation
            , runtimePlannerRewrite
            , namespaceGraphRewrite
            , GraphRewrite.anchor
            , GraphRewrite.spec
            , GraphRewrite.anchorDisposition
            , plannedFinalDefinitions
            ]expandNode.replaceNodenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.replaceNode spec)).spec.ValidhNamespacedDefinitions:DefinitionCoverage (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitionshNamespacedEntries:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhNamespacedExits:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhNoSelfLoop:(anchor, anchor) ∉ (denote context.topology).edges⊢ context.definitions.erase anchor ∪ (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions =
  (plannedFinalRelation context.topology
      (GraphRewrite.expandNode anchor ExpansionMode.replaceNode
        (namespaceSubgraphSpec (policy.namespaceNode anchor) spec))).vertices
          rw
            [ plannedFinalRelation_vertices_replace
                hNoSelfLoop
                hNamespacedEntries
                hNamespacedExits
            , hSource.definitionsCover
            , hNamespacedDefinitions
            ]All goals completed! 🐙
      | retainNodeAsEnvelope =>expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.Valid⊢ plannedFinalDefinitions context
    (runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)) =
  (constructedFinalRelation policy context
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).vertices
          have hNamespacedDefinitions :
              DefinitionCoverage
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.definitionsCoverAll goals completed! 🐙
          have hNamespacedEntries :
              NodesInside
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.entryNodesInsideAll goals completed! 🐙
          have hNamespacedExits :
              NodesInside
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
                (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
              hNamespacedValid.exitNodesInsideAll goals completed! 🐙
          have hAnchorIn :
              anchor ∈ (denote context.topology).vertices := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
            simpa only [GraphRewrite.anchor] using hAnchorInTopologyAll goals completed! 🐙
          simp only
            [ constructedFinalRelation
            , runtimePlannerRewrite
            , namespaceGraphRewrite
            , GraphRewrite.anchor
            , GraphRewrite.spec
            , GraphRewrite.anchorDisposition
            , plannedFinalDefinitions
            ]expandNode.retainNodeAsEnvelopenode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor,
    (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope spec)).spec.ValidhNamespacedDefinitions:DefinitionCoverage (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitionshNamespacedEntries:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhNamespacedExits:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhAnchorIn:anchor ∈ (denote context.topology).vertices⊢ context.definitions ∪ (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions =
  (plannedFinalRelation context.topology
      (GraphRewrite.expandNode anchor ExpansionMode.retainNodeAsEnvelope
        (namespaceSubgraphSpec (policy.namespaceNode anchor) spec))).vertices
          rw
            [ plannedFinalRelation_vertices_retain
                hAnchorIn
                hNamespacedEntries
                hNamespacedExits
            , hSource.definitionsCover
            , hNamespacedDefinitions
            ]All goals completed! 🐙
  | appendAfter anchor spec =>appendAfternode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.appendAfter anchor spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.appendAfter anchor spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.appendAfter anchor spec).anchor, (GraphRewrite.appendAfter anchor spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.Valid⊢ plannedFinalDefinitions context (runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)) =
  (constructedFinalRelation policy context (GraphRewrite.appendAfter anchor spec)).vertices
      have hNamespacedDefinitions :
          DefinitionCoverage
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
        simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
          hNamespacedValid.definitionsCoverAll goals completed! 🐙
      have hNamespacedEntries :
          NodesInside
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
        simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
          hNamespacedValid.entryNodesInsideAll goals completed! 🐙
      have hNamespacedExits :
          NodesInside
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
            (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
        simpa only [runtimePlannerRewrite, namespaceGraphRewrite, GraphRewrite.spec] using
          hNamespacedValid.exitNodesInsideAll goals completed! 🐙
      have hAnchorIn :
          anchor ∈ (denote context.topology).vertices := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contexthAnchorInTopology:rawRewrite.anchor ∈ (denote context.topology).verticeshRawSubgraphValid:rawRewrite.spec.Valid⊢ DefinitionCoverage (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions
        simpa only [GraphRewrite.anchor] using hAnchorInTopologyAll goals completed! 🐙
      simp only
        [ constructedFinalRelation
        , runtimePlannerRewrite
        , namespaceGraphRewrite
        , GraphRewrite.anchor
        , GraphRewrite.spec
        , GraphRewrite.anchorDisposition
        , plannedFinalDefinitions
        ]appendAfternode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext nodeinsertedDepth:ℕhSource:SourcePlanningContextValid contextanchor:nodespec:SubgraphSpec nodehAnchorInTopology:(GraphRewrite.appendAfter anchor spec).anchor ∈ (denote context.topology).verticeshRawSubgraphValid:(GraphRewrite.appendAfter anchor spec).spec.ValidhAnchorNoSelfLoop:((GraphRewrite.appendAfter anchor spec).anchor, (GraphRewrite.appendAfter anchor spec).anchor) ∉
  (denote context.topology).edgeshNamespacedValid:(runtimePlannerRewrite policy (GraphRewrite.appendAfter anchor spec)).spec.ValidhNamespacedDefinitions:DefinitionCoverage (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topology
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitionshNamespacedEntries:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).entryNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhNamespacedExits:NodesInside (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).exitNodes
  (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).topologyhAnchorIn:anchor ∈ (denote context.topology).vertices⊢ context.definitions ∪ (namespaceSubgraphSpec (policy.namespaceNode anchor) spec).definitions =
  (plannedFinalRelation context.topology
      (GraphRewrite.appendAfter anchor (namespaceSubgraphSpec (policy.namespaceNode anchor) spec))).vertices
      rw
        [ plannedFinalRelation_vertices_append
            hAnchorIn
            hNamespacedEntries
            hNamespacedExits
        , hSource.definitionsCover
        , hNamespacedDefinitions
        ]All goals completed! 🐙

Runtime validation inputs not computed by the pure construction equations.

structure RuntimeConstructionValidation
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node)
    (insertedDepth : Nat) :
    Prop where

The runtime namespace validator accepted local syntax and freshness.

  namespaceDiscipline :
    NamespaceDiscipline
      policy.localAllowed
      (policy.namespaceNode rawRewrite.anchor)
      context
      rawRewrite.spec

The raw anchor exists in the current topology.

anchorInTopology : rawRewrite.anchor ∈ (denote context.topology).vertices

The raw anchor has a current definition.

anchorHasDefinition : rawRewrite.anchor ∈ context.definitions

The current topology is already a DAG before planning starts.

sourceAcyclic : Acyclic context.topology

The raw inserted subgraph passed runtime subgraph validation.

rawSubgraphValid : rawRewrite.spec.Valid

Runtime longest-path computation agrees with the proof-side inserted-depth witness.

  insertedDepthMatches :
    LongestInsertedPathNodeCount
      (runtimePlannerRewrite policy rawRewrite).spec
      insertedDepth

The final definition domain exactly covers final topology vertices.

  finalDefinitionsCover :
    DefinitionCoverage
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions

The runtime validated the final topology as acyclic.

  finalAcyclic :
    Acyclic (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology

Runtime-shaped inputs from which construction validation is derived.

The remaining explicit fields correspond to executable checks: namespace validation, source anchor membership, raw subgraph validation, longest-path cost computation, and final DAG validation. Source definition coverage derives anchor definition membership and final definition coverage.

structure RuntimeConstructionInputs
    (policy : RuntimeNamespacePolicy node)
    (context : PlanningContext node)
    (rawRewrite : GraphRewrite node)
    (insertedDepth : Nat) :
    Prop where

The current materialized topology and definition domain are valid.

sourceValid : SourcePlanningContextValid context

The runtime namespace validator accepted local syntax and freshness.

  namespaceDiscipline :
    NamespaceDiscipline
      policy.localAllowed
      (policy.namespaceNode rawRewrite.anchor)
      context
      rawRewrite.spec

The raw anchor exists in the current topology.

anchorInTopology : rawRewrite.anchor ∈ (denote context.topology).vertices

The raw inserted subgraph passed runtime subgraph validation.

rawSubgraphValid : rawRewrite.spec.Valid

Runtime longest-path computation agrees with the proof-side inserted-depth witness.

  insertedDepthMatches :
    LongestInsertedPathNodeCount
      (runtimePlannerRewrite policy rawRewrite).spec
      insertedDepth

The runtime validated the final topology as acyclic.

  finalAcyclic :
    Acyclic (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology

Runtime-shaped inputs derive the older construction-validation bundle.

theorem RuntimeConstructionInputs.toValidation
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    (hInputs : RuntimeConstructionInputs policy context rawRewrite insertedDepth) :
    RuntimeConstructionValidation policy context rawRewrite insertedDepth :=
  { namespaceDiscipline := hInputs.namespaceDiscipline
    anchorInTopology := hInputs.anchorInTopology
    anchorHasDefinition :=
      hInputs.sourceValid.anchorHasDefinition hInputs.anchorInTopology
    sourceAcyclic := hInputs.sourceValid.sourceAcyclic
    rawSubgraphValid := hInputs.rawSubgraphValid
    insertedDepthMatches := hInputs.insertedDepthMatches
    finalDefinitionsCover :=
      constructedPlannedRewriteDelta_finalDefinitionsCover
        hInputs.sourceValid
        hInputs.anchorInTopology
        hInputs.rawSubgraphValid
    finalAcyclic := hInputs.finalAcyclic }

Runtime-shaped inputs carry the source-valid invariant to the next planner context.

theorem RuntimeConstructionInputs.toNextSourceValid
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    (hInputs : RuntimeConstructionInputs policy context rawRewrite insertedDepth) :
    SourcePlanningContextValid
      { topology :=
          (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology
        definitions :=
          (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions } :=
  { sourceAcyclic := hInputs.finalAcyclic
    definitionsCover :=
      constructedPlannedRewriteDelta_finalDefinitionsCover
        (insertedDepth := insertedDepth)
        hInputs.sourceValid
        hInputs.anchorInTopology
        hInputs.rawSubgraphValid }

The concrete construction equations establish RuntimePlannerConstruction.

theorem constructedPlannedRewriteDelta_runtimePlannerConstruction
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    (hValidation :
      RuntimeConstructionValidation policy context rawRewrite insertedDepth) :
    RuntimePlannerConstruction
      policy
      context
      rawRewrite
      (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) := bynode:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ RuntimePlannerConstruction policy context rawRewrite
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
  refine
    { namespaceDiscipline := hValidation.namespaceDiscipline
      anchorInTopology := hValidation.anchorInTopology
      anchorHasDefinition := hValidation.anchorHasDefinition
      rawSubgraphValid := hValidation.rawSubgraphValid
      anchorMatches :=
        constructedPlannedRewriteDelta_anchorMatches
          hValidation.namespaceDiscipline
          hValidation.anchorInTopology
          hValidation.sourceAcyclic
          hValidation.rawSubgraphValid
      deltaMatches := ?_
      costMatches := ?_
      finalDefinitionsCover := hValidation.finalDefinitionsCover
      finalAcyclic := hValidation.finalAcyclic }refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ RuntimeDeltaMatches policy context rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ RuntimeCostMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
  ·refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ RuntimeDeltaMatches policy context rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) refine
      { topology_eq := ?_
        entryNodes_eq := ?_
        exitNodes_eq := ?_
        newNodes_eq := ?_
        removedNodes_eq := ?_
        addedEdges_eq := ?_
        definitions_eq := ?_ }refine_1.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology =
  plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite)refine_1.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes =
  (runtimePlannerRewrite policy rawRewrite).spec.entryNodesrefine_1.refine_3node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).exitNodes =
  (runtimePlannerRewrite policy rawRewrite).spec.exitNodesrefine_1.refine_4node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes =
  relationAddedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)refine_1.refine_5node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).removedNodes =
  relationRemovedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)refine_1.refine_6node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges =
  relationAddedEdges (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology)refine_1.refine_7node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions =
  plannedFinalDefinitions context (runtimePlannerRewrite policy rawRewrite)
    ·refine_1.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology =
  plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite) exact denote_constructedFinalTopology policy context rawRewriteAll goals completed! 🐙
    ·refine_1.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes =
  (runtimePlannerRewrite policy rawRewrite).spec.entryNodes simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
    ·refine_1.refine_3node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).exitNodes =
  (runtimePlannerRewrite policy rawRewrite).spec.exitNodes simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
    ·refine_1.refine_4node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes =
  relationAddedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
        [ constructedPlannedRewriteDelta
        , constructedFinalRelation
        , denote_constructedFinalTopology
        ]All goals completed! 🐙
    ·refine_1.refine_5node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).removedNodes =
  relationRemovedNodes (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
        [ constructedPlannedRewriteDelta
        , constructedFinalRelation
        , denote_constructedFinalTopology
        ]All goals completed! 🐙
    ·refine_1.refine_6node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges =
  relationAddedEdges (denote context.topology)
    (denote (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topology) simp only
        [ constructedPlannedRewriteDelta
        , constructedFinalRelation
        , denote_constructedFinalTopology
        ]All goals completed! 🐙
    ·refine_1.refine_7node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).definitions =
  plannedFinalDefinitions context (runtimePlannerRewrite policy rawRewrite) simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
  ·refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ RuntimeCostMatches policy rawRewrite (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) refine
      { addedNodes_eq := ?_
        addedEdges_eq := ?_
        addedDepth_eq := ?_
        entryNodes_runtimeList := ?_
        rewriteOps_eq := ?_ }refine_2.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedNodes =
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes.cardrefine_2.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedEdges =
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges.cardrefine_2.refine_3node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ ∃ insertedDepth_1,
  LongestInsertedPathNodeCount (runtimePlannerRewrite policy rawRewrite).spec insertedDepth_1 ∧
    (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedDepth =
      match (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition with
      | RewriteAnchorDisposition.removed => insertedDepth_1 - 1
      | RewriteAnchorDisposition.retained => insertedDepth_1refine_2.refine_4node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ ∃ entryList,
  RuntimeNodeListMatches entryList (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes ∧
    (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta = entryList.length - 1refine_2.refine_5node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.rewriteOps = 1
    ·refine_2.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedNodes =
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).newNodes.card simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
    ·refine_2.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedEdges =
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).addedEdges.card simp only [constructedPlannedRewriteDelta]All goals completed! 🐙
    ·refine_2.refine_3node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ ∃ insertedDepth_1,
  LongestInsertedPathNodeCount (runtimePlannerRewrite policy rawRewrite).spec insertedDepth_1 ∧
    (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedDepth =
      match (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition with
      | RewriteAnchorDisposition.removed => insertedDepth_1 - 1
      | RewriteAnchorDisposition.retained => insertedDepth_1 refine ⟨insertedDepth, hValidation.insertedDepthMatches, ?_⟩refine_2.refine_3node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.addedDepth =
  match (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).anchorDisposition with
  | RewriteAnchorDisposition.removed => insertedDepth - 1
  | RewriteAnchorDisposition.retained => insertedDepth
      rflAll goals completed! 🐙
    ·refine_2.refine_4node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ ∃ entryList,
  RuntimeNodeListMatches entryList (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes ∧
    (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta = entryList.length - 1 let entryNodes :=
        (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodesrefine_2.refine_4node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes⊢ ∃ entryList,
  RuntimeNodeListMatches entryList (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes ∧
    (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta = entryList.length - 1
      refine ⟨entryNodes.toList, ?_, ?_⟩refine_2.refine_4.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes⊢ RuntimeNodeListMatches entryNodes.toList
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodesrefine_2.refine_4.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta =
  entryNodes.toList.length - 1
      ·refine_2.refine_4.refine_1node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes⊢ RuntimeNodeListMatches entryNodes.toList
  (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes exact
          ⟨ Finset.nodup_toList _
          , Finset.toList_toFinset _
          ⟩All goals completed! 🐙
      ·refine_2.refine_4.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodes⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta =
  entryNodes.toList.length - 1 have hEntryCard :
            entryNodes.card = entryNodes.toList.length :=
          RuntimeNodeListMatches.card_eq_length
            ⟨Finset.nodup_toList _, Finset.toList_toFinset _⟩refine_2.refine_4.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodeshEntryCard:entryNodes.card = entryNodes.toList.length⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.frontierDelta =
  entryNodes.toList.length - 1
        change entryNodes.card - 1 = entryNodes.toList.length - 1refine_2.refine_4.refine_2node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepthentryNodes:Finset node := (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).entryNodeshEntryCard:entryNodes.card = entryNodes.toList.length⊢ entryNodes.card - 1 = entryNodes.toList.length - 1
        rw [hEntryCard]All goals completed! 🐙
    ·refine_2.refine_5node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodeinsertedDepth:ℕhValidation:RuntimeConstructionValidation policy context rawRewrite insertedDepth⊢ (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).cost.rewriteOps = 1 simp only [constructedPlannedRewriteDelta]All goals completed! 🐙

Concrete construction plus budget admission gives an abstract admissible rewrite.

theorem constructedPlannedRewriteDelta_admissible
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    {budget remaining : RewriteBudget}
    {contractOk : Graph node → Prop}
    (hValidation :
      RuntimeConstructionValidation policy context rawRewrite insertedDepth)
    (hAdmitted :
      AdmittedRewriteDelta
        budget
        (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
        remaining)
    (hContracts :
      ∀ g,
        denote g = denote context.topology →
          contractOk g →
            contractOk
              (constructedPlannedRewriteDelta
                policy
                context
                rawRewrite
                insertedDepth).topology) :
    admissible
      ((constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).toRewrite
        context.topology
        (plannedRewriteSafety_of_checks
          (runtimePlannerConstruction_planGraphRewriteChecks
            (constructedPlannedRewriteDelta_runtimePlannerConstruction hValidation))
          hContracts))
      context.topology
      budget :=
  runtimePlannerConstruction_admissible
    (constructedPlannedRewriteDelta_runtimePlannerConstruction hValidation)
    hAdmitted
    hContracts

Runtime-shaped construction inputs plus budget admission give an admissible rewrite.

theorem constructedPlannedRewriteDelta_admissible_of_inputs
    {policy : RuntimeNamespacePolicy node}
    {context : PlanningContext node}
    {rawRewrite : GraphRewrite node}
    {insertedDepth : Nat}
    {budget remaining : RewriteBudget}
    {contractOk : Graph node → Prop}
    (hInputs :
      RuntimeConstructionInputs policy context rawRewrite insertedDepth)
    (hAdmitted :
      AdmittedRewriteDelta
        budget
        (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)
        remaining)
    (hContracts :
      ∀ g,
        denote g = denote context.topology →
          contractOk g →
            contractOk
              (constructedPlannedRewriteDelta
                policy
                context
                rawRewrite
                insertedDepth).topology) :
    admissible
      ((constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).toRewrite
        context.topology
        (plannedRewriteSafety_of_checks
          (runtimePlannerConstruction_planGraphRewriteChecks
            (constructedPlannedRewriteDelta_runtimePlannerConstruction
              hInputs.toValidation))
          hContracts))
      context.topology
      budget :=
  constructedPlannedRewriteDelta_admissible
    hInputs.toValidation
    hAdmitted
    hContracts

end ConstructedDeltaend Cortex.Wire