Algo.graph.Generated definitions

import Definitions.Def_Algo2LeanLib_Modules

set_option autoImplicit true
set_option backward.isDefEq.respectTransparency false
set_option backward.defeqAttrib.useBackward true


-- Generated by Algo2Lean 0.1.4 https://github.com/lunjiah/algo2lean

namespace Algo.«graph»

open _root_.Algo2LeanGenerated

-- Independently compiled module; imported algorithms keep their own transitions.
namespace Algo2LeanGenerated

abbrev Ref_Edge := ObjectRef
abbrev Ref_Graph := ObjectRef

-- Shallow class membership; fields and referenced objects are observed separately.
def is_Edge (h : Heap) (ref : Ref_Edge) : Prop :=
  ref < h.nextObject ∧ h.objectClass ref = some "graph.Edge"
instance (h : Heap) (ref : Ref_Edge) : Decidable (is_Edge h ref) :=
  inferInstanceAs (Decidable (ref < h.nextObject ∧ h.objectClass ref = some "graph.Edge"))

def field_Edge_target (h : Heap) (ref : Ref_Edge) : Option Int :=
  if is_Edge h ref then (h.readField ref "target").bind ObjectValue.asInt else none
def set_Edge_target (h : Heap) (ref : Ref_Edge) (value : Int) : Heap :=
  h.writeField ref "target" (ObjectValue.intValue value)
