toy — a customer germ, grown on foam

import Face
open Face
set_option autoImplicit false
universe u v w

namespace Toy

def counter : Machine Unit Nat := tally

def flipper : Machine Unit Bool := flip

theorem the_toy_counts (w : List Unit) : behavior counter w = w.length :=
  by (intros; (apply Face.the_wider_voice_releases_the_bank <;> fail))

/-- info: 'Toy.the_toy_counts' does not depend on any axioms -/
#guard_msgs in #print axioms the_toy_counts

theorem the_toy_parks (w : List Unit) (s : Nat) : park counter s w = s + w.length :=
  by (intros; (apply Face.the_tally_parks_at_its_count <;> fail))

/-- info: 'Toy.the_toy_parks' does not depend on any axioms -/
#guard_msgs in #print axioms the_toy_parks

theorem the_toy_resumes (u v : List Unit) (s : Nat) :
    park counter s (u ++ v) = park counter (park counter s u) v :=
  by (intros; (apply Face.the_park_resumes <;> fail))

/-- info: 'Toy.the_toy_resumes' does not depend on any axioms -/
#guard_msgs in #print axioms the_toy_resumes

theorem the_toy_flips_back : ∀ b : Bool, park flipper b [(), ()] = b :=
  by (intros; (try dsimp only [Face.park, flipper] at *); intros; (apply Room.not_not <;> fail))

/-- info: 'Toy.the_toy_flips_back' does not depend on any axioms -/
#guard_msgs in #print axioms the_toy_flips_back

end Toy

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

graph LR
  subgraph Toy["Toy"]
    the_toy_counts["the_toy_counts"]
    the_toy_flips_back["the_toy_flips_back"]
    the_toy_parks["the_toy_parks"]
    the_toy_resumes["the_toy_resumes"]
  end
  subgraph Face["Face"]
    Face_the_park_resumes["the_park_resumes"]
    Face_the_tally_parks_at_its_count["the_tally_parks_at_its_count"]
    Face_the_wider_voice_releases_the_bank["the_wider_voice_releases_the_bank"]
  end
  the_toy_parks --> Face_the_tally_parks_at_its_count
  the_toy_resumes --> Face_the_park_resumes
  the_toy_counts --> Face_the_wider_voice_releases_the_bank