inductive Person : Type

• A : Person
• B : Person
• C : Person
• E : Person

@[implicit_reducible]

instance instDecidableEqPerson : DecidableEq Person

Equations

• instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instFintypePerson : Fintype Person

Equations

• instFintypePerson = { elems := {Person.A, Person.B, Person.C, Person.E}, complete := instFintypePerson._proof_1 }

instance instNonemptyPerson : Nonempty Person

def exampleEdges : Multiset (Person × Person)

Equations

• exampleEdges = ↑[(Person.A, Person.B), (Person.B, Person.C), (Person.C, Person.E)]

def edgesWithLoop : Multiset (Person × Person)

Equations

• edgesWithLoop = ↑[(Person.A, Person.B), (Person.A, Person.A), (Person.B, Person.C)]

def example_graph : CFGraph

Equations

• One or more equations did not get rendered due to their size.

def initial_wealth : CFDiv example_graph

Equations

• initial_wealth Person.A = 2
• initial_wealth Person.B = -3
• initial_wealth Person.C = 4
• initial_wealth Person.E = -1

def after_charlie_lends : CFDiv example_graph

Equations

• after_charlie_lends = firing_move example_graph initial_wealth Person.C

def W₁ : Finset example_graph.V

Equations

• W₁ = {Person.A, Person.E, Person.C}

def after_W₁_firing : CFDiv example_graph

Equations

• after_W₁_firing = set_firing example_graph initial_wealth W₁

def W₂ : Finset example_graph.V

Equations

• W₂ = W₁

def after_W₂_firing : CFDiv example_graph

Equations

• after_W₂_firing = set_firing example_graph after_W₁_firing W₂

def W₃ : Finset example_graph.V

Equations

• W₃ = {Person.B, Person.C}

def after_W₃_firing : CFDiv example_graph

Equations

• after_W₃_firing = set_firing example_graph after_W₂_firing W₃

def after_bob_borrows : CFDiv example_graph

Equations

• after_bob_borrows = borrowing_move example_graph initial_wealth Person.B

def example_laplacian : Matrix example_graph.V example_graph.V ℤ

Equations

• example_laplacian = laplacian_matrix example_graph

def firing_script_example : firing_script example_graph

Equations

• firing_script_example Person.A = 0
• firing_script_example Person.B = -1
• firing_script_example Person.C = 1
• firing_script_example Person.E = 0

def res_div_post_lap_based_script_firing : CFDiv example_graph

Equations

• res_div_post_lap_based_script_firing = apply_laplacian example_graph firing_script_example initial_wealth

def non_q_reduced_example : CFDiv example_graph

Equations

• non_q_reduced_example Person.A = 1
• non_q_reduced_example Person.B = -1
• non_q_reduced_example Person.C = 2
• non_q_reduced_example Person.E = 1