@[simp] theorem field_Edge_target_set (h : Heap) (ref : Ref_Edge) (value : Int)
    (valid : is_Edge h ref) :
    field_Edge_target (set_Edge_target h ref value) ref = some value := by
  have valid' : is_Edge (set_Edge_target h ref value) ref := by
    simpa [set_Edge_target, is_Edge] using valid
  rw [field_Edge_target, if_pos valid']
  unfold set_Edge_target
  rw [Heap.readField_writeField_same h ref "target" _ "graph.Edge" valid.2]
  rfl

def field_Edge_weight (h : Heap) (ref : Ref_Edge) : Option Int :=
  if is_Edge h ref then (h.readField ref "weight").bind ObjectValue.asInt else none
def set_Edge_weight (h : Heap) (ref : Ref_Edge) (value : Int) : Heap :=
  h.writeField ref "weight" (ObjectValue.intValue value)
@[simp] theorem field_Edge_weight_set (h : Heap) (ref : Ref_Edge) (value : Int)
    (valid : is_Edge h ref) :
    field_Edge_weight (set_Edge_weight h ref value) ref = some value := by
  have valid' : is_Edge (set_Edge_weight h ref value) ref := by
    simpa [set_Edge_weight, is_Edge] using valid
  rw [field_Edge_weight, if_pos valid']
  unfold set_Edge_weight
  rw [Heap.readField_writeField_same h ref "weight" _ "graph.Edge" valid.2]
  rfl

def field_Edge_next (h : Heap) (ref : Ref_Edge) : Option (Option Ref_Edge) :=
  if is_Edge h ref then (h.readField ref "next").bind ObjectValue.asNullableObject else none
def set_Edge_next (h : Heap) (ref : Ref_Edge) (value : (Option Ref_Edge)) : Heap :=
  h.writeField ref "next" (match value with | some ref => ObjectValue.objectValue ref | none => ObjectValue.noneValue)
@[simp] theorem field_Edge_next_set (h : Heap) (ref : Ref_Edge) (value : (Option Ref_Edge))
    (valid : is_Edge h ref) :
    field_Edge_next (set_Edge_next h ref value) ref = some value := by
  have valid' : is_Edge (set_Edge_next h ref value) ref := by
    simpa [set_Edge_next, is_Edge] using valid
  rw [field_Edge_next, if_pos valid']
  unfold set_Edge_next
  rw [Heap.readField_writeField_same h ref "next" _ "graph.Edge" valid.2]
  cases value <;> rfl

/-- Build input data directly; this helper does not execute `__init__`. -/
def create_Edge (h : Heap) (value_target : Int) (value_weight : Int) (value_next : (Option Ref_Edge)) : Heap × Ref_Edge :=
  let ref := h.nextObject
  let h := h.allocateObject "graph.Edge"
  let h := set_Edge_target h ref value_target
  let h := set_Edge_weight h ref value_weight
  let h := set_Edge_next h ref value_next
  (h, ref)

-- Shallow class membership; fields and referenced objects are observed separately.
def is_Graph (h : Heap) (ref : Ref_Graph) : Prop :=
  ref < h.nextObject ∧ h.objectClass ref = some "graph.Graph"
instance (h : Heap) (ref : Ref_Graph) : Decidable (is_Graph h ref) :=
  inferInstanceAs (Decidable (ref < h.nextObject ∧ h.objectClass ref = some "graph.Graph"))

def field_Graph_size (h : Heap) (ref : Ref_Graph) : Option Int :=
  if is_Graph h ref then (h.readField ref "size").bind ObjectValue.asInt else none
def set_Graph_size (h : Heap) (ref : Ref_Graph) (value : Int) : Heap :=
  h.writeField ref "size" (ObjectValue.intValue value)
@[simp] theorem field_Graph_size_set (h : Heap) (ref : Ref_Graph) (value : Int)
    (valid : is_Graph h ref) :
    field_Graph_size (set_Graph_size h ref value) ref = some value := by
  have valid' : is_Graph (set_Graph_size h ref value) ref := by
    simpa [set_Graph_size, is_Graph] using valid
  rw [field_Graph_size, if_pos valid']
  unfold set_Graph_size
  rw [Heap.readField_writeField_same h ref "size" _ "graph.Graph" valid.2]
  rfl

def field_Graph_heads (h : Heap) (ref : Ref_Graph) : Option CollectionRef :=
  if is_Graph h ref then (h.readField ref "heads").bind ObjectValue.asCollection else none
def set_Graph_heads (h : Heap) (ref : Ref_Graph) (value : CollectionRef) : Heap :=
  h.writeField ref "heads" (ObjectValue.collectionValue value)
@[simp] theorem field_Graph_heads_set (h : Heap) (ref : Ref_Graph) (value : CollectionRef)
    (valid : is_Graph h ref) :
    field_Graph_heads (set_Graph_heads h ref value) ref = some value := by
  have valid' : is_Graph (set_Graph_heads h ref value) ref := by
    simpa [set_Graph_heads, is_Graph] using valid
  rw [field_Graph_heads, if_pos valid']
  unfold set_Graph_heads
  rw [Heap.readField_writeField_same h ref "heads" _ "graph.Graph" valid.2]
  rfl

/-- Build input data directly; this helper does not execute `__init__`. -/
def create_Graph (h : Heap) (value_size : Int) (value_heads : CollectionRef) : Heap × Ref_Graph :=
  let ref := h.nextObject
  let h := h.allocateObject "graph.Graph"
  let h := set_Graph_size h ref value_size
  let h := set_Graph_heads h ref value_heads
  (h, ref)

def seq_Edge_optional : SequenceType (Option Ref_Edge) where
  name := "graph.Edge?"
  encode := fun value => (match value with | some ref => ObjectValue.objectValue ref | none => ObjectValue.noneValue)
  decode := ObjectValue.asNullableObject
  decode_encode := by intro value; cases value <;> rfl

structure State_Edge___init__ where
  v0 : Ref_Edge := 0 -- self
  v1 : Int := 0 -- target
  v2 : Int := 0 -- weight
  v3 : (Option Ref_Edge) := none -- next
  t4 : Unit := () -- temporary

structure State_Graph___init__ where
  v0 : Ref_Graph := 0 -- self
  v1 : Int := 0 -- size
  t2 : Unit := () -- temporary
  t3 : CollectionRef := 0 -- temporary
  t4 : Ref_Graph := 0 -- temporary
  t5 : (Option Ref_Edge) := none -- temporary
  t6 : Bool := false -- temporary

structure State_Graph_add_edge where
  v0 : Ref_Graph := 0 -- self
  v1 : Int := 0 -- source
  v2 : Int := 0 -- target
  v3 : Int := 0 -- weight
  t4 : Bool := false -- temporary
  t5 : (Option Ref_Edge) := none -- temporary
  t6 : Int := 0 -- temporary
  t7 : CollectionRef := 0 -- temporary
  t8 : Int := 0 -- temporary
  t9 : Int := 0 -- temporary
  t10 : (Option Ref_Edge) := none -- temporary
  t11 : Bool := false -- temporary
  t12 : Bool := false -- temporary

structure State_Edge where
  v0 : Int := 0 -- target
  v1 : Int := 0 -- weight
  v2 : (Option Ref_Edge) := none -- next
  v3 : Ref_Edge := 0 -- _instance
  t4 : Ref_Edge := 0 -- temporary
  t5 : Unit := () -- temporary
  t6 : Ref_Edge := 0 -- temporary
  t7 : Int := 0 -- temporary
  t8 : Int := 0 -- temporary
  t9 : (Option Ref_Edge) := none -- temporary
  t10 : Ref_Edge := 0 -- temporary

structure State_Graph where
  v0 : Int := 0 -- size
  v1 : Ref_Graph := 0 -- _instance
  t2 : Ref_Graph := 0 -- temporary
  t3 : Unit := () -- temporary
  t4 : Ref_Graph := 0 -- temporary
  t5 : Int := 0 -- temporary
  t6 : Ref_Graph := 0 -- temporary

inductive Frame where
  | invalid
  | fn_Edge___init__ (pc : Nat) (state : State_Edge___init__)
  | fn_Graph___init__ (pc : Nat) (state : State_Graph___init__)
  | fn_Graph_add_edge (pc : Nat) (state : State_Graph_add_edge)
  | fn_Edge (pc : Nat) (state : State_Edge)
  | fn_Graph (pc : Nat) (state : State_Graph)

inductive Result where
  | fn_Edge___init__ (value : Unit)
  | fn_Graph___init__ (value : Unit)
  | fn_Graph_add_edge (value : Bool)
  | fn_Edge (value : Ref_Edge)
  | fn_Graph (value : Ref_Graph)

abbrev Configuration := Algo2LeanCore.Config Heap (Frame) Result
abbrev Stack := Algo2LeanCore.Stack (Frame) Result
abbrev Transcript := List (Configuration)

inductive Step : Configuration → Configuration → Prop where
  | Edge___init___pc1 (h : Heap) (s : State_Edge___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Edge___init__ 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Edge___init__ (s.t4)) stack)
  | Edge___init___pc2 (h : Heap) (s : State_Edge___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Edge___init__ 2 s) stack) (.active h (Frame.fn_Edge___init__ 1 { s with t4 := () }) stack)
  | Edge___init___pc3 (h : Heap) (s : State_Edge___init__) (stack : Stack) (defined : (is_Edge h (s.v0))) :
      Step (.active h (Frame.fn_Edge___init__ 3 s) stack) (.active (set_Edge_next h (s.v0) (s.v3)) (Frame.fn_Edge___init__ 2 s) stack)
  | Edge___init___pc4 (h : Heap) (s : State_Edge___init__) (stack : Stack) (defined : (is_Edge h (s.v0))) :
      Step (.active h (Frame.fn_Edge___init__ 4 s) stack) (.active (set_Edge_weight h (s.v0) (s.v2)) (Frame.fn_Edge___init__ 3 s) stack)
  | Edge___init___pc5 (h : Heap) (s : State_Edge___init__) (stack : Stack) (defined : (is_Edge h (s.v0))) :
      Step (.active h (Frame.fn_Edge___init__ 5 s) stack) (.active (set_Edge_target h (s.v0) (s.v1)) (Frame.fn_Edge___init__ 4 s) stack)
  | Graph___init___pc1 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Graph___init__ (s.t2)) stack)
  | Graph___init___pc2 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 2 s) stack) (.active h (Frame.fn_Graph___init__ 1 { s with t2 := () }) stack)
  | Graph___init___pc3 (h : Heap) (s : State_Graph___init__) (stack : Stack) (defined : (is_Graph h (s.t4))) :
      Step (.active h (Frame.fn_Graph___init__ 3 s) stack) (.active (set_Graph_heads h (s.t4) (s.t3)) (Frame.fn_Graph___init__ 2 s) stack)
  | Graph___init___pc4 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 4 s) stack) (.active h (Frame.fn_Graph___init__ 3 { s with t4 := s.v0 }) stack)
  | Graph___init___pc5 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 5 s) stack) (.active (seq_Edge_optional.const h s.t5).1 (Frame.fn_Graph___init__ 4 { s with t3 := h.nextCollection }) stack)
  | Graph___init___pc6 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 6 s) stack) (.active h (Frame.fn_Graph___init__ 5 { s with t5 := none }) stack)
  | Graph___init___pc7 (h : Heap) (s : State_Graph___init__) (stack : Stack) (defined : (is_Graph h (s.v0))) :
      Step (.active h (Frame.fn_Graph___init__ 7 s) stack) (.active (set_Graph_size h (s.v0) ((0 : Int))) (Frame.fn_Graph___init__ 6 s) stack)
  | Graph___init___pc8_true (h : Heap) (s : State_Graph___init__) (stack : Stack) (condition : s.t6 = true) :
      Step (.active h (Frame.fn_Graph___init__ 8 s) stack) (.active h (Frame.fn_Graph___init__ 7 s) stack)
  | Graph___init___pc8_false (h : Heap) (s : State_Graph___init__) (stack : Stack) (condition : s.t6 = false) :
      Step (.active h (Frame.fn_Graph___init__ 8 s) stack) (.active h (Frame.fn_Graph___init__ 6 s) stack)
  | Graph___init___pc9 (h : Heap) (s : State_Graph___init__) (stack : Stack) :
      Step (.active h (Frame.fn_Graph___init__ 9 s) stack) (.active h (Frame.fn_Graph___init__ 8 { s with t6 := (decide ((s.v1 < (0 : Int)))) }) stack)
  | Graph___init___pc10 (h : Heap) (s : State_Graph___init__) (stack : Stack) (defined : (is_Graph h (s.v0))) :
      Step (.active h (Frame.fn_Graph___init__ 10 s) stack) (.active (set_Graph_size h (s.v0) (s.v1)) (Frame.fn_Graph___init__ 9 s) stack)
  | Graph_add_edge_pc1 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Graph_add_edge (s.t4)) stack)
  | Graph_add_edge_pc2 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 2 s) stack) (.active h (Frame.fn_Graph_add_edge 1 { s with t4 := true }) stack)
  | Graph_add_edge_pc3 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (defined : (seq_Edge_optional.valid h s.t7)) :
      Step (.active h (Frame.fn_Graph_add_edge 3 s) stack) (.active (seq_Edge_optional.set h s.t7 s.t6 s.t5) (Frame.fn_Graph_add_edge 2 s) stack)
  | Graph_add_edge_pc4 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 4 s) stack) (.active h (Frame.fn_Graph_add_edge 3 { s with t6 := s.v1 }) stack)
  | Graph_add_edge_pc5 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (defined : (((field_Graph_heads h (s.v0)).isSome = true))) :
      Step (.active h (Frame.fn_Graph_add_edge 5 s) stack) (.active h (Frame.fn_Graph_add_edge 4 { s with t7 := ((field_Graph_heads h (s.v0)).getD 0) }) stack)
  | Graph_add_edge_pc6 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 6 s) stack) (.active h (Frame.fn_Edge 9 ({ v0 := s.t8, v1 := s.t9, v2 := s.t10 } : State_Edge)) ((fun value => match value with | .fn_Edge result => (Frame.fn_Graph_add_edge 5 { s with t5 := (some result) }) | _ => .invalid) :: stack))
  | Graph_add_edge_pc7 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (defined : ((((field_Graph_heads h (s.v0)).isSome = true))) ∧ ((seq_Edge_optional.get h ((field_Graph_heads h (s.v0)).getD 0) s.v1).isSome = true)) :
      Step (.active h (Frame.fn_Graph_add_edge 7 s) stack) (.active h (Frame.fn_Graph_add_edge 6 { s with t10 := ((seq_Edge_optional.get h ((field_Graph_heads h (s.v0)).getD 0) s.v1).getD none) }) stack)
  | Graph_add_edge_pc8 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 8 s) stack) (.active h (Frame.fn_Graph_add_edge 7 { s with t9 := s.v3 }) stack)
  | Graph_add_edge_pc9 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 9 s) stack) (.active h (Frame.fn_Graph_add_edge 8 { s with t8 := s.v2 }) stack)
  | Graph_add_edge_pc10 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 10 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Graph_add_edge (s.t12)) stack)
  | Graph_add_edge_pc11 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) :
      Step (.active h (Frame.fn_Graph_add_edge 11 s) stack) (.active h (Frame.fn_Graph_add_edge 10 { s with t12 := false }) stack)
  | Graph_add_edge_pc12_true (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (condition : s.t11 = true) :
      Step (.active h (Frame.fn_Graph_add_edge 12 s) stack) (.active h (Frame.fn_Graph_add_edge 11 s) stack)
  | Graph_add_edge_pc12_false (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (condition : s.t11 = false) :
      Step (.active h (Frame.fn_Graph_add_edge 12 s) stack) (.active h (Frame.fn_Graph_add_edge 9 s) stack)
  | Graph_add_edge_pc13 (h : Heap) (s : State_Graph_add_edge) (stack : Stack) (defined : (((decide ((s.v1 < (0 : Int)))) = false → ((((field_Graph_size h (s.v0)).isSome = true))))) ∧ (((decide ((s.v1 < (0 : Int)))) = false ∧ (decide ((s.v1 ≥ ((field_Graph_size h (s.v0)).getD 0)))) = false ∧ (decide ((s.v2 < (0 : Int)))) = false → ((((field_Graph_size h (s.v0)).isSome = true)))))) :
      Step (.active h (Frame.fn_Graph_add_edge 13 s) stack) (.active h (Frame.fn_Graph_add_edge 12 { s with t11 := ((decide ((s.v1 < (0 : Int)))) || (decide ((s.v1 ≥ ((field_Graph_size h (s.v0)).getD 0)))) || (decide ((s.v2 < (0 : Int)))) || (decide ((s.v2 ≥ ((field_Graph_size h (s.v0)).getD 0)))) || (decide ((s.v3 < (0 : Int))))) }) stack)
  | Edge_pc1 (h : Heap) (s : State_Edge) (stack : Stack) (defined : is_Edge h s.t4) :
      Step (.active h (Frame.fn_Edge 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Edge (s.t4)) stack)
  | Edge_pc2 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 2 s) stack) (.active h (Frame.fn_Edge 1 { s with t4 := s.v3 }) stack)
  | Edge_pc3 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 3 s) stack) (.active h (Frame.fn_Edge___init__ 5 ({ v0 := s.t6, v1 := s.t7, v2 := s.t8, v3 := s.t9 } : State_Edge___init__)) ((fun value => match value with | .fn_Edge___init__ result => (Frame.fn_Edge 2 { s with t5 := result }) | _ => .invalid) :: stack))
  | Edge_pc4 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 4 s) stack) (.active h (Frame.fn_Edge 3 { s with t9 := s.v2 }) stack)
  | Edge_pc5 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 5 s) stack) (.active h (Frame.fn_Edge 4 { s with t8 := s.v1 }) stack)
  | Edge_pc6 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 6 s) stack) (.active h (Frame.fn_Edge 5 { s with t7 := s.v0 }) stack)
  | Edge_pc7 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 7 s) stack) (.active h (Frame.fn_Edge 6 { s with t6 := s.v3 }) stack)
  | Edge_pc8 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 8 s) stack) (.active h (Frame.fn_Edge 7 { s with v3 := s.t10 }) stack)
  | Edge_pc9 (h : Heap) (s : State_Edge) (stack : Stack) :
      Step (.active h (Frame.fn_Edge 9 s) stack) (.active (h.allocateObject "graph.Edge") (Frame.fn_Edge 8 { s with t10 := h.nextObject }) stack)
  | Graph_pc1 (h : Heap) (s : State_Graph) (stack : Stack) (defined : is_Graph h s.t2) :
      Step (.active h (Frame.fn_Graph 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_Graph (s.t2)) stack)
  | Graph_pc2 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 2 s) stack) (.active h (Frame.fn_Graph 1 { s with t2 := s.v1 }) stack)
  | Graph_pc3 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 3 s) stack) (.active h (Frame.fn_Graph___init__ 10 ({ v0 := s.t4, v1 := s.t5 } : State_Graph___init__)) ((fun value => match value with | .fn_Graph___init__ result => (Frame.fn_Graph 2 { s with t3 := result }) | _ => .invalid) :: stack))
  | Graph_pc4 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 4 s) stack) (.active h (Frame.fn_Graph 3 { s with t5 := s.v0 }) stack)
  | Graph_pc5 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 5 s) stack) (.active h (Frame.fn_Graph 4 { s with t4 := s.v1 }) stack)
  | Graph_pc6 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 6 s) stack) (.active h (Frame.fn_Graph 5 { s with v1 := s.t6 }) stack)
  | Graph_pc7 (h : Heap) (s : State_Graph) (stack : Stack) :
      Step (.active h (Frame.fn_Graph 7 s) stack) (.active (h.allocateObject "graph.Graph") (Frame.fn_Graph 6 { s with t6 := h.nextObject }) stack)

