Face — the seeing, grown from germ/Face.lean

import Room
open Room

namespace Face

universe u v w u' v' w' u''

structure Face where
  State : Type u
  Probe : Type v
  Ans   : Type w
  obs   : State → Probe → Ans

def alike (F : Face) (s t : F.State) : Prop :=
  ∀ p, F.obs s p = F.obs t p

def appFace (P : Type v) (A : Type w) : Face :=
  ⟨P → A, P, A, fun g p => g p⟩

def reseat (F : Face) {S' : Type u'} (h : S' → F.State) : Face :=
  ⟨S', F.Probe, F.Ans, fun s p => F.obs (h s) p⟩

def rehear (F : Face) {Q : Type v'} (f : Q → F.Probe) : Face :=
  ⟨F.State, Q, F.Ans, fun s q => F.obs s (f q)⟩

def retell (F : Face) {B : Type w'} (g : F.Ans → B) : Face :=
  ⟨F.State, F.Probe, B, fun s p => g (F.obs s p)⟩

inductive Interview (P : Type v) (A : Type w) where
  | rest : Interview P A
  | ask  : P → (A → Interview P A) → Interview P A

def sound (F : Face) (s : F.State) : Interview F.Probe F.Ans → List F.Ans
  | .rest => []
  | .ask p k => F.obs s p :: sound F s (k (F.obs s p))

def door (H : Type u) (W : Type v) : Type (max u v) :=
  H × W

def atTheDoor {H : Type u} {W : Type v} (h : H) (w : W) : door H W :=
  (h, w)

def face {H : Type u} {W : Type v} (d : door H W) : H :=
  d.1

def met {H : Type u} {W : Type v} (d : door H W) : W :=
  d.2

def turnAbout {H : Type u} {W : Type v} (d : door H W) : door W H :=
  atTheDoor (met d) (face d)

inductive fork (P : Type v) (Q : Type v') where
  | viaLeft  : P → fork P Q
  | viaRight : Q → fork P Q

def greet {P : Type v} {Q : Type v'} {X : Type w} (f : P → X) (g : Q → X) : fork P Q → X
  | .viaLeft p => f p
  | .viaRight q => g q

def crossOver {P : Type v} {Q : Type v'} : fork P Q → fork Q P
  | .viaLeft p => .viaRight p
  | .viaRight q => .viaLeft q

def deepen {H : Type u} {W : Type v} {V : Type w} (d : door (door H W) V) :
    door H (door W V) :=
  atTheDoor (face (face d)) (atTheDoor (met (face d)) (met d))

def shallow {H : Type u} {W : Type v} {V : Type w} (d : door H (door W V)) :
    door (door H W) V :=
  atTheDoor (atTheDoor (face d) (face (met d))) (met (met d))

def distribute {H : Type u} {W : Type v} {V : Type w} (d : door H (fork W V)) :
    fork (door H W) (door H V) :=
  greet (fun w => .viaLeft (atTheDoor (face d) w)) (fun v => .viaRight (atTheDoor (face d) v))
    (met d)

def collect {H : Type u} {W : Type v} {V : Type w} : fork (door H W) (door H V) → door H (fork W V) :=
  greet (fun d => atTheDoor (face d) (.viaLeft (met d)))
        (fun d => atTheDoor (face d) (.viaRight (met d)))

def holdOpen {H : Type u} {W : Type v} {X : Type w} (g : door H W → X) : H → W → X :=
  fun h w => g (atTheDoor h w)

def walkIn {H : Type u} {W : Type v} {X : Type w} (g : H → W → X) : door H W → X :=
  fun d => g (face d) (met d)

def faceOf {H : Type u} {W : Type v} {X : Type w} (g : door H W → X) : Face :=
  ⟨H, W, X, holdOpen g⟩

def host (F : Face) (W : Type v') : Face :=
  reseat F (fun d : door F.State W => face d)

def vertical {H : Type u} {W : Type v} (σ : door H W → W) (d : door H W) : door H W :=
  atTheDoor (face d) (σ d)

def selfMeet (F : Face) (r : F.State → F.Probe) (s : F.State) : F.Ans :=
  F.obs s (r s)

def sharpen (F : Face) {X : Type w'} (r : F.State → X) : Face :=
  ⟨F.State, fork F.Probe Unit, fork F.Ans X,
   fun s => greet (fun p => .viaLeft (F.obs s p)) (fun _ => .viaRight (r s))⟩

def widen (F : Face) (W : Type v') : Face :=
  sharpen (host F W) met

def pairFace (F G : Face) {S : Type u'} (f : S → F.State) (g : S → G.State) : Face :=
  ⟨S, door F.Probe G.Probe, door F.Ans G.Ans,
   fun s pq => atTheDoor (F.obs (f s) (face pq)) (G.obs (g s) (met pq))⟩

def originFace (S' : Type u') : Face :=
  ⟨S', Unit, Unit, fun _ _ => ()⟩

def unheard (F : Face) (m : F.State → F.State) : Prop :=
  ∀ s, alike F (m s) s

def exchange {H : Type u} {W : Type v} (σ : door H W → W) (d : door H W) : door W H :=
  turnAbout (vertical σ d)

structure Machine (I : Type u) (O : Type v) where
  S    : Type w
  s0   : S
  step : S → I → S
  out  : S → O

def park {I : Type u} {O : Type v} (m : Machine I O) (s : m.S) : List I → m.S
  | [] => s
  | i :: w => park m (m.step s i) w

def drive {I : Type u} {O : Type v} (m : Machine I O) (s : m.S) (w : List I) : O :=
  m.out (park m s w)

def behavior {I : Type u} {O : Type v} (m : Machine I O) (w : List I) : O :=
  drive m m.s0 w

def airGap (I : Type u) (O : Type v) : Face :=
  reseat (appFace (List I) O) (fun m : Machine.{u, v, w} I O => behavior m)

def retune {I : Type u} {I' : Type u'} {O : Type v} (f : I → I') (m : Machine I' O) :
    Machine I O :=
  ⟨m.S, m.s0, fun s i => m.step s (f i), m.out⟩

def revoice {I : Type u} {O : Type v} {O' : Type v'} (g : O → O') (m : Machine I O) :
    Machine I O' :=
  ⟨m.S, m.s0, m.step, fun s => g (m.out s)⟩

def tally : Machine Unit Nat :=
  ⟨Nat, 0, fun s _ => s + 1, fun s => s⟩

def flip : Machine Unit Bool :=
  ⟨Bool, false, fun s _ => !s, fun s => s⟩

def paceOne : Machine Unit Bool :=
  ⟨Nat, 0, fun s _ => s + 1, oddNat⟩

inductive Plan where
  | ground : Plan
  | board  : Plan → Plan → Plan

def fold {A : Type u} (op : A → A → A) (base : A) : Plan → A
  | .ground => base
  | .board p q => op (fold op base p) (fold op base q)

def reading : Plan → Nat :=
  fold (fun a b => a + b) 1

def graft (base : Plan) : Plan → Plan :=
  fold .board base

def build (W : Type u) : Plan → Type u :=
  fold (fun A B : Type u => door A B) W

def reground {W : Type u} {W' : Type v} (f : W → W') : (p : Plan) → build W p → build W' p
  | .ground, w => f w
  | .board p q, d => atTheDoor (reground f p (face d)) (reground f q (met d))

def pour {W : Type u} : (p : Plan) → build W p → List W
  | .ground, w => [w]
  | .board p q, d => pour p (face d) ++ pour q (met d)

def reboardAux {W : Type u} (w0 : W) : (p : Plan) → List W → build W p × List W
  | .ground => fun l =>
      match l with
      | [] => (w0, [])
      | w :: t => (w, t)
  | .board p q => fun l =>
      (atTheDoor (reboardAux w0 p l).1 (reboardAux w0 q (reboardAux w0 p l).2).1,
       (reboardAux w0 q (reboardAux w0 p l).2).2)

def reboard {W : Type u} (w0 : W) (p : Plan) (l : List W) : build W p :=
  (reboardAux w0 p l).1

def drain {W : Type u} (w0 : W) (p : Plan) (l : List W) : List W :=
  pour p (reboard w0 p l)

def cross : List Plan → List Plan → List Plan
  | [], _ => []
  | p :: ps, qs => qs.map (Plan.board p) ++ cross ps qs

def allPlans : Nat → List Plan
  | 0 => [.ground]
  | d + 1 => .ground :: cross (allPlans d) (allPlans d)

def census : Nat → Nat
  | 0 => 0
  | k + 1 => ((allPlans k).filter (fun p => Nat.beq (reading p) (k + 1))).length

def recite {P : Type v} {A : Type w} : List P → Interview P A
  | [] => .rest
  | p :: ps => .ask p (fun _ => recite ps)

def restingCounter : Machine Unit Bool :=
  ⟨Nat, 0, fun n _ => n + 1, fun _ => true⟩

def hollowShell : Machine Unit Bool :=
  ⟨Unit, (), fun _ _ => (), fun _ => true⟩

def selfSteered {I : Type u} {O : Type v} (m : Machine I O) (r : m.S → I) :
    Machine Unit O :=
  ⟨m.S, m.s0, fun s _ => m.step s (r s), m.out⟩

def orbit {I : Type u} {O : Type v} (m : Machine I O) (r : m.S → I) :
    m.S → Nat → m.S
  | s, 0 => s
  | s, n + 1 => orbit m r (m.step s (r s)) n

def selfWord {I : Type u} {O : Type v} (m : Machine I O) (r : m.S → I) :
    m.S → Nat → List I
  | _, 0 => []
  | s, n + 1 => r s :: selfWord m r (m.step s (r s)) n

def buffered {I : Type u} {O : Type v} (m : Machine I O) : Machine I O :=
  ⟨m.S × List I, (m.s0, []), fun st i => (st.1, st.2 ++ [i]),
   fun st => drive m st.1 st.2⟩

def settleHeld {I : Type u} {O : Type v} (m : Machine I O)
    (st : m.S × List I) : m.S × List I :=
  (park m st.1 st.2, [])

def ledger (I : Type u) : Machine I (List I) :=
  ⟨List I, [], fun rec i => rec ++ [i], fun rec => rec⟩

def replayer {I : Type u} {O : Type v} (m : Machine I O) : Machine I O :=
  ⟨List I, [], fun rec i => rec ++ [i], fun rec => m.out (park m m.s0 rec)⟩

inductive reassoc : Plan → Plan → Prop
  | here (a b c : Plan) :
      reassoc (.board (.board a b) c) (.board a (.board b c))
  | left {p q : Plan} (r : Plan) :
      reassoc p q → reassoc (.board p r) (.board q r)
  | right (r : Plan) {p q : Plan} :
      reassoc p q → reassoc (.board r p) (.board r q)

inductive chain : Nat → Plan → Plan → Prop
  | rest (p : Plan) : chain 0 p p
  | step {n : Nat} {p q r : Plan} :
      reassoc p q → chain n q r → chain (n + 1) p r

def sheet (I : Type u) (O : Type v) : Type (max u v) :=
  List I → O

def peek {I : Type u} {O : Type v} (f : sheet I O) : O :=
  f []

def feed {I : Type u} {O : Type v} (f : sheet I O) (i : I) : sheet I O :=
  fun w => f (i :: w)

def liftFrom {I : Type u} {O : Type v} (m : Machine I O) (s : m.S) : sheet I O :=
  fun w => drive m s w

def inStep {I : Type u} {O : Type v} (m : Machine I O) (h : m.S → sheet I O) : Prop :=
  (∀ s, peek (h s) = m.out s) ∧ (∀ s i, feed (h s) i = h (m.step s i))

def stream (A : Type u) : Type u :=
  Nat → A

def toStream {O : Type v} (f : sheet Unit O) : stream O :=
  fun n => f (List.replicate n ())

def toSheet {O : Type v} (g : stream O) : sheet Unit O :=
  fun w => g w.length

def streamOf {O : Type v} (m : Machine Unit O) : stream O :=
  fun n => m.out (orbit m (fun _ => ()) m.s0 n)

def Derived (F : Face) (P : F.State → Prop) : Prop :=
  ∀ s t, alike F s t → (P s ↔ P t)

def concordFace (F : Face) (V : Type v') : Face :=
  pairFace (host F V) ⟨door F.State V, Unit, V, fun x _ => met x⟩ (fun x => x) (fun x => x)

def differOnly (F : Face) (x y : F.State) (p : F.Probe) : Prop :=
  ∀ q, q ≠ p → F.obs x q = F.obs y q

theorem no_interview_parts_the_alike (F : Face) {s t : F.State} (h : alike F s t) :
    ∀ q, sound F s q = sound F t q
  | .rest => rfl
  | .ask p k => by
      show F.obs s p :: sound F s (k (F.obs s p)) = F.obs t p :: sound F t (k (F.obs t p))
      rw [h p]
      exact congrArg (List.cons (F.obs t p))
        (no_interview_parts_the_alike F h (k (F.obs t p)))

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

theorem the_interview_crosses_the_carrier {S : Type u} {T : Type u'} {P : Type v} {A : Type w}
    (f : S → P → A) (g : T → P → A) (h : S → T) (c : carries f g h) (s : S) :
    ∀ q, sound ⟨T, P, A, g⟩ (h s) q = sound ⟨S, P, A, f⟩ s q
  | .rest => rfl
  | .ask p k => by
      show g (h s) p :: sound ⟨T, P, A, g⟩ (h s) (k (g (h s) p))
         = f s p :: sound ⟨S, P, A, f⟩ s (k (f s p))
      rw [c s p]
      exact congrArg (List.cons (f s p))
        (the_interview_crosses_the_carrier f g h c s (k (f s p)))

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

theorem a_guest_blind_reading_is_a_face_reading {H : Type u} {W : Type v} {X : Type w}
    (r : door H W → X) (w0 : W) :
    (∀ h w w', r (atTheDoor h w) = r (atTheDoor h w')) ↔
    (∀ d, r d = r (atTheDoor (face d) w0)) :=
  ⟨fun hb d => hb (face d) (met d) w0,
   fun hf h w w' => (hf (atTheDoor h w)).trans (hf (atTheDoor h w')).symm⟩

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

theorem the_pairing_is_unique {H : Type u} {W : Type v} {X : Type w}
    (f : X → H) (g : X → W) (u : X → door H W)
    (hf : ∀ x, face (u x) = f x) (hg : ∀ x, met (u x) = g x) (x : X) :
    u x = atTheDoor (f x) (g x) :=
  (congr (congrArg atTheDoor (hf x)) (hg x) :
    atTheDoor (face (u x)) (met (u x)) = atTheDoor (f x) (g x))

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

theorem any_ready_greeter_is_the_greeter {P : Type v} {Q : Type v'} {X : Type w}
    (f : P → X) (g : Q → X) (h : fork P Q → X)
    (hl : ∀ p, h (.viaLeft p) = f p) (hr : ∀ q, h (.viaRight q) = g q) :
    ∀ e, h e = greet f g e :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; (apply hl <;> fail))
          | (intros; (apply hr <;> fail))))

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

theorem the_host_serves_both_branches {H : Type u} {W : Type v} {V : Type w} :
    ∀ d : door H (fork W V), collect (distribute d) = d
  | (_, .viaLeft _) => rfl
  | (_, .viaRight _) => rfl

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

theorem the_sharpening_is_exact (F : Face) {X : Type w'} (r : F.State → X) (s t : F.State) :
    alike (sharpen F r) s t ↔ (alike F s t ∧ r s = r t) :=
  ⟨fun h =>
    ⟨fun p => congrArg (greet (fun a => a) (fun _ => F.obs s p)) (h (.viaLeft p)),
     congrArg (greet (fun _ => r s) (fun x => x)) (h (.viaRight ()))⟩,
   fun h q =>
    match q with
    | .viaLeft p => congrArg fork.viaLeft (h.1 p)
    | .viaRight _ => congrArg fork.viaRight h.2⟩

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

theorem the_widening_is_exact (F : Face) {W : Type v'} (d d' : door F.State W) :
    alike (widen F W) d d' ↔ (alike F (face d) (face d') ∧ met d = met d') :=
  ⟨fun h =>
    ⟨fun p => congrArg (greet (fun a => a) (fun _ => F.obs (face d) p)) (h (fork.viaLeft p)),
     congrArg (greet (fun _ => met d) (fun x => x)) (h (fork.viaRight ()))⟩,
   fun h q =>
    match q with
    | .viaLeft p => congrArg fork.viaLeft (h.1 p)
    | .viaRight _ => congrArg fork.viaRight h.2⟩

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

theorem the_pairing_is_exact (F G : Face) {S : Type u'}
    (f : S → F.State) (g : S → G.State) (p0 : F.Probe) (q0 : G.Probe) (s t : S) :
    alike (pairFace F G f g) s t ↔ (alike F (f s) (f t) ∧ alike G (g s) (g t)) :=
  ⟨fun h =>
    ⟨fun p => congrArg face (h (atTheDoor p q0)),
     fun q => congrArg met (h (atTheDoor p0 q))⟩,
   fun h pq =>
    (congr (congrArg atTheDoor (h.1 (face pq))) (h.2 (met pq)) :
      atTheDoor (F.obs (f s) (face pq)) (G.obs (g s) (met pq))
        = atTheDoor (F.obs (f t) (face pq)) (G.obs (g t) (met pq)))⟩

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

theorem the_origin_is_the_pairs_unit (F : Face) {S : Type u'} {S' : Type v'}
    (f : S → F.State) (g : S → S') (s t : S) :
    alike (pairFace F (originFace S') f g) s t ↔ alike F (f s) (f t) :=
  ⟨fun h p => congrArg face (h (atTheDoor p ())),
   fun h pq => congrArg (fun a => atTheDoor a ()) (h (face pq))⟩

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

theorem the_unheard_hands_compose (F : Face) (m n : F.State → F.State)
    (hm : unheard F m) (hn : unheard F n) : unheard F (fun s => m (n s)) :=
  by (intros; (try dsimp only [unheard, Face] at *); intros; (apply Room.the_carriers_compose <;> assumption))

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

theorem the_yield_fixes_the_agreed {H : Type u} (d : door H H) :
    turnAbout d = d ↔ met d = face d :=
  ⟨fun h => congrArg face h,
   fun h =>
    (congr (congrArg atTheDoor h) h.symm :
      atTheDoor (met d) (face d) = atTheDoor (face d) (met d))⟩

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

theorem no_move_at_the_ground : ∀ {q : Plan}, ¬ reassoc .ground q :=
  fun h => nomatch h

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

theorem the_two_shapes_of_three :
    reassoc (.board (.board .ground .ground) .ground)
        (.board .ground (.board .ground .ground))
      ∧ reading (.board (.board .ground .ground) .ground)
          = reading (.board .ground (.board .ground .ground))
      ∧ (.board (.board .ground .ground) .ground : Plan)
          ≠ .board .ground (.board .ground .ground)
      ∧ census 3 = 2 :=
  ⟨.here .ground .ground .ground,
   rfl,
   (fun h => nomatch (Plan.board.inj h).1),
   rfl⟩

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

theorem the_pentagon_turns_at_four :
    chain 2 (.board (.board (.board .ground .ground) .ground) .ground)
        (.board .ground (.board .ground (.board .ground .ground)))
      ∧ chain 3 (.board (.board (.board .ground .ground) .ground) .ground)
          (.board .ground (.board .ground (.board .ground .ground))) :=
  ⟨.step (.here (.board .ground .ground) .ground .ground)
     (.step (.here .ground .ground (.board .ground .ground)) (.rest _)),
   .step (.left .ground (.here .ground .ground .ground))
     (.step (.here .ground (.board .ground .ground) .ground)
       (.step (.right .ground (.here .ground .ground .ground)) (.rest _)))⟩

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

theorem the_lift_is_unique {I : Type u} {O : Type v} (m : Machine I O)
    (h : m.S → sheet I O) (hf : inStep m h) :
    ∀ (w : List I) (s : m.S), h s w = liftFrom m s w
  | [], s => hf.1 s
  | i :: w, s =>
      (congrFun (hf.2 s i) w).trans
        (the_lift_is_unique m h hf w (m.step s i))

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

theorem a_role_read_at_a_probe_is_derived (F : Face) (p : F.Probe) (Q : F.Ans → Prop) :
    Derived F (fun s => Q (F.obs s p)) :=
  fun s t h => by
    show Q (F.obs s p) ↔ Q (F.obs t p)
    rw [h p]

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

theorem the_window_agrees_or_names_the_gap (F : Face)
    (beq : F.Ans → F.Ans → Bool) (s t : F.State) :
    ∀ ps : List F.Probe,
      (∀ p, p ∈ ps → beq (F.obs s p) (F.obs t p) = true)
        ∨ ∃ p, p ∈ ps ∧ beq (F.obs s p) (F.obs t p) = false
  | [] => Or.inl (fun _ hp => nomatch hp)
  | p :: ps => by
      cases hb : beq (F.obs s p) (F.obs t p) with
      | false => exact Or.inr ⟨p, List.Mem.head ps, hb⟩
      | true =>
          cases the_window_agrees_or_names_the_gap F beq s t ps with
          | inl hall =>
              refine Or.inl (fun q hq => ?_)
              cases hq with
              | head => exact hb
              | tail _ hq' => exact hall q hq'
          | inr hw =>
              obtain ⟨q, hq, hbq⟩ := hw
              exact Or.inr ⟨q, List.Mem.tail p hq, hbq⟩

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

theorem the_agreed_window_sounds_as_one (F : Face) (s t : F.State) :
    ∀ ps : List F.Probe, (∀ p, p ∈ ps → F.obs s p = F.obs t p) →
      sound F s (recite ps) = sound F t (recite ps)
  | [], _ => rfl
  | p :: ps, h => by
      show F.obs s p :: sound F s (recite ps) = F.obs t p :: sound F t (recite ps)
      rw [h p (List.Mem.head ps),
          the_agreed_window_sounds_as_one F s t ps (fun q hq => h q (List.Mem.tail p hq))]

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

theorem the_mutual_records_ride_together (F : Face.{u, v, w}) {V : Type v'} {W : Type w'}
    (mine : door F.State (door V W) → V) (yours : door F.State (door V W) → W) :
    unheard (host F (door V W)) (fun x => atTheDoor (face x) (atTheDoor (mine x) (met (met x))))
      ∧ unheard (host F (door V W)) (fun x => atTheDoor (face x) (atTheDoor (face (met x)) (yours x)))
      ∧ unheard (host F (door V W)) (fun x => atTheDoor (face x) (atTheDoor (mine x) (yours x))) :=
  ⟨fun _ _ => rfl, fun _ _ => rfl, fun _ _ => rfl⟩

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

theorem the_records_part_the_seats (F : Face.{u, v, w}) {V : Type v'} {W : Type w'}
    (s : F.State) {v v' : V} (hv : v ≠ v') (w : W) :
    alike (host F (door V W)) (atTheDoor s (atTheDoor v w)) (atTheDoor s (atTheDoor v' w))
      ∧ atTheDoor s (atTheDoor v w) ≠ atTheDoor s (atTheDoor v' w)
      ∧ (widen F (door V W)).obs (atTheDoor s (atTheDoor v w)) (.viaRight ())
          ≠ (widen F (door V W)).obs (atTheDoor s (atTheDoor v' w)) (.viaRight ()) :=
  ⟨fun _ => rfl,
   fun he => hv (congrArg (fun y => face (met y)) he),
   fun he => hv (congrArg face (fork.viaRight.inj he))⟩

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

theorem no_seat_reads_the_concord_alone (F : Face) {V : Type v'}
    (p₀ : F.Probe) (s : F.State) {v v' : V} (hv : v ≠ v') :
    alike (host F V) (atTheDoor s v) (atTheDoor s v')
      ∧ ¬ alike (concordFace F V) (atTheDoor s v) (atTheDoor s v') :=
  ⟨fun _ => rfl,
   fun hal => hv (congrArg met (hal (atTheDoor p₀ ())))⟩

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

theorem the_concord_agrees_or_names_the_gap (F : Face) {V : Type v'}
    (beq : F.Ans → V → Bool) (x : door F.State V) :
    ∀ ps : List F.Probe,
      (∀ p, p ∈ ps → beq (F.obs (face x) p) (met x) = true)
        ∨ ∃ p, p ∈ ps ∧ beq (F.obs (face x) p) (met x) = false
  | [] => Or.inl (fun _ hp => nomatch hp)
  | p :: ps => by
      cases hb : beq (F.obs (face x) p) (met x) with
      | false => exact Or.inr ⟨p, List.Mem.head ps, hb⟩
      | true =>
          cases the_concord_agrees_or_names_the_gap F beq x ps with
          | inl hall =>
              refine Or.inl (fun r hr => ?_)
              cases hr with
              | head => exact hb
              | tail _ hr' => exact hall r hr'
          | inr hw =>
              obtain ⟨r, hr, hbr⟩ := hw
              exact Or.inr ⟨r, List.Mem.tail p hr, hbr⟩

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

theorem the_gap_is_minted_at_the_meeting (F : Face) {V : Type v'}
    (p₀ : F.Probe) (s : F.State) {v v' : V} (hv : v ≠ v') :
    alike (host F V) (atTheDoor s v) (atTheDoor s v')
      ∧ met ((concordFace F V).obs (atTheDoor s v) (atTheDoor p₀ ()))
          ≠ met ((concordFace F V).obs (atTheDoor s v') (atTheDoor p₀ ())) :=
  ⟨fun _ => rfl, hv⟩

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

theorem the_pointwise_license (P : Type v) (A : Type w) (g h : P → A) :
    alike (appFace P A) g h ↔ ∀ p, g p = h p :=
  Iff.rfl

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

theorem one_face_many_seats (F : Face) :
    reseat (appFace F.Probe F.Ans) F.obs = F :=
  rfl

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

theorem the_seat_map_carries_the_conduct (F : Face) (s t : F.State) :
    alike F s t ↔ alike (appFace F.Probe F.Ans) (F.obs s) (F.obs t) :=
  Iff.rfl

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

theorem the_seats_stack_backward (F : Face) {S' : Type u'} {S'' : Type u''}
    (h : S' → F.State) (h' : S'' → S') :
    reseat (reseat F h) h' = reseat F (fun s => h (h' s)) :=
  rfl

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

theorem the_ear_and_the_voice_commute (F : Face) {Q : Type v'} {B : Type w'}
    (f : Q → F.Probe) (g : F.Ans → B) :
    rehear (retell F g) f = retell (rehear F f) g :=
  rfl

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

theorem the_ear_crosses_the_seat (F : Face) {S' : Type u'} {Q : Type v'}
    (h : S' → F.State) (f : Q → F.Probe) :
    rehear (reseat F h) f = reseat (rehear F f) h :=
  rfl

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

theorem the_voice_crosses_the_seat (F : Face) {S' : Type u'} {B : Type w'}
    (h : S' → F.State) (g : F.Ans → B) :
    retell (reseat F h) g = reseat (retell F g) h :=
  rfl

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

theorem the_carrier_was_a_seating {S : Type u} {T : Type u'} {P : Type v} {A : Type w}
    (f : S → P → A) (g : T → P → A) (h : S → T) :
    carries f g h ↔ ∀ s, alike (appFace P A) (g (h s)) (f s) :=
  Iff.rfl

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

theorem the_obs_carries_to_the_one_face (F : Face) :
    carries F.obs (fun g p => g p) F.obs :=
  fun _ _ => rfl

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

theorem no_face_reads_the_guest {H : Type u} {W : Type v} {X : Type w}
    (g : H → X) (h : H) (w w' : W) :
    g (face (atTheDoor h w)) = g (face (atTheDoor h w')) :=
  rfl

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

theorem the_guest_is_real {H : Type u} {W : Type v} (h : H) (w : W) :
    met (atTheDoor h w) = w :=
  rfl

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

theorem the_turn_returns {H : Type u} {W : Type v} (d : door H W) :
    turnAbout (turnAbout d) = d :=
  rfl

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

theorem the_crossing_returns {P : Type v} {Q : Type v'} :
    ∀ e : fork P Q, crossOver (crossOver e) = e :=
  by (intro x; induction x; all_goals ((intros; rfl)))

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

theorem hosting_associates {H : Type u} {W : Type v} {V : Type w} (d : door (door H W) V) :
    shallow (deepen d) = d :=
  rfl

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

theorem hosting_associates_back {H : Type u} {W : Type v} {V : Type w} (d : door H (door W V)) :
    deepen (shallow d) = d :=
  rfl

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

theorem the_branches_come_home {H : Type u} {W : Type v} {V : Type w} :
    ∀ e : fork (door H W) (door H V), distribute (collect e) = e :=
  by (intro x; induction x; all_goals ((intros; rfl)))

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

theorem the_deferral_is_free {H : Type u} {W : Type v} {X : Type w}
    (g : door H W → X) (d : door H W) :
    walkIn (holdOpen g) d = g d :=
  rfl

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

theorem the_holding_returns {H : Type u} {W : Type v} {X : Type w}
    (g : H → W → X) (h : H) (w : W) :
    holdOpen (walkIn g) h w = g h w :=
  rfl

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

theorem the_face_was_a_held_door (F : Face) : faceOf (walkIn F.obs) = F :=
  rfl

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

theorem every_door_reading_is_a_face {H : Type u} {W : Type v} {X : Type w}
    (g : door H W → X) (d : door H W) :
    walkIn (faceOf g).obs d = g d :=
  rfl

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

theorem the_measurement_is_a_meeting (F : Face) (s : F.State) (p : F.Probe) :
    F.obs s p = walkIn F.obs (atTheDoor s p) :=
  rfl

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

theorem the_host_was_a_reseat (F : Face) (W : Type v') :
    host F W = reseat F (fun d : door F.State W => face d) :=
  rfl

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

theorem the_host_merges_the_guests (F : Face) (W : Type v') (s : F.State) (w w' : W) :
    alike (host F W) (atTheDoor s w) (atTheDoor s w') :=
  fun _ => rfl

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

theorem the_probe_boards_as_the_guest (F : Face) (s : F.State) (p : F.Probe) :
    selfMeet (host F F.Probe) met (atTheDoor s p) = F.obs s p :=
  rfl

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

theorem the_meeting_was_a_self_meeting {H : Type u} {W : Type v} {X : Type w}
    (g : door H W → X) (d : door H W) :
    selfMeet (host (faceOf g) W) met d = g d :=
  rfl

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

theorem the_self_meeting_reads_the_guest (F : Face) {W : Type v'}
    (r : W → F.Probe) (s : F.State) (w : W) :
    selfMeet (host F W) (fun d => r (met d)) (atTheDoor s w) = F.obs s (r w) :=
  rfl

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

theorem a_guest_mover_is_unheard (F : Face) {W : Type v'} (σ : door F.State W → W)
    (d : door F.State W) : alike (host F W) (vertical σ d) d :=
  fun _ => rfl

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

theorem the_origin_merges_every_seat {S' : Type u'} (s t : S') :
    alike (originFace S') s t :=
  fun _ => rfl

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

theorem the_still_hand_is_unheard (F : Face) : unheard F (fun s => s) :=
  fun _ _ => rfl

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

theorem the_maintenance_is_the_identitys_hom (F : Face) (m : F.State → F.State) :
    unheard F m ↔ carries F.obs F.obs m :=
  Iff.rfl

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

theorem the_spoken_arrives_at_the_face {H : Type u} {W : Type v}
    (σ : door H W → W) (d : door H W) : face (exchange σ d) = σ d :=
  rfl

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

theorem the_speaker_rides_unread {H : Type u} {W : Type v}
    (σ : door H W → W) (d : door H W) : met (exchange σ d) = face d :=
  rfl

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

theorem the_listening_turn_is_the_yield {H : Type u} {W : Type v} (d : door H W) :
    exchange met d = turnAbout d :=
  rfl

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

theorem the_two_listeners_restore_the_table {H : Type u} {W : Type v} (d : door H W) :
    exchange met (exchange met d) = d :=
  rfl

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

theorem the_ode_comes_home {H : Type u} {W : Type v} (σ : door H W → W) (d : door H W) :
    exchange met (exchange σ d) = vertical σ d :=
  rfl

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

theorem the_air_gap_wears_the_one_face (I : Type u) (O : Type v) :
    airGap.{u, v, w} I O
      = reseat (appFace (List I) O) (fun m : Machine.{u, v, w} I O => behavior m) :=
  rfl

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

theorem the_park_resumes {I : Type u} {O : Type v} (m : Machine I O) :
    ∀ (u : List I) (s : m.S) (v : List I),
      park m s (u ++ v) = park m (park m s u) v :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _ _)))

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

theorem the_retuned_seat_walks_the_translated_word {I : Type u} {I' : Type u'} {O : Type v}
    (f : I → I') (m : Machine I' O) :
    ∀ (w : List I) (s : m.S), park (retune f m) s w = park m s (w.map f) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _)))

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

theorem the_revoice_moves_no_seat {I : Type u} {O : Type v} {O' : Type v'}
    (g : O → O') (m : Machine I O) :
    ∀ (w : List I) (s : m.S), park (revoice g m) s w = park m s w :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _)))

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

theorem the_intertwined_walks_agree {I : Type u} {O : Type v} (m n : Machine I O)
    (h : m.S → n.S) (hstep : ∀ s i, n.step (h s) i = h (m.step s i)) :
    ∀ (w : List I) (s : m.S), park n (h s) w = h (park m s w) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; (try dsimp only [Machine, park] at *); (rw [hstep]; exact ih _))))

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

theorem the_pace_wears_the_tallys_voice : paceOne = revoice oddNat tally :=
  rfl

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

theorem any_two_readings_agree {A : Type u} (op : A → A → A) (base : A) (h : Plan → A)
    (hg : h .ground = base) (hb : ∀ p q, h (.board p q) = op (h p) (h q)) :
    ∀ p, h p = fold op base p :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; assumption)
          |
            (rename_i ih₁ ih₂; intros;
              (dsimp only [fold, Plan]; exact (by (apply hb <;> fail) : _ = _).trans (congr (congrArg _ ih₁) ih₂)))))

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

theorem the_revision_is_a_reading (base : Plan) : graft base = fold .board base :=
  rfl

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

theorem the_trivial_revision_changes_nothing (t : Plan) : graft t .ground = t :=
  rfl

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

theorem the_parent_folds_into_the_ground {A : Type u} (op : A → A → A) (base : A) (t : Plan) :
    ∀ δ, fold op (fold op base t) δ = fold op base (graft t δ) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih₁ ih₂; intros; (dsimp only [graft, fold, Plan]; exact congr (congrArg _ ih₁) ih₂))))

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

theorem the_type_is_a_reading (W : Type u) (p : Plan) :
    build W p = fold (fun A B : Type u => door A B) W p :=
  rfl

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

theorem the_customs_keep_the_still_world {W : Type u} :
    ∀ (p : Plan) (x : build W p), reground (fun w => w) p x = x :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih₁ ih₂; intros; exact congr (congrArg _ (ih₁ _)) (ih₂ _))))

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

theorem the_customs_stack_forward {W : Type u} {W' : Type v} {W'' : Type w}
    (f : W → W') (g : W' → W'') :
    ∀ (p : Plan) (x : build W p),
      reground g p (reground f p x) = reground (fun w => g (f w)) p x :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih₁ ih₂; intros; exact congr (congrArg _ (ih₁ _)) (ih₂ _))))

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

theorem the_census_checksums_with_the_polygon_cutters :
    census 1 = 1 ∧ census 2 = 1 ∧ census 3 = 2 ∧ census 4 = 5
      ∧ census 5 = 14 :=
  by decide

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

theorem the_repeated_ask_hears_one_answer (F : Face) (s : F.State) (p : F.Probe) :
    ∀ n : Nat,
      sound F s (recite (List.replicate n p)) = List.replicate n (F.obs s p) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact congrArg _ ih)))

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

theorem the_muffled_tally_is_the_resting_counter :
    revoice (fun _ => true) tally = restingCounter :=
  rfl

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

theorem the_self_steered_machine_is_a_clock {I : Type u} {O : Type v}
    (m : Machine I O) (r : m.S → I) :
    ∀ (w : List Unit) (s : m.S),
      drive (selfSteered m r) s w = m.out (orbit m r s w.length) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _)))

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

theorem the_instinct_replays_its_word {I : Type u} {O : Type v}
    (m : Machine I O) (r : m.S → I) :
    ∀ (w : List Unit) (s : m.S),
      drive (selfSteered m r) s w = drive m s (selfWord m r s w.length) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _)))

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

theorem the_lift_peeks_the_out {I : Type u} {O : Type v} (m : Machine I O) (s : m.S) :
    peek (liftFrom m s) = m.out s :=
  rfl

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

theorem the_lift_feeds_the_step {I : Type u} {O : Type v} (m : Machine I O)
    (s : m.S) (i : I) :
    feed (liftFrom m s) i = liftFrom m (m.step s i) :=
  rfl

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

theorem the_unit_machine_steers_itself {O : Type v} (m : Machine Unit O) :
    selfSteered m (fun _ => ()) = m :=
  rfl

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

theorem the_comparison_mints_a_face (F G : Face) {S : Type u'}
    (f : S → F.State) (g : S → G.State) {X : Type w'}
    (c : F.Ans → G.Ans → X) (s : S) (p : F.Probe) (q : G.Probe) :
    c (F.obs (f s) p) (G.obs (g s) q)
      = walkIn c ((pairFace F G f g).obs s (atTheDoor p q)) :=
  rfl

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

theorem the_concord_reads_both_models (F : Face) {V : Type v'}
    (x : door F.State V) (p : F.Probe) :
    (concordFace F V).obs x (atTheDoor p ()) = atTheDoor (F.obs (face x) p) (met x) :=
  rfl

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

theorem the_interview_crosses_the_seat (F : Face) {S' : Type u'} (h : S' → F.State) (s : S') :
    ∀ q, sound F (h s) q = sound (reseat F h) s q :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact congrArg _ (ih _))))

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

theorem no_interview_parts_the_origin {S' : Type u'} (s t : S') :
    ∀ q, sound (originFace S') s q = sound (originFace S') t q :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact congrArg _ (ih _))))

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

theorem the_record_writes_where_the_face_is_blind (F : Face.{u, v, w}) {W : Type v'}
    (keep : door F.State W → W) :
    unheard (host F W) (fun x => atTheDoor (face x) (keep x)) :=
  fun _ _ => rfl

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

theorem the_sounding_reads_the_alike (F : Face) {s t : F.State}
    (h : ∀ q, sound F s q = sound F t q) : alike F s t :=
  fun p =>
    the_first_mark_reads
      (show F.obs s p :: [] = F.obs t p :: [] from h (.ask p fun _ => .rest))

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

theorem the_guests_reboard_in_order {W : Type u} (w0 : W) :
    ∀ (p : Plan) (x : build W p) (t : List W),
      reboardAux w0 p (pour p x ++ t) = (x, t)
  | .ground, x, t => rfl
  | .board p q, d, t => by
      show (atTheDoor (reboardAux w0 p ((pour p (face d) ++ pour q (met d)) ++ t)).1
              (reboardAux w0 q (reboardAux w0 p ((pour p (face d) ++ pour q (met d)) ++ t)).2).1,
            (reboardAux w0 q (reboardAux w0 p ((pour p (face d) ++ pour q (met d)) ++ t)).2).2)
          = (d, t)
      rw [the_appends_regroup (pour p (face d)) (pour q (met d)) t]
      rw [the_guests_reboard_in_order w0 p (face d) (pour q (met d) ++ t)]
      show (atTheDoor (face d) (reboardAux w0 q (pour q (met d) ++ t)).1,
            (reboardAux w0 q (pour q (met d) ++ t)).2) = (d, t)
      rw [the_guests_reboard_in_order w0 q (met d) t]
      exact rfl

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

theorem mem_cross_split :
    ∀ (ps : List Plan) {qs : List Plan} {x : Plan},
      x ∈ cross ps qs → ∃ l r, x = Plan.board l r ∧ l ∈ ps ∧ r ∈ qs
  | [], _, _, h => nomatch h
  | p :: ps, qs, _, h =>
      match mem_append_split (qs.map (Plan.board p)) h with
      | Or.inl hm =>
          match mem_map_back qs hm with
          | ⟨r, hr, he⟩ => ⟨p, r, he.symm, List.Mem.head _, hr⟩
      | Or.inr hc =>
          match mem_cross_split ps hc with
          | ⟨l, r, he, hl, hr⟩ => ⟨l, r, he, List.Mem.tail _ hl, hr⟩

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

theorem mem_cross {qs : List Plan} {r : Plan} (hr : r ∈ qs) :
    ∀ {ps : List Plan} {l : Plan}, l ∈ ps → Plan.board l r ∈ cross ps qs
  | _ :: ps, _, List.Mem.head _ =>
      mem_append_left (cross ps qs) (mem_map_intro (Plan.board _) hr)
  | p :: _, _, List.Mem.tail _ h =>
      mem_append_right (qs.map (Plan.board p)) (mem_cross hr h)

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

theorem the_ledger_parks_the_word {I : Type u} :
    ∀ (ws rec : List I), park (ledger I) rec ws = rec ++ ws :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; (apply ((Room.the_append_rests _)).symm <;> fail))
          | (rename_i ih; intros; exact (ih _).trans (by (apply Room.the_appends_regroup <;> fail)))))

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

theorem the_round_trips_come_home {O : Type v} (f : sheet Unit O) (g : stream O)
    (w : List Unit) (n : Nat) :
    toSheet (toStream f) w = f w ∧ toStream (toSheet g) n = g n :=
  ⟨congrArg f (the_unit_word_is_its_count w),
   congrArg g (len_replicate () n)⟩

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

theorem the_manifest_is_natural {W : Type u} {W' : Type v} (f : W → W') :
    ∀ (p : Plan) (x : build W p), pour p (reground f p x) = (pour p x).map f :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          |
            (rename_i ih₁ ih₂; intros;
              exact
                (congr (congrArg _ (ih₁ _)) (ih₂ _)).trans (by (apply ((Room.map_crosses_append _ _ _)).symm <;> fail)))))

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

theorem the_held_scale_rides (c : Nat) :
    ∀ p : Plan, fold (fun a b => a + b) c p = c * reading p
  | .ground => (mul_one_reads c).symm
  | .board a b =>
      ((congr (congrArg (fun x y => x + y) (the_held_scale_rides c a))
          (the_held_scale_rides c b) :
          fold (fun x y => x + y) c a + fold (fun x y => x + y) c b
            = c * reading a + c * reading b)).trans
        (mul_spreads c (reading a) (reading b)).symm

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

theorem the_reading_is_positive :
    ∀ p : Plan, ∃ m : Nat, reading p = m + 1
  | .ground => ⟨0, rfl⟩
  | .board l r =>
      match the_reading_is_positive l with
      | ⟨a, ha⟩ =>
          ⟨a + reading r, by
            show reading l + reading r = (a + reading r) + 1
            rw [ha, succ_adds]⟩

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

theorem the_manifest_counts {W : Type u} :
    ∀ (p : Plan) (x : build W p), (pour p x).length = reading p :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          |
            (rename_i ih₁ ih₂; intros; (try dsimp only [build, pour, reading, Plan] at *);
              (rw [Room.lengths_add]; exact congr (congrArg _ (ih₁ _)) (ih₂ _)))))

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

theorem the_tally_parks_at_its_count :
    ∀ (w : List Unit) (s : Nat), park tally s w = s + w.length :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact (ih _).trans (by (apply Room.succ_adds <;> fail)))))

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