theorem terminal (h : Heap) (result : Result) :
    Algo2LeanCore.Terminal Step (.done h result) := by
  intro next transition
  cases transition

end Algo2LeanGenerated

open Algo2LeanGenerated

def entry_Edge___init__ (input : Ref_Edge × Int × Int × (Option Ref_Edge)) : Frame :=
  (Frame.fn_Edge___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Edge___init__))

def Edge.__init__.ValidInput (h : Heap) (input : Ref_Edge × Int × Int × (Option Ref_Edge)) : Prop := is_Edge h input.1 ∧ (∀ ref ∈ input.2.2.2, is_Edge h ref)
def Edge.__init__.initial (h : Heap) (input : Ref_Edge × Int × Int × (Option Ref_Edge)) : Configuration :=
  Algo2LeanCore.start h (Frame.fn_Edge___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Edge___init__))
def Edge.__init__.Run (h : Heap) (input : Ref_Edge × Int × Int × (Option Ref_Edge)) (h' : Heap) (output : Unit) : Prop :=
  _root_.Algo.«graph».Edge.__init__.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph».Edge.__init__.initial h input) (.done h' (Result.fn_Edge___init__ output))
def Edge.__init__.ValidHeapTranscript (h : Heap) (input : Ref_Edge × Int × Int × (Option Ref_Edge)) (trace : Transcript) : Prop :=
  _root_.Algo.«graph».Edge.__init__.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph».Edge.__init__.initial h input) trace final
def Edge.__init__.Call (h : Heap) (input : Ref_Edge × Int × Int × (Option Ref_Edge)) (h' : Heap) (output : Unit) : Prop :=
  _root_.Algo.«graph».Edge.__init__.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_Edge___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Edge___init__)) h' (Result.fn_Edge___init__ output)
-- Complete this function from the supplied local state, under any caller stack.
def Edge.__init__.CallFrom (state : Configuration) (finalHeap : Heap) (output : Unit) : Prop :=
  match state with
  | .active heap (Frame.fn_Edge___init__ pc locals) _ =>
      Algo2LeanCore.Summary Step heap (Frame.fn_Edge___init__ pc locals) finalHeap (Result.fn_Edge___init__ output)
  | _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def Edge.__init__.load (input : Heap × (Ref_Edge × Int × Int × (Option Ref_Edge))) : Heap × (Ref_Edge × Int × Int × (Option Ref_Edge)) := input
def Edge.__init__.ValidTranscript (my_input : Heap × (Ref_Edge × Int × Int × (Option Ref_Edge))) (trace : Transcript) : Prop :=
  let loaded := _root_.Algo.«graph».Edge.__init__.load my_input
  _root_.Algo.«graph».Edge.__init__.ValidHeapTranscript loaded.1 loaded.2 trace