theorem a_wider_seat_reads_the_remainder (F : Face) {W : Type v'}
    (s : F.State) {w w' : W} (hw : w ≠ w') :
    ¬ alike (widen F W) (atTheDoor s w) (atTheDoor s w') :=
  fun h => hw (((the_widening_is_exact F (atTheDoor s w) (atTheDoor s w')).mp h).2)

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

theorem no_interview_hears_the_unheard (F : Face) (m : F.State → F.State)
    (h : unheard F m) : ∀ s q, sound F (m s) q = sound F s q :=
  by (intros; (apply no_interview_parts_the_alike <;> (apply h <;> fail)))

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

theorem the_intertwiner_carries_the_walk {I : Type u} {O : Type v} (m n : Machine I O)
    (h : m.S → n.S) (hstep : ∀ s i, n.step (h s) i = h (m.step s i))
    (hout : ∀ s, n.out (h s) = m.out s) :
    carries (fun s w => drive m s w) (fun s w => drive n s w) h :=
  fun s w =>
    (congrArg n.out (the_intertwined_walks_agree m n h hstep w s)).trans
      (hout (park m s w))

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

theorem a_stage_may_ground_a_stage (W : Type u) (t δ : Plan) :
    build W (graft t δ) = build (build W t) δ :=
  by (intros; (apply ((the_parent_folds_into_the_ground _ _ _ _)).symm <;> fail))

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

theorem the_hold_walks_beside_the_work {I : Type u} {O : Type v}
    (m : Machine I O) (w : List I) (s : m.S) (held : List I) :
    drive (buffered m) (s, held) w = drive m (park m s held) w :=
  (congrArg m.out
    (the_intertwined_walks_agree (buffered m) m
      (fun st => park m st.1 st.2)
      (fun st i => (the_park_resumes m st.2 st.1 [i]).symm)
      w (s, held))).symm

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

theorem the_replay_is_the_machine {I : Type u} {O : Type v} (m : Machine I O)
    (w : List I) :
    behavior (replayer m) w = behavior m w :=
  (congrArg m.out
    (the_intertwined_walks_agree (replayer m) m
      (fun rec => park m m.s0 rec)
      (fun rec i => (the_park_resumes m rec m.s0 [i]).symm)
      w [])).symm

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

theorem no_move_at_the_mirror :
    ∀ {q : Plan}, ¬ reassoc (.board .ground .ground) q := by
  intro q h
  cases h with
  | left r h' => exact no_move_at_the_ground h'
  | right r h' => exact no_move_at_the_ground h'

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

theorem the_clocks_lift_is_a_stream {O : Type v} (m : Machine Unit O) (n : Nat) :
    streamOf m n = toStream (liftFrom m m.s0) n :=
  ((congrArg (fun k => m.out (orbit m (fun _ => ()) m.s0 k))
      (len_replicate () n)).symm).trans
    ((the_self_steered_machine_is_a_clock m (fun _ => ())
        (List.replicate n ()) m.s0).symm)

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

theorem every_widening_is_one_pairing (F G H : Face) {S : Type u'}
    (f : S → F.State) (g : S → G.State) (h : S → H.State)
    (p0 : F.Probe) (q0 : G.Probe) (r0 : H.Probe) (s t : S) :
    alike (pairFace (pairFace F G f g) H (fun x => x) h) s t
      ↔ alike (pairFace F (pairFace G H g h) f (fun x => x)) s t :=
  (the_pairing_is_exact (pairFace F G f g) H (fun x => x) h
      (atTheDoor p0 q0) r0 s t).trans
    ((and_congr_first (the_pairing_is_exact F G f g p0 q0 s t)).trans
      (and_regroups.trans
        ((and_congr_second (the_pairing_is_exact G H g h q0 r0 s t)).symm.trans
          (the_pairing_is_exact F (pairFace G H g h) f (fun x => x)
            p0 (atTheDoor q0 r0) s t).symm)))

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

theorem the_meeting_mints_the_concord (F : Face) {V : Type v'}
    (agree : F.Ans → V → Prop) (p : F.Probe) :
    Derived (concordFace F V)
      (fun x => agree (face ((concordFace F V).obs x (atTheDoor p ())))
        (met ((concordFace F V).obs x (atTheDoor p ())))) :=
  a_role_read_at_a_probe_is_derived (concordFace F V) (atTheDoor p ())
    (fun a => agree (face a) (met a))

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

theorem an_audition_hears_only_the_conduct {I : Type u} {O : Type v} (m n : Machine I O)
    (h : ∀ w, behavior m w = behavior n w) :
    ∀ q, sound (airGap I O) m q = sound (airGap I O) n q :=
  by (intros; (apply no_interview_parts_the_alike <;> assumption))

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

theorem lineages_compose (t d1 d2 : Plan) :
    graft (graft t d1) d2 = graft t (graft d1 d2) :=
  by (intros; (apply the_parent_folds_into_the_ground <;> fail))

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

theorem the_manifest_rebuilds_the_carrier {W : Type u} (w0 : W) (p : Plan) (x : build W p) :
    reboard w0 p (pour p x) = x :=
  congrArg Prod.fst
    ((congrArg (reboardAux w0 p) (the_append_rests (pour p x)).symm).trans
      (the_guests_reboard_in_order w0 p x []))

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

theorem the_cross_keeps_apart {qs : List Plan} (hqs : Apart qs) :
    ∀ {ps : List Plan}, Apart ps → Apart (cross ps qs)
  | [], _ => Apart.nil
  | _ :: ps, Apart.cons hp hps =>
      apart_append (cross ps qs)
        (apart_map (fun _ _ h => (Plan.board.inj h).2) hqs)
        (the_cross_keeps_apart hqs hps)
        (fun _ hx _ hy he =>
          match mem_map_back qs hx, mem_cross_split ps hy with
          | ⟨_, _, hfr⟩, ⟨l', _, hy_eq, hl', _⟩ =>
              hp l' hl'
                (Plan.board.inj ((hfr.trans he).trans hy_eq)).1)

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

theorem every_seat_is_a_reading_of_the_record {I : Type u} {O : Type v}
    (m : Machine I O) (rec ws : List I) :
    park m m.s0 (park (ledger I) rec ws) = park m (park m m.s0 rec) ws :=
  (congrArg (park m m.s0) (the_ledger_parks_the_word ws rec)).trans
    (the_park_resumes m rec m.s0 ws)

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

theorem the_curtain_is_exact (F : Face) (s t : F.State) :
    alike F s t ↔ ∀ q, sound F s q = sound F t q :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply no_interview_parts_the_alike <;> assumption)
          | (apply the_sounding_reads_the_alike <;> assumption)))

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

theorem the_audition_is_exact {I : Type u} {O : Type v} (m n : Machine I O) :
    alike (airGap I O) m n ↔ ∀ q, sound (airGap I O) m q = sound (airGap I O) n q :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply no_interview_parts_the_alike <;> assumption)
          | (apply the_sounding_reads_the_alike <;> assumption)))

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

theorem the_revision_multiplies_the_reading (t δ : Plan) :
    reading (graft t δ) = reading t * reading δ :=
  (the_parent_folds_into_the_ground (fun a b => a + b) 1 t δ).symm.trans
    (the_held_scale_rides (reading t) δ)

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

theorem the_horizon_holds_every_reading :
    ∀ (n : Nat) (p : Plan),
      Nat.ble (reading p) (n + 1) = true → p ∈ allPlans n
  | 0, .ground, _ => List.Mem.head _
  | _ + 1, .ground, _ => List.Mem.head _
  | 0, .board l r, h =>
      match the_reading_is_positive l, the_reading_is_positive r with
      | ⟨a, ha⟩, ⟨b, hb⟩ => by
          have e : (a + 1) + (b + 1) = ((a + b) + 1) + 1 :=
            congrArg (· + 1) (succ_adds a b)
          have h0 : Nat.ble (reading l + reading r) 1 = true := h
          rw [ha, hb, e] at h0
          exact nomatch h0
  | n + 1, .board l r, h =>
      match the_reading_is_positive l, the_reading_is_positive r with
      | ⟨a, ha⟩, ⟨b, hb⟩ =>
          have e : (a + 1) + (b + 1) = ((a + b) + 1) + 1 :=
            congrArg (· + 1) (succ_adds a b)
          have h' : Nat.ble ((a + b) + 1) (n + 1) = true := by
            have h0 : Nat.ble (reading l + reading r) ((n + 1) + 1) = true := h
            rw [ha, hb, e] at h0
            exact h0
          have hL : l ∈ allPlans n :=
            the_horizon_holds_every_reading n l (by
              rw [ha]
              exact ble_trans (a + 1) ((a + b) + 1) (n + 1)
                (ble_le_add a b) h')
          have hR : r ∈ allPlans n :=
            the_horizon_holds_every_reading n r (by
              rw [hb]
              exact ble_trans (b + 1) ((a + b) + 1) (n + 1)
                (ble_le_add_left a b) h')
          List.Mem.tail _ (mem_cross hR hL)

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

theorem the_muffler_banks_the_run (w : List Unit) (s : Nat) :
    park restingCounter s w = s + w.length :=
  (the_revoice_moves_no_seat (fun _ => true) tally w s).trans
    (the_tally_parks_at_its_count w s)

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

theorem the_wider_voice_releases_the_bank (w : List Unit) :
    behavior tally w = w.length :=
  by
    (intros; (try dsimp only [behavior, tally] at *); intros;
      (apply ((the_tally_parks_at_its_count _ _)).trans (by (apply Room.zero_add <;> fail)) <;> fail))

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

theorem the_rep_lands_where_it_is_fed {I : Type u} {O : Type v}
    (m : Machine I O) (w v : List I) (n : Nat) (s : m.S)
    (u : List Unit) (t : Nat) (r : m.S → I) (vs : List Unit) :
    sound (airGap I O) m (recite (List.replicate n w))
        = List.replicate n (behavior m w)
      ∧ park m s (w ++ v) = park m (park m s w) v
      ∧ park tally (park tally t u) u = (t + u.length) + u.length
      ∧ drive (selfSteered m r) s vs = drive m s (selfWord m r s vs.length) :=
  ⟨the_repeated_ask_hears_one_answer (airGap I O) m w n,
   the_park_resumes m w s v,
   (the_tally_parks_at_its_count u (park tally t u)).trans
     (congrArg (· + u.length) (the_tally_parks_at_its_count u t)),
   the_instinct_replays_its_word m r vs s⟩

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

theorem the_drained_is_on_spec {W : Type u} (w0 : W) (p : Plan) (l : List W) :
    (drain w0 p l).length = reading p :=
  by (intros; (apply the_manifest_counts <;> fail))

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

theorem recording_the_recording_grounds (F : Face.{u, v, w}) {W : Type v'}
    (keep : door F.State W → W) (x : door F.State W) (q : Interview F.Probe F.Ans) :
    sound (host F W) (atTheDoor (face x) (keep x)) q = sound (host F W) x q
      ∧ sound (host F W) (atTheDoor (face x) (keep (atTheDoor (face x) (keep x)))) q
          = sound (host F W) x q :=
  by
    (intros; (repeat' constructor);
      all_goals (intros; (apply no_interview_parts_the_alike <;> (apply the_host_merges_the_guests <;> fail))))

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

theorem the_mutual_recording_is_unheard (F : Face.{u, v, w}) {V : Type v'} {W : Type w'}
    (mine : door F.State (door V W) → V) (yours : door F.State (door V W) → W)
    (x : door F.State (door V W)) (q : Interview F.Probe F.Ans) :
    sound (host F (door V W)) (atTheDoor (face x) (atTheDoor (mine x) (yours x))) q
      = sound (host F (door V W)) x q :=
  by (intros; (apply no_interview_parts_the_alike <;> (apply the_host_merges_the_guests <;> fail)))

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

theorem the_settled_gap_moves_the_model (F : Face) {V : Type v'}
    (fix : door F.State V → V) (x : door F.State V)
    (q : Interview F.Probe F.Ans) (p : F.Probe) :
    sound (host F V) (atTheDoor (face x) (fix x)) q = sound (host F V) x q
      ∧ (concordFace F V).obs (atTheDoor (face x) (fix x)) (atTheDoor p ())
          = atTheDoor (F.obs (face x) p) (fix x) :=
  by
    (intros; (repeat' constructor);
      all_goals (intros; (apply no_interview_parts_the_alike <;> (apply the_host_merges_the_guests <;> fail))))

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

theorem two_seats_record_each_other (F : Face.{u, v, w}) {V : Type v'} {W : Type w'}
    (mine : door F.State (door V W) → V) (yours : door F.State (door V W) → W)
    (x : door F.State (door V W)) (q : Interview F.Probe F.Ans)
    (s : F.State) {v v' : V} (hv : v ≠ v') (w : W) :
    unheard (host F (door V W)) (fun y => atTheDoor (face y) (atTheDoor (mine y) (yours y)))
      ∧ sound (host F (door V W)) (atTheDoor (face x) (atTheDoor (mine x) (yours x))) q
          = sound (host F (door V W)) x q
      ∧ alike (host F (door V W)) (atTheDoor s (atTheDoor v w)) (atTheDoor s (atTheDoor v' w))
      ∧ atTheDoor s (atTheDoor v w) ≠ atTheDoor s (atTheDoor v' w)
      ∧ (widen F (door V W)).obs (atTheDoor s (atTheDoor v w)) (.viaRight ())
          ≠ (widen F (door V W)).obs (atTheDoor s (atTheDoor v' w)) (.viaRight ()) :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply the_record_writes_where_the_face_is_blind <;> fail)
          | (apply no_interview_parts_the_alike <;> (apply the_host_merges_the_guests <;> fail))
          | (apply the_host_merges_the_guests <;> fail)
          | (apply (((the_records_part_the_seats _ _ _ _)).2).1 <;> assumption)
          | (apply (((the_records_part_the_seats _ _ _ _)).2).2 <;> assumption)))

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

theorem the_handshake :
    (∀ (F : Face) (s t : F.State), alike F s t → ∀ q, sound F s q = sound F t q) ∧
    (∀ (F : Face) (W : Type v') (s : F.State) (w w' : W),
      (∀ q, sound (host F W) (atTheDoor s w) q = sound (host F W) (atTheDoor s w') q) ∧
      (w ≠ w' → ¬ alike (widen F W) (atTheDoor s w) (atTheDoor s w'))) :=
  ⟨fun F _ _ h => no_interview_parts_the_alike F h,
   fun F W s w w' =>
    ⟨no_interview_parts_the_alike (host F W) (the_host_merges_the_guests F W s w w'),
     fun hw => a_wider_seat_reads_the_remainder F s hw⟩⟩

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

theorem only_the_unheard_survives_the_sounding (F : Face) (m : F.State → F.State) :
    unheard F m ↔ ∀ s q, sound F (m s) q = sound F s q :=
  ⟨no_interview_hears_the_unheard F m,
   fun h s => the_sounding_reads_the_alike F (h s)⟩

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

theorem correct_maintenance_has_no_signature (F : Face) (m n : F.State → F.State)
    (hm : unheard F m) (hn : unheard F n) :
    ∀ s q, sound F (m s) q = sound F (n s) q :=
  fun s q => (no_interview_hears_the_unheard F m hm s q).trans
    (no_interview_hears_the_unheard F n hn s q).symm

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

theorem the_pace_is_carried_onto_the_flip :
    carries (fun s w => drive paceOne s w) (fun s w => drive flip s w) oddNat :=
  the_intertwiner_carries_the_walk paceOne flip oddNat (fun _ _ => rfl) (fun _ => rfl)

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

theorem the_flywheel_and_the_shell_sound_alike (q : Interview (List Unit) Bool) :
    sound (airGap Unit Bool) restingCounter q = sound (airGap Unit Bool) hollowShell q :=
  an_audition_hears_only_the_conduct restingCounter hollowShell (fun _ => rfl) q

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

theorem the_settle_is_unheard {I : Type u} {O : Type v} (m : Machine I O)
    (st : m.S × List I) (w : List I) :
    drive (buffered m) (settleHeld m st) w = drive (buffered m) st w :=
  (the_hold_walks_beside_the_work m w (park m st.1 st.2) []).trans
    (the_hold_walks_beside_the_work m w st.1 st.2).symm

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

theorem no_move_past_the_right_comb :
    ∀ {q : Plan}, ¬ reassoc (.board .ground (.board .ground .ground)) q := by
  intro q h
  cases h with
  | left r h' => exact no_move_at_the_ground h'
  | right r h' => exact no_move_at_the_mirror h'

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

theorem the_left_comb_moves_once :
    ∀ {q : Plan}, reassoc (.board (.board .ground .ground) .ground) q
      → q = .board .ground (.board .ground .ground) := by
  intro q h
  cases h with
  | here a b c => rfl
  | left r h' => exact absurd h' no_move_at_the_mirror
  | right r h' => exact absurd h' no_move_at_the_ground

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

theorem the_buffer_is_invisible {I : Type u} {O : Type v} (m : Machine I O)
    (w : List I) :
    behavior (buffered m) w = behavior m w :=
  by (intros; (apply the_hold_walks_beside_the_work <;> fail))

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

theorem the_drain_settles {W : Type u} (w0 : W) (p : Plan) (l : List W) :
    drain w0 p (drain w0 p l) = drain w0 p l :=
  congrArg (pour p) (the_manifest_rebuilds_the_carrier w0 p (reboard w0 p l))

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

theorem the_room_repeats_no_plan : ∀ d : Nat, Apart (allPlans d)
  | 0 => Apart.cons (fun _ hb => nomatch hb) Apart.nil
  | d + 1 =>
      Apart.cons
        (fun _ hb =>
          match mem_cross_split (allPlans d) hb with
          | ⟨_, _, he, _, _⟩ => fun hg => nomatch hg.trans he)
        (the_cross_keeps_apart (the_room_repeats_no_plan d)
          (the_room_repeats_no_plan d))

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

theorem the_lift_is_the_conduct {I : Type u} {O : Type v} (m n : Machine I O)
    (f g : sheet I O) :
    (∀ s, peek (liftFrom m s) = m.out s)
      ∧ (∀ s i, feed (liftFrom m s) i = liftFrom m (m.step s i))
      ∧ (∀ (h : m.S → sheet I O),
          (∀ s, peek (h s) = m.out s) →
          (∀ s i, feed (h s) i = h (m.step s i)) →
          ∀ (w : List I) (s : m.S), h s w = liftFrom m s w)
      ∧ liftFrom m m.s0 = behavior m
      ∧ (alike (airGap I O) m n ↔ ∀ q, sound (airGap I O) m q = sound (airGap I O) n q)
      ∧ (alike (appFace (List I) O) f g ↔ ∀ w, f w = g w) :=
  ⟨fun _ => rfl,
   fun _ _ => rfl,
   fun h hp hf => the_lift_is_unique m h ⟨hp, hf⟩,
   rfl,
   the_audition_is_exact m n,
   the_pointwise_license (List I) O f g⟩

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

theorem the_tallys_stream_counts (n : Nat) :
    streamOf tally n = n :=
  (the_clocks_lift_is_a_stream tally n).trans
    ((the_wider_voice_releases_the_bank (List.replicate n ())).trans
      (len_replicate () n))

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

theorem the_concord_is_the_meetings_own (F : Face) {V : Type v'}
    (agree : F.Ans → V → Prop) (beq : F.Ans → V → Bool) (p : F.Probe)
    (s : F.State) {v v' : V} (hv : v ≠ v')
    (fix : door F.State V → V) (x : door F.State V)
    (q : Interview F.Probe F.Ans) (ps : List F.Probe) :
    Derived (concordFace F V)
        (fun y => agree (face ((concordFace F V).obs y (atTheDoor p ())))
          (met ((concordFace F V).obs y (atTheDoor p ()))))
      ∧ alike (host F V) (atTheDoor s v) (atTheDoor s v')
      ∧ ¬ alike (concordFace F V) (atTheDoor s v) (atTheDoor s v')
      ∧ ((∀ r, r ∈ ps → beq (F.obs (face x) r) (met x) = true)
          ∨ ∃ r, r ∈ ps ∧ beq (F.obs (face x) r) (met x) = false)
      ∧ sound (host F V) (atTheDoor (face x) (fix x)) q = sound (host F V) x q
      ∧ (concordFace F V).obs (atTheDoor (face x) (fix x)) (atTheDoor p ())
          = atTheDoor (F.obs (face x) p) (fix x) :=
  ⟨the_meeting_mints_the_concord F agree p,
   (no_seat_reads_the_concord_alone F p s hv).1,
   (no_seat_reads_the_concord_alone F p s hv).2,
   the_concord_agrees_or_names_the_gap F beq x ps,
   (the_settled_gap_moves_the_model F fix x q p).1,
   (the_settled_gap_moves_the_model F fix x q p).2⟩

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

theorem the_right_comb_rests :
    ∀ {n : Nat} {q : Plan},
      chain n (.board .ground (.board .ground .ground)) q
        → q = .board .ground (.board .ground .ground) := by
  intro n q h
  cases h with
  | rest => rfl
  | step h1 h2 => exact absurd h1 no_move_past_the_right_comb

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

theorem the_right_loop_reads_zero :
    ∀ {k : Nat}, chain k (.board .ground (.board .ground .ground))
        (.board .ground (.board .ground .ground)) → k = 0 := by
  intro k h
  cases h with
  | rest => rfl
  | step h1 h2 => exact absurd h1 no_move_past_the_right_comb

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

theorem the_census_is_exact (k : Nat) :
    Apart ((allPlans k).filter (fun p => Nat.beq (reading p) (k + 1)))
      ∧ ∀ p : Plan,
          p ∈ (allPlans k).filter (fun p => Nat.beq (reading p) (k + 1))
            ↔ reading p = k + 1 :=
  ⟨apart_filter (the_room_repeats_no_plan k),
   fun p =>
     ⟨fun h =>
        have hq :=
          filter_holds (A := Plan)
            (q := fun p => Nat.beq (reading p) (k + 1))
            (x := p) (allPlans k) h
        eq_of_beq _ _ hq,
      fun h =>
        mem_filter_intro (allPlans k)
          (the_horizon_holds_every_reading k p
            (by rw [h]; exact ble_refl (k + 1)))
          (by rw [h]; exact beq_self (k + 1))⟩⟩

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

theorem the_clock_is_a_room {I : Type u} {O : Type v}
    (m : Machine I O) (r : m.S → I) (w : List Unit) (s : m.S)
    (st : m.S × List I) (v : List I) (u : List Unit) :
    drive (selfSteered m r) s w = m.out (orbit m r s w.length)
      ∧ selfSteered tally (fun _ => ()) = tally
      ∧ orbit tally (fun _ => ()) (0 : Nat) u.length = u.length
      ∧ (∀ b : Bool, park flip b [(), ()] = b)
      ∧ drive (buffered m) (settleHeld m st) v = drive (buffered m) st v
      ∧ behavior tally u = u.length :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply the_self_steered_machine_is_a_clock <;> fail)
          | (apply the_tallys_stream_counts <;> fail)
          | (apply Room.not_not <;> fail)
          | (apply the_settle_is_unheard <;> fail)
          | (apply the_wider_voice_releases_the_bank <;> fail)))

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

theorem room_margin_flywheel_door {I : Type u} {O : Type v} {A : Type w}
    (m : Machine I O) (r : m.S → I) (u : List Unit) (s : m.S)
    (st : m.S × List I) (v : List I) (q : Interview (List Unit) Bool)
    (beq : A → A → Bool) (hrefl : ∀ y : A, beq y y = true)
    (x : A) (st' : List A × List (A × List A)) (word : List (A × List A))
    (hall needs : List A)
    (F : Face) {W : Type v'} (g : F.State) {w1 w2 : W} (hw : w1 ≠ w2) :
    drive (selfSteered m r) s u = m.out (orbit m r s u.length)
      ∧ drive (buffered m) (settleHeld m st) v = drive (buffered m) st v
      ∧ sound (airGap Unit Bool) restingCounter q = sound (airGap Unit Bool) hollowShell q
      ∧ (∀ tw : List Unit, behavior tally tw = tw.length)
      ∧ (enrolled beq st'.1 x = false →
          (∀ arr, arr ∈ word → beq arr.1 x = true → x ∈ arr.2) →
          enrolled beq (intake beq st' word).1 x = false)
      ∧ (lacking beq hall needs = 1 →
          ∃ k, k ∈ needs ∧ enrolled beq hall k = false ∧
            backed beq (k :: hall) needs = true)
      ∧ ¬ alike (widen F W) (atTheDoor g w1) (atTheDoor g w2) :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply the_self_steered_machine_is_a_clock <;> fail)
          | (apply the_settle_is_unheard <;> fail)
          | (apply the_flywheel_and_the_shell_sound_alike <;> fail)
          | (apply the_wider_voice_releases_the_bank <;> fail)
          | (apply Room.no_mark_lights_itself <;> assumption)
          | (apply Room.the_key_is_cut_from_the_room <;> assumption)
          | (apply a_wider_seat_reads_the_remainder <;> assumption)))

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

theorem the_clock_writes_its_sequence {O : Type v} (m m' : Machine Unit O)
    (f : sheet Unit O) (g : stream O) (w : List Unit) (n : Nat) :
    streamOf m n = toStream (liftFrom m m.s0) n
      ∧ toSheet (toStream f) w = f w
      ∧ toStream (toSheet g) n = g n
      ∧ streamOf tally n = n
      ∧ (alike (airGap Unit O) m m' ↔
          ∀ q, sound (airGap Unit O) m q = sound (airGap Unit O) m' q) :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply the_clocks_lift_is_a_stream <;> fail)
          | (apply ((the_round_trips_come_home _ _ _ _)).1 <;> assumption)
          | (apply ((the_round_trips_come_home _ _ _ _)).2 <;> assumption)
          | (apply the_tallys_stream_counts <;> fail)
          | (apply an_audition_hears_only_the_conduct <;> assumption)
          | (apply the_sounding_reads_the_alike <;> assumption)))

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

theorem the_left_loop_reads_zero :
    ∀ {k : Nat}, chain k (.board (.board .ground .ground) .ground)
        (.board (.board .ground .ground) .ground) → k = 0 := by
  intro k h
  cases h with
  | rest => rfl
  | @step m p q r h1 h2 =>
    have he : q = .board .ground (.board .ground .ground) :=
      the_left_comb_moves_once h1
    have h2' : chain m (.board .ground (.board .ground .ground))
        (.board (.board .ground .ground) .ground) := he ▸ h2
    exact nomatch (Plan.board.inj (the_right_comb_rests h2').symm).1

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

theorem three_has_no_loop (n : Nat) :
    ¬ chain (n + 1) (.board (.board .ground .ground) .ground)
        (.board (.board .ground .ground) .ground)
      ∧ ¬ chain (n + 1) (.board .ground (.board .ground .ground))
          (.board .ground (.board .ground .ground)) :=
  ⟨(fun h => nomatch (the_left_loop_reads_zero h)),
   (fun h => nomatch (the_right_loop_reads_zero h))⟩

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

theorem entanglement_is_the_loop (n : Nat) :
    (reassoc (.board (.board .ground .ground) .ground)
        (.board .ground (.board .ground .ground))
      ∧ census 3 = 2)
      ∧ (¬ chain (n + 1) (.board (.board .ground .ground) .ground)
            (.board (.board .ground .ground) .ground))
      ∧ chain 2 (.board (.board (.board .ground .ground) .ground) .ground)
          (.board .ground (.board .ground (.board .ground .ground)))
      ∧ chain 3 (.board (.board (.board .ground .ground) .ground) .ground)
          (.board .ground (.board .ground (.board .ground .ground)))
      ∧ (2 : Nat) ≠ 3
      ∧ reading (.board (.board (.board .ground .ground) .ground) .ground)
          = reading (.board .ground (.board .ground (.board .ground .ground)))
      ∧ census 4 = 5 :=
  ⟨⟨the_two_shapes_of_three.1, the_two_shapes_of_three.2.2.2⟩,
   (three_has_no_loop n).1,
   the_pentagon_turns_at_four.1,
   the_pentagon_turns_at_four.2,
   (fun h => nomatch (Nat.succ.inj (Nat.succ.inj h))),
   rfl,
   rfl⟩

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

theorem three_is_the_width_of_contact (F G H : Face) {S : Type u'}
    (f : S → F.State) (g : S → G.State) (h : S → H.State)
    (p0 : F.Probe) (q0 : G.Probe) (r0 : H.Probe) (s t : S)
    {T : Type u''} (r : T → Bool) (a b c : T) (n : Nat) :
    (r a = r b ∨ r b = r c ∨ r a = r c)
      ∧ (alike (pairFace F G f g) s t ↔ (alike F (f s) (f t) ∧ alike G (g s) (g t)))
      ∧ (alike (pairFace (pairFace F G f g) H (fun x => x) h) s t
          ↔ alike (pairFace F (pairFace G H g h) f (fun x => x)) s t)
      ∧ ¬ chain (n + 1) (.board (.board .ground .ground) .ground)
          (.board (.board .ground .ground) .ground)
      ∧ chain 2 (.board (.board (.board .ground .ground) .ground) .ground)
          (.board .ground (.board .ground (.board .ground .ground)))
      ∧ chain 3 (.board (.board (.board .ground .ground) .ground) .ground)
          (.board .ground (.board .ground (.board .ground .ground))) :=
  ⟨the_hallway_is_too_small r a b c,
   the_pairing_is_exact F G f g p0 q0 s t,
   every_widening_is_one_pairing F G H f g h p0 q0 r0 s t,
   (three_has_no_loop n).1,
   the_pentagon_turns_at_four.1,
   the_pentagon_turns_at_four.2⟩

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

end Face

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 Face["Face"]
    a_guest_blind_reading_is_a_face_reading["a_guest_blind_reading_is_a_face_reading"]
    a_guest_mover_is_unheard["a_guest_mover_is_unheard"]
    a_role_read_at_a_probe_is_derived["a_role_read_at_a_probe_is_derived"]
    a_stage_may_ground_a_stage["a_stage_may_ground_a_stage"]
    a_wider_seat_reads_the_remainder["a_wider_seat_reads_the_remainder"]
    an_audition_hears_only_the_conduct["an_audition_hears_only_the_conduct"]
    any_ready_greeter_is_the_greeter["any_ready_greeter_is_the_greeter"]
    any_two_readings_agree["any_two_readings_agree"]
    correct_maintenance_has_no_signature["correct_maintenance_has_no_signature"]
    entanglement_is_the_loop["entanglement_is_the_loop"]
    every_door_reading_is_a_face["every_door_reading_is_a_face"]
    every_seat_is_a_reading_of_the_record["every_seat_is_a_reading_of_the_record"]
    every_widening_is_one_pairing["every_widening_is_one_pairing"]
    hosting_associates["hosting_associates"]
    hosting_associates_back["hosting_associates_back"]
    lineages_compose["lineages_compose"]
    mem_cross["mem_cross"]
    mem_cross_split["mem_cross_split"]
    no_face_reads_the_guest["no_face_reads_the_guest"]
    no_interview_hears_the_unheard["no_interview_hears_the_unheard"]
    no_interview_parts_the_alike["no_interview_parts_the_alike"]
    no_interview_parts_the_origin["no_interview_parts_the_origin"]
    no_move_at_the_ground["no_move_at_the_ground"]
    no_move_at_the_mirror["no_move_at_the_mirror"]
    no_move_past_the_right_comb["no_move_past_the_right_comb"]
    no_seat_reads_the_concord_alone["no_seat_reads_the_concord_alone"]
    one_face_many_seats["one_face_many_seats"]
    only_the_unheard_survives_the_sounding["only_the_unheard_survives_the_sounding"]
    recording_the_recording_grounds["recording_the_recording_grounds"]
    room_margin_flywheel_door["room_margin_flywheel_door"]
    the_agreed_window_sounds_as_one["the_agreed_window_sounds_as_one"]
    the_air_gap_wears_the_one_face["the_air_gap_wears_the_one_face"]
    the_audition_is_exact["the_audition_is_exact"]
    the_branches_come_home["the_branches_come_home"]
    the_buffer_is_invisible["the_buffer_is_invisible"]
    the_carrier_was_a_seating["the_carrier_was_a_seating"]
    the_census_checksums_with_the_polygon_cutters["the_census_checksums_with_the_polygon_cutters"]
    the_census_is_exact["the_census_is_exact"]
    the_clock_is_a_room["the_clock_is_a_room"]
    the_clock_writes_its_sequence["the_clock_writes_its_sequence"]
    the_clocks_lift_is_a_stream["the_clocks_lift_is_a_stream"]
    the_comparison_mints_a_face["the_comparison_mints_a_face"]
    the_concord_agrees_or_names_the_gap["the_concord_agrees_or_names_the_gap"]
    the_concord_is_the_meetings_own["the_concord_is_the_meetings_own"]
    the_concord_reads_both_models["the_concord_reads_both_models"]
    the_cross_keeps_apart["the_cross_keeps_apart"]
    the_crossing_returns["the_crossing_returns"]
    the_curtain_is_exact["the_curtain_is_exact"]
    the_customs_keep_the_still_world["the_customs_keep_the_still_world"]
    the_customs_stack_forward["the_customs_stack_forward"]
    the_deferral_is_free["the_deferral_is_free"]
    the_drain_settles["the_drain_settles"]
    the_drained_is_on_spec["the_drained_is_on_spec"]
    the_ear_and_the_voice_commute["the_ear_and_the_voice_commute"]
    the_ear_crosses_the_seat["the_ear_crosses_the_seat"]
    the_face_was_a_held_door["the_face_was_a_held_door"]
    the_flywheel_and_the_shell_sound_alike["the_flywheel_and_the_shell_sound_alike"]
    the_gap_is_minted_at_the_meeting["the_gap_is_minted_at_the_meeting"]
    the_guest_is_real["the_guest_is_real"]
    the_guests_reboard_in_order["the_guests_reboard_in_order"]
    the_handshake["the_handshake"]
    the_held_scale_rides["the_held_scale_rides"]
    the_hold_walks_beside_the_work["the_hold_walks_beside_the_work"]
    the_holding_returns["the_holding_returns"]
    the_horizon_holds_every_reading["the_horizon_holds_every_reading"]
    the_host_merges_the_guests["the_host_merges_the_guests"]
    the_host_serves_both_branches["the_host_serves_both_branches"]
    the_host_was_a_reseat["the_host_was_a_reseat"]
    the_instinct_replays_its_word["the_instinct_replays_its_word"]
    the_intertwined_walks_agree["the_intertwined_walks_agree"]
    the_intertwiner_carries_the_walk["the_intertwiner_carries_the_walk"]
    the_interview_crosses_the_carrier["the_interview_crosses_the_carrier"]
    the_interview_crosses_the_seat["the_interview_crosses_the_seat"]
    the_ledger_parks_the_word["the_ledger_parks_the_word"]
    the_left_comb_moves_once["the_left_comb_moves_once"]
    the_left_loop_reads_zero["the_left_loop_reads_zero"]
    the_lift_feeds_the_step["the_lift_feeds_the_step"]
    the_lift_is_the_conduct["the_lift_is_the_conduct"]
    the_lift_is_unique["the_lift_is_unique"]
    the_lift_peeks_the_out["the_lift_peeks_the_out"]
    the_listening_turn_is_the_yield["the_listening_turn_is_the_yield"]
    the_maintenance_is_the_identitys_hom["the_maintenance_is_the_identitys_hom"]
    the_manifest_counts["the_manifest_counts"]
    the_manifest_is_natural["the_manifest_is_natural"]
    the_manifest_rebuilds_the_carrier["the_manifest_rebuilds_the_carrier"]
    the_measurement_is_a_meeting["the_measurement_is_a_meeting"]
    the_meeting_mints_the_concord["the_meeting_mints_the_concord"]
    the_meeting_was_a_self_meeting["the_meeting_was_a_self_meeting"]
    the_muffled_tally_is_the_resting_counter["the_muffled_tally_is_the_resting_counter"]
    the_muffler_banks_the_run["the_muffler_banks_the_run"]
    the_mutual_recording_is_unheard["the_mutual_recording_is_unheard"]
    the_mutual_records_ride_together["the_mutual_records_ride_together"]
    the_obs_carries_to_the_one_face["the_obs_carries_to_the_one_face"]
    the_ode_comes_home["the_ode_comes_home"]
    the_origin_is_the_pairs_unit["the_origin_is_the_pairs_unit"]
    the_origin_merges_every_seat["the_origin_merges_every_seat"]
    the_pace_is_carried_onto_the_flip["the_pace_is_carried_onto_the_flip"]
    the_pace_wears_the_tallys_voice["the_pace_wears_the_tallys_voice"]
    the_pairing_is_exact["the_pairing_is_exact"]
    the_pairing_is_unique["the_pairing_is_unique"]
    the_parent_folds_into_the_ground["the_parent_folds_into_the_ground"]
    the_park_resumes["the_park_resumes"]
    the_pentagon_turns_at_four["the_pentagon_turns_at_four"]
    the_pointwise_license["the_pointwise_license"]
    the_probe_boards_as_the_guest["the_probe_boards_as_the_guest"]
    the_reading_is_positive["the_reading_is_positive"]
    the_record_writes_where_the_face_is_blind["the_record_writes_where_the_face_is_blind"]
    the_records_part_the_seats["the_records_part_the_seats"]
    the_rep_lands_where_it_is_fed["the_rep_lands_where_it_is_fed"]
    the_repeated_ask_hears_one_answer["the_repeated_ask_hears_one_answer"]
    the_replay_is_the_machine["the_replay_is_the_machine"]
    the_retuned_seat_walks_the_translated_word["the_retuned_seat_walks_the_translated_word"]
    the_revision_is_a_reading["the_revision_is_a_reading"]
    the_revision_multiplies_the_reading["the_revision_multiplies_the_reading"]
    the_revoice_moves_no_seat["the_revoice_moves_no_seat"]
    the_right_comb_rests["the_right_comb_rests"]
    the_right_loop_reads_zero["the_right_loop_reads_zero"]
    the_room_repeats_no_plan["the_room_repeats_no_plan"]
    the_round_trips_come_home["the_round_trips_come_home"]
    the_seat_map_carries_the_conduct["the_seat_map_carries_the_conduct"]
    the_seats_stack_backward["the_seats_stack_backward"]
    the_self_meeting_reads_the_guest["the_self_meeting_reads_the_guest"]
    the_self_steered_machine_is_a_clock["the_self_steered_machine_is_a_clock"]
    the_settle_is_unheard["the_settle_is_unheard"]
    the_settled_gap_moves_the_model["the_settled_gap_moves_the_model"]
    the_sharpening_is_exact["the_sharpening_is_exact"]
    the_sounding_reads_the_alike["the_sounding_reads_the_alike"]
    the_speaker_rides_unread["the_speaker_rides_unread"]
    the_spoken_arrives_at_the_face["the_spoken_arrives_at_the_face"]
    the_still_hand_is_unheard["the_still_hand_is_unheard"]
    the_tally_parks_at_its_count["the_tally_parks_at_its_count"]
    the_tallys_stream_counts["the_tallys_stream_counts"]
    the_trivial_revision_changes_nothing["the_trivial_revision_changes_nothing"]
    the_turn_returns["the_turn_returns"]
    the_two_listeners_restore_the_table["the_two_listeners_restore_the_table"]
    the_two_shapes_of_three["the_two_shapes_of_three"]
    the_type_is_a_reading["the_type_is_a_reading"]
    the_unheard_hands_compose["the_unheard_hands_compose"]
    the_unit_machine_steers_itself["the_unit_machine_steers_itself"]
    the_voice_crosses_the_seat["the_voice_crosses_the_seat"]
    the_widening_is_exact["the_widening_is_exact"]
    the_wider_voice_releases_the_bank["the_wider_voice_releases_the_bank"]
    the_window_agrees_or_names_the_gap["the_window_agrees_or_names_the_gap"]
    the_yield_fixes_the_agreed["the_yield_fixes_the_agreed"]
    three_has_no_loop["three_has_no_loop"]
    three_is_the_width_of_contact["three_is_the_width_of_contact"]
    two_seats_record_each_other["two_seats_record_each_other"]
  end
  subgraph Room["Room"]
    Room_and_congr_first["and_congr_first"]
    Room_and_congr_second["and_congr_second"]
    Room_and_regroups["and_regroups"]
    Room_apart_append["apart_append"]
    Room_apart_filter["apart_filter"]
    Room_apart_map["apart_map"]
    Room_beq_self["beq_self"]
    Room_ble_le_add["ble_le_add"]
    Room_ble_le_add_left["ble_le_add_left"]
    Room_ble_refl["ble_refl"]
    Room_ble_trans["ble_trans"]
    Room_eq_of_beq["eq_of_beq"]
    Room_filter_holds["filter_holds"]
    Room_len_replicate["len_replicate"]
    Room_lengths_add["lengths_add"]
    Room_map_crosses_append["map_crosses_append"]
    Room_mem_append_left["mem_append_left"]
    Room_mem_append_right["mem_append_right"]
    Room_mem_append_split["mem_append_split"]
    Room_mem_filter_intro["mem_filter_intro"]
    Room_mem_map_back["mem_map_back"]
    Room_mem_map_intro["mem_map_intro"]
    Room_mul_one_reads["mul_one_reads"]
    Room_mul_spreads["mul_spreads"]
    Room_no_mark_lights_itself["no_mark_lights_itself"]
    Room_not_not["not_not"]
    Room_succ_adds["succ_adds"]
    Room_the_append_rests["the_append_rests"]
    Room_the_appends_regroup["the_appends_regroup"]
    Room_the_carriers_compose["the_carriers_compose"]
    Room_the_first_mark_reads["the_first_mark_reads"]
    Room_the_hallway_is_too_small["the_hallway_is_too_small"]
    Room_the_key_is_cut_from_the_room["the_key_is_cut_from_the_room"]
    Room_the_unit_word_is_its_count["the_unit_word_is_its_count"]
    Room_zero_add["zero_add"]
  end
  the_round_trips_come_home --> Room_len_replicate
  the_round_trips_come_home --> Room_the_unit_word_is_its_count
  the_manifest_rebuilds_the_carrier --> Room_the_append_rests
  the_manifest_rebuilds_the_carrier --> the_guests_reboard_in_order
  the_census_is_exact --> Room_mem_filter_intro
  the_census_is_exact --> Room_beq_self
  the_census_is_exact --> the_horizon_holds_every_reading
  the_census_is_exact --> the_room_repeats_no_plan
  the_census_is_exact --> Room_filter_holds
  the_census_is_exact --> Room_apart_filter
  the_census_is_exact --> Room_eq_of_beq
  the_census_is_exact --> Room_ble_refl
  entanglement_is_the_loop --> the_two_shapes_of_three
  entanglement_is_the_loop --> the_pentagon_turns_at_four
  entanglement_is_the_loop --> three_has_no_loop
  every_seat_is_a_reading_of_the_record --> the_park_resumes
  every_seat_is_a_reading_of_the_record --> the_ledger_parks_the_word
  a_wider_seat_reads_the_remainder --> the_widening_is_exact
  only_the_unheard_survives_the_sounding --> the_sounding_reads_the_alike
  only_the_unheard_survives_the_sounding --> no_interview_hears_the_unheard
  mem_cross_split --> Room_mem_map_back
  mem_cross_split --> Room_mem_append_split
  the_meeting_mints_the_concord --> a_role_read_at_a_probe_is_derived
  the_clock_is_a_room --> the_wider_voice_releases_the_bank
  the_clock_is_a_room --> the_settle_is_unheard
  the_clock_is_a_room --> the_self_steered_machine_is_a_clock
  the_clock_is_a_room --> the_tallys_stream_counts
  the_clock_is_a_room --> Room_not_not
  the_mutual_recording_is_unheard --> no_interview_parts_the_alike
  the_mutual_recording_is_unheard --> the_host_merges_the_guests
  the_flywheel_and_the_shell_sound_alike --> an_audition_hears_only_the_conduct
  the_rep_lands_where_it_is_fed --> the_repeated_ask_hears_one_answer
  the_rep_lands_where_it_is_fed --> the_park_resumes
  the_rep_lands_where_it_is_fed --> the_tally_parks_at_its_count
  the_rep_lands_where_it_is_fed --> the_instinct_replays_its_word
  the_right_loop_reads_zero --> no_move_past_the_right_comb
  the_room_repeats_no_plan --> mem_cross_split
  the_room_repeats_no_plan --> the_cross_keeps_apart
  the_settle_is_unheard --> the_hold_walks_beside_the_work
  every_widening_is_one_pairing --> the_pairing_is_exact
  every_widening_is_one_pairing --> Room_and_regroups
  every_widening_is_one_pairing --> Room_and_congr_first
  every_widening_is_one_pairing --> Room_and_congr_second
  the_clocks_lift_is_a_stream --> Room_len_replicate
  the_clocks_lift_is_a_stream --> the_self_steered_machine_is_a_clock
  a_stage_may_ground_a_stage --> the_parent_folds_into_the_ground
  the_intertwiner_carries_the_walk --> the_intertwined_walks_agree
  the_manifest_counts --> Room_lengths_add
  three_is_the_width_of_contact --> the_pairing_is_exact
  three_is_the_width_of_contact --> every_widening_is_one_pairing
  three_is_the_width_of_contact --> the_pentagon_turns_at_four
  three_is_the_width_of_contact --> three_has_no_loop
  three_is_the_width_of_contact --> Room_the_hallway_is_too_small
  the_replay_is_the_machine --> the_intertwined_walks_agree
  the_replay_is_the_machine --> the_park_resumes
  no_interview_hears_the_unheard --> no_interview_parts_the_alike
  the_reading_is_positive --> Room_succ_adds
  the_audition_is_exact --> the_sounding_reads_the_alike
  the_audition_is_exact --> no_interview_parts_the_alike
  the_wider_voice_releases_the_bank --> Room_zero_add
  the_wider_voice_releases_the_bank --> the_tally_parks_at_its_count
  the_concord_is_the_meetings_own --> the_meeting_mints_the_concord
  the_concord_is_the_meetings_own --> the_settled_gap_moves_the_model
  the_concord_is_the_meetings_own --> no_seat_reads_the_concord_alone
  the_concord_is_the_meetings_own --> the_concord_agrees_or_names_the_gap
  the_left_comb_moves_once --> no_move_at_the_mirror
  the_left_comb_moves_once --> no_move_at_the_ground
  the_muffler_banks_the_run --> the_tally_parks_at_its_count
  the_muffler_banks_the_run --> the_revoice_moves_no_seat
  the_guests_reboard_in_order --> Room_the_appends_regroup
  the_ledger_parks_the_word --> Room_the_append_rests
  the_ledger_parks_the_word --> Room_the_appends_regroup
  no_move_past_the_right_comb --> no_move_at_the_mirror
  no_move_past_the_right_comb --> no_move_at_the_ground
  the_hold_walks_beside_the_work --> the_intertwined_walks_agree
  the_hold_walks_beside_the_work --> the_park_resumes
  the_drain_settles --> the_manifest_rebuilds_the_carrier
  room_margin_flywheel_door --> the_wider_voice_releases_the_bank
  room_margin_flywheel_door --> the_flywheel_and_the_shell_sound_alike
  room_margin_flywheel_door --> the_settle_is_unheard
  room_margin_flywheel_door --> Room_the_key_is_cut_from_the_room
  room_margin_flywheel_door --> the_self_steered_machine_is_a_clock
  room_margin_flywheel_door --> Room_no_mark_lights_itself
  room_margin_flywheel_door --> a_wider_seat_reads_the_remainder
  recording_the_recording_grounds --> no_interview_parts_the_alike
  recording_the_recording_grounds --> the_host_merges_the_guests
  the_held_scale_rides --> Room_mul_one_reads
  the_held_scale_rides --> Room_mul_spreads
  three_has_no_loop --> the_right_loop_reads_zero
  three_has_no_loop --> the_left_loop_reads_zero
  the_revision_multiplies_the_reading --> the_parent_folds_into_the_ground
  the_revision_multiplies_the_reading --> the_held_scale_rides
  the_drained_is_on_spec --> the_manifest_counts
  the_unheard_hands_compose --> Room_the_carriers_compose
  mem_cross --> Room_mem_map_intro
  mem_cross --> Room_mem_append_right
  mem_cross --> Room_mem_append_left
  two_seats_record_each_other --> no_interview_parts_the_alike
  two_seats_record_each_other --> the_record_writes_where_the_face_is_blind
  two_seats_record_each_other --> the_host_merges_the_guests
  two_seats_record_each_other --> the_records_part_the_seats
  the_curtain_is_exact --> the_sounding_reads_the_alike
  the_curtain_is_exact --> no_interview_parts_the_alike
  the_manifest_is_natural --> Room_map_crosses_append
  the_lift_is_the_conduct --> the_lift_is_unique
  the_lift_is_the_conduct --> the_audition_is_exact
  the_lift_is_the_conduct --> the_pointwise_license
  the_left_loop_reads_zero --> the_right_comb_rests
  the_left_loop_reads_zero --> the_left_comb_moves_once
  the_right_comb_rests --> no_move_past_the_right_comb
  the_tally_parks_at_its_count --> Room_succ_adds
  the_tallys_stream_counts --> the_wider_voice_releases_the_bank
  the_tallys_stream_counts --> Room_len_replicate
  the_tallys_stream_counts --> the_clocks_lift_is_a_stream
  the_sounding_reads_the_alike --> Room_the_first_mark_reads
  the_buffer_is_invisible --> the_hold_walks_beside_the_work
  the_handshake --> no_interview_parts_the_alike
  the_handshake --> a_wider_seat_reads_the_remainder
  the_handshake --> the_host_merges_the_guests
  the_pace_is_carried_onto_the_flip --> the_intertwiner_carries_the_walk
  no_move_at_the_mirror --> no_move_at_the_ground
  the_clock_writes_its_sequence --> the_round_trips_come_home
  the_clock_writes_its_sequence --> the_sounding_reads_the_alike
  the_clock_writes_its_sequence --> an_audition_hears_only_the_conduct
  the_clock_writes_its_sequence --> the_clocks_lift_is_a_stream
  the_clock_writes_its_sequence --> the_tallys_stream_counts
  lineages_compose --> the_parent_folds_into_the_ground
  the_cross_keeps_apart --> Room_mem_map_back
  the_cross_keeps_apart --> mem_cross_split
  the_cross_keeps_apart --> Room_apart_map
  the_cross_keeps_apart --> Room_apart_append
  correct_maintenance_has_no_signature --> no_interview_hears_the_unheard
  the_settled_gap_moves_the_model --> no_interview_parts_the_alike
  the_settled_gap_moves_the_model --> the_host_merges_the_guests
  the_horizon_holds_every_reading --> Room_succ_adds
  the_horizon_holds_every_reading --> mem_cross
  the_horizon_holds_every_reading --> Room_ble_le_add_left
  the_horizon_holds_every_reading --> the_reading_is_positive
  the_horizon_holds_every_reading --> Room_ble_le_add
  the_horizon_holds_every_reading --> Room_ble_trans
  an_audition_hears_only_the_conduct --> no_interview_parts_the_alike