def Edge.__init__.Returns (my_input : Heap × (Ref_Edge × Int × Int × (Option Ref_Edge))) (my_output : Unit) : Prop :=
  let loaded := _root_.Algo.«graph».Edge.__init__.load my_input
  ∃ finalHeap, _root_.Algo.«graph».Edge.__init__.Run loaded.1 loaded.2 finalHeap my_output

theorem Edge.__init__.Call.run {before input after output}
    (call : _root_.Algo.«graph».Edge.__init__.Call before input after output) :
    _root_.Algo.«graph».Edge.__init__.Run before input after output :=
  ⟨call.1, call.2.root⟩

def entry_Graph___init__ (input : Ref_Graph × Int) : Frame :=
  (Frame.fn_Graph___init__ 10 ({ v0 := input.1, v1 := input.2 } : State_Graph___init__))

def Graph.__init__.ValidInput (h : Heap) (input : Ref_Graph × Int) : Prop := is_Graph h input.1
def Graph.__init__.initial (h : Heap) (input : Ref_Graph × Int) : Configuration :=
  Algo2LeanCore.start h (Frame.fn_Graph___init__ 10 ({ v0 := input.1, v1 := input.2 } : State_Graph___init__))
def Graph.__init__.Run (h : Heap) (input : Ref_Graph × Int) (h' : Heap) (output : Unit) : Prop :=
  _root_.Algo.«graph».Graph.__init__.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph».Graph.__init__.initial h input) (.done h' (Result.fn_Graph___init__ output))
def Graph.__init__.ValidHeapTranscript (h : Heap) (input : Ref_Graph × Int) (trace : Transcript) : Prop :=
  _root_.Algo.«graph».Graph.__init__.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph».Graph.__init__.initial h input) trace final
def Graph.__init__.Call (h : Heap) (input : Ref_Graph × Int) (h' : Heap) (output : Unit) : Prop :=
  _root_.Algo.«graph».Graph.__init__.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_Graph___init__ 10 ({ v0 := input.1, v1 := input.2 } : State_Graph___init__)) h' (Result.fn_Graph___init__ output)
-- Complete this function from the supplied local state, under any caller stack.
def Graph.__init__.CallFrom (state : Configuration) (finalHeap : Heap) (output : Unit) : Prop :=
  match state with
  | .active heap (Frame.fn_Graph___init__ pc locals) _ =>
      Algo2LeanCore.Summary Step heap (Frame.fn_Graph___init__ pc locals) finalHeap (Result.fn_Graph___init__ output)
  | _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def Graph.__init__.load (input : Heap × (Ref_Graph × Int)) : Heap × (Ref_Graph × Int) := input
def Graph.__init__.ValidTranscript (my_input : Heap × (Ref_Graph × Int)) (trace : Transcript) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.__init__.load my_input
  _root_.Algo.«graph».Graph.__init__.ValidHeapTranscript loaded.1 loaded.2 trace
def Graph.__init__.Returns (my_input : Heap × (Ref_Graph × Int)) (my_output : Unit) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.__init__.load my_input
  ∃ finalHeap, _root_.Algo.«graph».Graph.__init__.Run loaded.1 loaded.2 finalHeap my_output

theorem Graph.__init__.Call.run {before input after output}
    (call : _root_.Algo.«graph».Graph.__init__.Call before input after output) :
    _root_.Algo.«graph».Graph.__init__.Run before input after output :=
  ⟨call.1, call.2.root⟩

def entry_Graph_add_edge (input : Ref_Graph × Int × Int × Int) : Frame :=
  (Frame.fn_Graph_add_edge 13 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Graph_add_edge))

def Graph.add_edge.ValidInput (h : Heap) (input : Ref_Graph × Int × Int × Int) : Prop := is_Graph h input.1
def Graph.add_edge.initial (h : Heap) (input : Ref_Graph × Int × Int × Int) : Configuration :=
  Algo2LeanCore.start h (Frame.fn_Graph_add_edge 13 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Graph_add_edge))
def Graph.add_edge.Run (h : Heap) (input : Ref_Graph × Int × Int × Int) (h' : Heap) (output : Bool) : Prop :=
  _root_.Algo.«graph».Graph.add_edge.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph».Graph.add_edge.initial h input) (.done h' (Result.fn_Graph_add_edge output))
def Graph.add_edge.ValidHeapTranscript (h : Heap) (input : Ref_Graph × Int × Int × Int) (trace : Transcript) : Prop :=
  _root_.Algo.«graph».Graph.add_edge.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph».Graph.add_edge.initial h input) trace final
def Graph.add_edge.Call (h : Heap) (input : Ref_Graph × Int × Int × Int) (h' : Heap) (output : Bool) : Prop :=
  _root_.Algo.«graph».Graph.add_edge.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_Graph_add_edge 13 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_Graph_add_edge)) h' (Result.fn_Graph_add_edge output)
-- Complete this function from the supplied local state, under any caller stack.
def Graph.add_edge.CallFrom (state : Configuration) (finalHeap : Heap) (output : Bool) : Prop :=
  match state with
  | .active heap (Frame.fn_Graph_add_edge pc locals) _ =>
      Algo2LeanCore.Summary Step heap (Frame.fn_Graph_add_edge pc locals) finalHeap (Result.fn_Graph_add_edge output)
  | _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def Graph.add_edge.load (input : Heap × (Ref_Graph × Int × Int × Int)) : Heap × (Ref_Graph × Int × Int × Int) := input
def Graph.add_edge.ValidTranscript (my_input : Heap × (Ref_Graph × Int × Int × Int)) (trace : Transcript) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.add_edge.load my_input
  _root_.Algo.«graph».Graph.add_edge.ValidHeapTranscript loaded.1 loaded.2 trace
def Graph.add_edge.Returns (my_input : Heap × (Ref_Graph × Int × Int × Int)) (my_output : Bool) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.add_edge.load my_input
  ∃ finalHeap, _root_.Algo.«graph».Graph.add_edge.Run loaded.1 loaded.2 finalHeap my_output

theorem Graph.add_edge.Call.run {before input after output}
    (call : _root_.Algo.«graph».Graph.add_edge.Call before input after output) :
    _root_.Algo.«graph».Graph.add_edge.Run before input after output :=
  ⟨call.1, call.2.root⟩

def entry_Edge (input : Int × Int × (Option Ref_Edge)) : Frame :=
  (Frame.fn_Edge 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_Edge))

def Edge.ValidInput (h : Heap) (input : Int × Int × (Option Ref_Edge)) : Prop := (∀ ref ∈ input.2.2, is_Edge h ref)
def Edge.initial (h : Heap) (input : Int × Int × (Option Ref_Edge)) : Configuration :=
  Algo2LeanCore.start h (Frame.fn_Edge 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_Edge))
def Edge.Run (h : Heap) (input : Int × Int × (Option Ref_Edge)) (h' : Heap) (output : Ref_Edge) : Prop :=
  _root_.Algo.«graph».Edge.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph».Edge.initial h input) (.done h' (Result.fn_Edge output))
def Edge.ValidHeapTranscript (h : Heap) (input : Int × Int × (Option Ref_Edge)) (trace : Transcript) : Prop :=
  _root_.Algo.«graph».Edge.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph».Edge.initial h input) trace final
def Edge.Call (h : Heap) (input : Int × Int × (Option Ref_Edge)) (h' : Heap) (output : Ref_Edge) : Prop :=
  _root_.Algo.«graph».Edge.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_Edge 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_Edge)) h' (Result.fn_Edge output)
-- Complete this function from the supplied local state, under any caller stack.
def Edge.CallFrom (state : Configuration) (finalHeap : Heap) (output : Ref_Edge) : Prop :=
  match state with
  | .active heap (Frame.fn_Edge pc locals) _ =>
      Algo2LeanCore.Summary Step heap (Frame.fn_Edge pc locals) finalHeap (Result.fn_Edge output)
  | _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def Edge.load (input : Heap × (Int × Int × (Option Ref_Edge))) : Heap × (Int × Int × (Option Ref_Edge)) := input
def Edge.ValidTranscript (my_input : Heap × (Int × Int × (Option Ref_Edge))) (trace : Transcript) : Prop :=
  let loaded := _root_.Algo.«graph».Edge.load my_input
  _root_.Algo.«graph».Edge.ValidHeapTranscript loaded.1 loaded.2 trace
def Edge.Returns (my_input : Heap × (Int × Int × (Option Ref_Edge))) (my_output : Heap × (Ref_Edge)) : Prop :=
  let loaded := _root_.Algo.«graph».Edge.load my_input
  _root_.Algo.«graph».Edge.Run loaded.1 loaded.2 my_output.1 my_output.2

theorem Edge.Call.run {before input after output}
    (call : _root_.Algo.«graph».Edge.Call before input after output) :
    _root_.Algo.«graph».Edge.Run before input after output :=
  ⟨call.1, call.2.root⟩

def entry_Graph (input : Int) : Frame :=
  (Frame.fn_Graph 7 ({ v0 := input } : State_Graph))

def Graph.ValidInput (_h : Heap) (_input : Int) : Prop := True
def Graph.initial (h : Heap) (input : Int) : Configuration :=
  Algo2LeanCore.start h (Frame.fn_Graph 7 ({ v0 := input } : State_Graph))
def Graph.Run (h : Heap) (input : Int) (h' : Heap) (output : Ref_Graph) : Prop :=
  _root_.Algo.«graph».Graph.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph».Graph.initial h input) (.done h' (Result.fn_Graph output))
def Graph.ValidHeapTranscript (h : Heap) (input : Int) (trace : Transcript) : Prop :=
  _root_.Algo.«graph».Graph.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph».Graph.initial h input) trace final
def Graph.Call (h : Heap) (input : Int) (h' : Heap) (output : Ref_Graph) : Prop :=
  _root_.Algo.«graph».Graph.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_Graph 7 ({ v0 := input } : State_Graph)) h' (Result.fn_Graph output)
-- Complete this function from the supplied local state, under any caller stack.
def Graph.CallFrom (state : Configuration) (finalHeap : Heap) (output : Ref_Graph) : Prop :=
  match state with
  | .active heap (Frame.fn_Graph pc locals) _ =>
      Algo2LeanCore.Summary Step heap (Frame.fn_Graph pc locals) finalHeap (Result.fn_Graph output)
  | _ => False
-- The value view gives each sequence input its own object.
def Graph.load (input : Int) : Heap × (Int) :=
  let h0 : Heap := {}
  (h0, input)
def Graph.ValidTranscript (my_input : Int) (trace : Transcript) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.load my_input
  _root_.Algo.«graph».Graph.ValidHeapTranscript loaded.1 loaded.2 trace
def Graph.Returns (my_input : Int) (my_output : Heap × (Ref_Graph)) : Prop :=
  let loaded := _root_.Algo.«graph».Graph.load my_input
  _root_.Algo.«graph».Graph.Run loaded.1 loaded.2 my_output.1 my_output.2

theorem Graph.Call.run {before input after output}
    (call : _root_.Algo.«graph».Graph.Call before input after output) :
    _root_.Algo.«graph».Graph.Run before input after output :=
  ⟨call.1, call.2.root⟩

end Algo.«graph»