TG3Differential.lean

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
--
-- TG3Differential.lean — GENERATED by compiler/test/tg3/tg3_emit.ml.  DO NOT EDIT BY HAND.
-- Regenerate: (cd compiler && dune exec ./test/tg3/tg3_emit.exe -- --emit <abs>/proofs/TG3Differential.lean)
--
-- Each `example` certifies that OCaml `infer_expr` agrees with Lean's *proven*
-- `infer` (TG-2: infer ≡ HasType) on one term of the shared core fragment.
-- `by decide` kernel-checks each.  Build via proofs/check-tg3-differential.sh.
-- This is the machine-checked half of TG-3; see proofs/TG3-REFINEMENT.md.
import Tangle
open Tangle

section CoreAgreement
-- OCaml infer_expr result == Lean infer result, for every core-fragment term.
example : infer [] (.num 0) = some .num := by decide  -- 1/490
example : infer [] (.num 1) = some .num := by decide  -- 2/490
example : infer [] (.num 7) = some .num := by decide  -- 3/490
example : infer [] (.num (-3)) = some .num := by decide  -- 4/490
example : infer [] (.str "") = some .str := by decide  -- 5/490
example : infer [] (.str "ab") = some .str := by decide  -- 6/490
example : infer [] (.str "knot") = some .str := by decide  -- 7/490
example : infer [] (.boolLit true) = some .bool := by decide  -- 8/490
example : infer [] (.boolLit false) = some .bool := by decide  -- 9/490
example : infer [] .identity = some (.word 0) := by decide  -- 10/490
example : infer [] (.braidLit []) = some (.word 0) := by decide  -- 11/490
example : infer [] (.braidLit [⟨0, 1⟩]) = some (.word 1) := by decide  -- 12/490
example : infer [] (.braidLit [⟨1, 1⟩]) = some (.word 2) := by decide  -- 13/490
example : infer [] (.braidLit [⟨1, (-1)⟩]) = some (.word 2) := by decide  -- 14/490
example : infer [] (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) = some (.word 2) := by decide  -- 15/490
example : infer [] (.braidLit [⟨2, 1⟩]) = some (.word 3) := by decide  -- 16/490
example : infer [] (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) = some (.word 3) := by decide  -- 17/490
example : infer [] (.compose .identity .identity) = some (.word 0) := by decide  -- 18/490
example : infer [] (.tensor .identity .identity) = some (.word 0) := by decide  -- 19/490
example : infer [] (.pipeline .identity .identity) = some (.word 0) := by decide  -- 20/490
example : infer [] (.compose .identity (.braidLit [])) = some (.word 0) := by decide  -- 21/490
example : infer [] (.tensor .identity (.braidLit [])) = some (.word 0) := by decide  -- 22/490
example : infer [] (.pipeline .identity (.braidLit [])) = some (.word 0) := by decide  -- 23/490
example : infer [] (.compose .identity (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 24/490
example : infer [] (.tensor .identity (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 25/490
example : infer [] (.pipeline .identity (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 26/490
example : infer [] (.compose .identity (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 27/490
example : infer [] (.tensor .identity (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 28/490
example : infer [] (.pipeline .identity (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 29/490
example : infer [] (.compose .identity (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 30/490
example : infer [] (.tensor .identity (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 31/490
example : infer [] (.pipeline .identity (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 32/490
example : infer [] (.compose .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 33/490
example : infer [] (.tensor .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 34/490
example : infer [] (.pipeline .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 35/490
example : infer [] (.compose .identity (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 36/490
example : infer [] (.tensor .identity (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 37/490
example : infer [] (.pipeline .identity (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 38/490
example : infer [] (.compose .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 39/490
example : infer [] (.tensor .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 40/490
example : infer [] (.pipeline .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 41/490
example : infer [] (.compose (.braidLit []) .identity) = some (.word 0) := by decide  -- 42/490
example : infer [] (.tensor (.braidLit []) .identity) = some (.word 0) := by decide  -- 43/490
example : infer [] (.pipeline (.braidLit []) .identity) = some (.word 0) := by decide  -- 44/490
example : infer [] (.compose (.braidLit []) (.braidLit [])) = some (.word 0) := by decide  -- 45/490
example : infer [] (.tensor (.braidLit []) (.braidLit [])) = some (.word 0) := by decide  -- 46/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [])) = some (.word 0) := by decide  -- 47/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 48/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 49/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 50/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 51/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 52/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 53/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 54/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 55/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 56/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 57/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 58/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 59/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 60/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 61/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 62/490
example : infer [] (.compose (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 63/490
example : infer [] (.tensor (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 64/490
example : infer [] (.pipeline (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 65/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) .identity) = some (.word 1) := by decide  -- 66/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) .identity) = some (.word 1) := by decide  -- 67/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) .identity) = some (.word 1) := by decide  -- 68/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [])) = some (.word 1) := by decide  -- 69/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [])) = some (.word 1) := by decide  -- 70/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [])) = some (.word 1) := by decide  -- 71/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 72/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 73/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide  -- 74/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 75/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 3) := by decide  -- 76/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 77/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 78/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 3) := by decide  -- 79/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 80/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 81/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 3) := by decide  -- 82/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 83/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 84/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 4) := by decide  -- 85/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 86/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 87/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 4) := by decide  -- 88/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 89/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 90/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 91/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 92/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 93/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 94/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 95/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 96/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 97/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 98/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 99/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 4) := by decide  -- 100/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 101/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 102/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 4) := by decide  -- 103/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 104/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 105/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 4) := by decide  -- 106/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 107/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 108/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 5) := by decide  -- 109/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 110/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 111/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 5) := by decide  -- 112/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 113/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) .identity) = some (.word 2) := by decide  -- 114/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) .identity) = some (.word 2) := by decide  -- 115/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) .identity) = some (.word 2) := by decide  -- 116/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 117/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 118/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 119/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 120/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 121/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 122/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 123/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 4) := by decide  -- 124/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 125/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 126/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 4) := by decide  -- 127/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 128/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 129/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 4) := by decide  -- 130/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 131/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 132/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 5) := by decide  -- 133/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 134/490
example : infer [] (.compose (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 135/490
example : infer [] (.tensor (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 5) := by decide  -- 136/490
example : infer [] (.pipeline (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 137/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 138/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 139/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = some (.word 2) := by decide  -- 140/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 141/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 142/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = some (.word 2) := by decide  -- 143/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 144/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 145/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 2) := by decide  -- 146/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 147/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 4) := by decide  -- 148/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 2) := by decide  -- 149/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 150/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 4) := by decide  -- 151/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 2) := by decide  -- 152/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 153/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 4) := by decide  -- 154/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 2) := by decide  -- 155/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 156/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 5) := by decide  -- 157/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 158/490
example : infer [] (.compose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 159/490
example : infer [] (.tensor (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 5) := by decide  -- 160/490
example : infer [] (.pipeline (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 161/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) .identity) = some (.word 3) := by decide  -- 162/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) .identity) = some (.word 3) := by decide  -- 163/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) .identity) = some (.word 3) := by decide  -- 164/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 165/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 166/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 167/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 168/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 4) := by decide  -- 169/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 170/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 3) := by decide  -- 171/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 5) := by decide  -- 172/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 3) := by decide  -- 173/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 3) := by decide  -- 174/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 5) := by decide  -- 175/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 3) := by decide  -- 176/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 3) := by decide  -- 177/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 5) := by decide  -- 178/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 3) := by decide  -- 179/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 180/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 6) := by decide  -- 181/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 182/490
example : infer [] (.compose (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 183/490
example : infer [] (.tensor (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 6) := by decide  -- 184/490
example : infer [] (.pipeline (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 185/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = some (.word 3) := by decide  -- 186/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = some (.word 3) := by decide  -- 187/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = some (.word 3) := by decide  -- 188/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 189/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 190/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = some (.word 3) := by decide  -- 191/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 192/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 4) := by decide  -- 193/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.word 3) := by decide  -- 194/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 3) := by decide  -- 195/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 5) := by decide  -- 196/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.word 3) := by decide  -- 197/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 3) := by decide  -- 198/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 5) := by decide  -- 199/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.word 3) := by decide  -- 200/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 3) := by decide  -- 201/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 5) := by decide  -- 202/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.word 3) := by decide  -- 203/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 204/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 6) := by decide  -- 205/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.word 3) := by decide  -- 206/490
example : infer [] (.compose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 207/490
example : infer [] (.tensor (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 6) := by decide  -- 208/490
example : infer [] (.pipeline (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.word 3) := by decide  -- 209/490
example : infer [] (.add (.num 0) (.num 0)) = some .num := by decide  -- 210/490
example : infer [] (.add (.num 0) (.num 1)) = some .num := by decide  -- 211/490
example : infer [] (.add (.num 0) (.num 7)) = some .num := by decide  -- 212/490
example : infer [] (.add (.num 0) (.num (-3))) = some .num := by decide  -- 213/490
example : infer [] (.add (.num 1) (.num 0)) = some .num := by decide  -- 214/490
example : infer [] (.add (.num 1) (.num 1)) = some .num := by decide  -- 215/490
example : infer [] (.add (.num 1) (.num 7)) = some .num := by decide  -- 216/490
example : infer [] (.add (.num 1) (.num (-3))) = some .num := by decide  -- 217/490
example : infer [] (.add (.num 7) (.num 0)) = some .num := by decide  -- 218/490
example : infer [] (.add (.num 7) (.num 1)) = some .num := by decide  -- 219/490
example : infer [] (.add (.num 7) (.num 7)) = some .num := by decide  -- 220/490
example : infer [] (.add (.num 7) (.num (-3))) = some .num := by decide  -- 221/490
example : infer [] (.add (.num (-3)) (.num 0)) = some .num := by decide  -- 222/490
example : infer [] (.add (.num (-3)) (.num 1)) = some .num := by decide  -- 223/490
example : infer [] (.add (.num (-3)) (.num 7)) = some .num := by decide  -- 224/490
example : infer [] (.add (.num (-3)) (.num (-3))) = some .num := by decide  -- 225/490
example : infer [] (.eq (.num 0) (.num 0)) = some .bool := by decide  -- 226/490
example : infer [] (.eq (.num 0) (.num 1)) = some .bool := by decide  -- 227/490
example : infer [] (.eq (.num 0) (.num 7)) = some .bool := by decide  -- 228/490
example : infer [] (.eq (.num 0) (.num (-3))) = some .bool := by decide  -- 229/490
example : infer [] (.eq (.num 1) (.num 0)) = some .bool := by decide  -- 230/490
example : infer [] (.eq (.num 1) (.num 1)) = some .bool := by decide  -- 231/490
example : infer [] (.eq (.num 1) (.num 7)) = some .bool := by decide  -- 232/490
example : infer [] (.eq (.num 1) (.num (-3))) = some .bool := by decide  -- 233/490
example : infer [] (.eq (.num 7) (.num 0)) = some .bool := by decide  -- 234/490
example : infer [] (.eq (.num 7) (.num 1)) = some .bool := by decide  -- 235/490
example : infer [] (.eq (.num 7) (.num 7)) = some .bool := by decide  -- 236/490
example : infer [] (.eq (.num 7) (.num (-3))) = some .bool := by decide  -- 237/490
example : infer [] (.eq (.num (-3)) (.num 0)) = some .bool := by decide  -- 238/490
example : infer [] (.eq (.num (-3)) (.num 1)) = some .bool := by decide  -- 239/490
example : infer [] (.eq (.num (-3)) (.num 7)) = some .bool := by decide  -- 240/490
example : infer [] (.eq (.num (-3)) (.num (-3))) = some .bool := by decide  -- 241/490
example : infer [] (.eq (.str "") (.str "")) = some .bool := by decide  -- 242/490
example : infer [] (.eq (.str "") (.str "ab")) = some .bool := by decide  -- 243/490
example : infer [] (.eq (.str "") (.str "knot")) = some .bool := by decide  -- 244/490
example : infer [] (.eq (.str "ab") (.str "")) = some .bool := by decide  -- 245/490
example : infer [] (.eq (.str "ab") (.str "ab")) = some .bool := by decide  -- 246/490
example : infer [] (.eq (.str "ab") (.str "knot")) = some .bool := by decide  -- 247/490
example : infer [] (.eq (.str "knot") (.str "")) = some .bool := by decide  -- 248/490
example : infer [] (.eq (.str "knot") (.str "ab")) = some .bool := by decide  -- 249/490
example : infer [] (.eq (.str "knot") (.str "knot")) = some .bool := by decide  -- 250/490
example : infer [] (.eq .identity .identity) = some .bool := by decide  -- 251/490
example : infer [] (.eq .identity (.braidLit [])) = some .bool := by decide  -- 252/490
example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 253/490
example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 254/490
example : infer [] (.eq .identity (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 255/490
example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 256/490
example : infer [] (.eq .identity (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 257/490
example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 258/490
example : infer [] (.eq (.braidLit []) .identity) = some .bool := by decide  -- 259/490
example : infer [] (.eq (.braidLit []) (.braidLit [])) = some .bool := by decide  -- 260/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 261/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 262/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 263/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 264/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 265/490
example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 266/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) .identity) = some .bool := by decide  -- 267/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [])) = some .bool := by decide  -- 268/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 269/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 270/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 271/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 272/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 273/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 274/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) .identity) = some .bool := by decide  -- 275/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [])) = some .bool := by decide  -- 276/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 277/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 278/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 279/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 280/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 281/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 282/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) .identity) = some .bool := by decide  -- 283/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = some .bool := by decide  -- 284/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 285/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 286/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 287/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 288/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 289/490
example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 290/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = some .bool := by decide  -- 291/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = some .bool := by decide  -- 292/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 293/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 294/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 295/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 296/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 297/490
example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 298/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) .identity) = some .bool := by decide  -- 299/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [])) = some .bool := by decide  -- 300/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 301/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 302/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 303/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 304/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 305/490
example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 306/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = some .bool := by decide  -- 307/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = some .bool := by decide  -- 308/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide  -- 309/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide  -- 310/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide  -- 311/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide  -- 312/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide  -- 313/490
example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide  -- 314/490
example : infer [] (.echoClose .identity) = some (.echo (.word 0) (.word 0)) := by decide  -- 315/490
example : infer [] (.lower (.echoClose .identity)) = some (.word 0) := by decide  -- 316/490
example : infer [] (.residue (.echoClose .identity)) = some (.word 0) := by decide  -- 317/490
example : infer [] (.echoClose (.braidLit [])) = some (.echo (.word 0) (.word 0)) := by decide  -- 318/490
example : infer [] (.lower (.echoClose (.braidLit []))) = some (.word 0) := by decide  -- 319/490
example : infer [] (.residue (.echoClose (.braidLit []))) = some (.word 0) := by decide  -- 320/490
example : infer [] (.echoClose (.braidLit [⟨0, 1⟩])) = some (.echo (.word 1) (.word 0)) := by decide  -- 321/490
example : infer [] (.lower (.echoClose (.braidLit [⟨0, 1⟩]))) = some (.word 0) := by decide  -- 322/490
example : infer [] (.residue (.echoClose (.braidLit [⟨0, 1⟩]))) = some (.word 1) := by decide  -- 323/490
example : infer [] (.echoClose (.braidLit [⟨1, 1⟩])) = some (.echo (.word 2) (.word 0)) := by decide  -- 324/490
example : infer [] (.lower (.echoClose (.braidLit [⟨1, 1⟩]))) = some (.word 0) := by decide  -- 325/490
example : infer [] (.residue (.echoClose (.braidLit [⟨1, 1⟩]))) = some (.word 2) := by decide  -- 326/490
example : infer [] (.echoClose (.braidLit [⟨1, (-1)⟩])) = some (.echo (.word 2) (.word 0)) := by decide  -- 327/490
example : infer [] (.lower (.echoClose (.braidLit [⟨1, (-1)⟩]))) = some (.word 0) := by decide  -- 328/490
example : infer [] (.residue (.echoClose (.braidLit [⟨1, (-1)⟩]))) = some (.word 2) := by decide  -- 329/490
example : infer [] (.echoClose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.echo (.word 2) (.word 0)) := by decide  -- 330/490
example : infer [] (.lower (.echoClose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]))) = some (.word 0) := by decide  -- 331/490
example : infer [] (.residue (.echoClose (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]))) = some (.word 2) := by decide  -- 332/490
example : infer [] (.echoClose (.braidLit [⟨2, 1⟩])) = some (.echo (.word 3) (.word 0)) := by decide  -- 333/490
example : infer [] (.lower (.echoClose (.braidLit [⟨2, 1⟩]))) = some (.word 0) := by decide  -- 334/490
example : infer [] (.residue (.echoClose (.braidLit [⟨2, 1⟩]))) = some (.word 3) := by decide  -- 335/490
example : infer [] (.echoClose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.echo (.word 3) (.word 0)) := by decide  -- 336/490
example : infer [] (.lower (.echoClose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]))) = some (.word 0) := by decide  -- 337/490
example : infer [] (.residue (.echoClose (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]))) = some (.word 3) := by decide  -- 338/490
example : infer [] (.echoAdd (.num 0) (.num 0)) = some (.echo (.prod .num .num) .num) := by decide  -- 339/490
example : infer [] (.echoAdd (.num 0) (.num 1)) = some (.echo (.prod .num .num) .num) := by decide  -- 340/490
example : infer [] (.echoAdd (.num 0) (.num 7)) = some (.echo (.prod .num .num) .num) := by decide  -- 341/490
example : infer [] (.echoAdd (.num 0) (.num (-3))) = some (.echo (.prod .num .num) .num) := by decide  -- 342/490
example : infer [] (.echoAdd (.num 1) (.num 0)) = some (.echo (.prod .num .num) .num) := by decide  -- 343/490
example : infer [] (.echoAdd (.num 1) (.num 1)) = some (.echo (.prod .num .num) .num) := by decide  -- 344/490
example : infer [] (.echoAdd (.num 1) (.num 7)) = some (.echo (.prod .num .num) .num) := by decide  -- 345/490
example : infer [] (.echoAdd (.num 1) (.num (-3))) = some (.echo (.prod .num .num) .num) := by decide  -- 346/490
example : infer [] (.echoAdd (.num 7) (.num 0)) = some (.echo (.prod .num .num) .num) := by decide  -- 347/490
example : infer [] (.echoAdd (.num 7) (.num 1)) = some (.echo (.prod .num .num) .num) := by decide  -- 348/490
example : infer [] (.echoAdd (.num 7) (.num 7)) = some (.echo (.prod .num .num) .num) := by decide  -- 349/490
example : infer [] (.echoAdd (.num 7) (.num (-3))) = some (.echo (.prod .num .num) .num) := by decide  -- 350/490
example : infer [] (.echoAdd (.num (-3)) (.num 0)) = some (.echo (.prod .num .num) .num) := by decide  -- 351/490
example : infer [] (.echoAdd (.num (-3)) (.num 1)) = some (.echo (.prod .num .num) .num) := by decide  -- 352/490
example : infer [] (.echoAdd (.num (-3)) (.num 7)) = some (.echo (.prod .num .num) .num) := by decide  -- 353/490
example : infer [] (.echoAdd (.num (-3)) (.num (-3))) = some (.echo (.prod .num .num) .num) := by decide  -- 354/490
example : infer [] (.echoEq (.num 0) (.num 0)) = some (.echo (.prod .num .num) .bool) := by decide  -- 355/490
example : infer [] (.echoEq (.num 0) (.num 1)) = some (.echo (.prod .num .num) .bool) := by decide  -- 356/490
example : infer [] (.echoEq (.num 0) (.num 7)) = some (.echo (.prod .num .num) .bool) := by decide  -- 357/490
example : infer [] (.echoEq (.num 0) (.num (-3))) = some (.echo (.prod .num .num) .bool) := by decide  -- 358/490
example : infer [] (.echoEq (.num 1) (.num 0)) = some (.echo (.prod .num .num) .bool) := by decide  -- 359/490
example : infer [] (.echoEq (.num 1) (.num 1)) = some (.echo (.prod .num .num) .bool) := by decide  -- 360/490
example : infer [] (.echoEq (.num 1) (.num 7)) = some (.echo (.prod .num .num) .bool) := by decide  -- 361/490
example : infer [] (.echoEq (.num 1) (.num (-3))) = some (.echo (.prod .num .num) .bool) := by decide  -- 362/490
example : infer [] (.echoEq (.num 7) (.num 0)) = some (.echo (.prod .num .num) .bool) := by decide  -- 363/490
example : infer [] (.echoEq (.num 7) (.num 1)) = some (.echo (.prod .num .num) .bool) := by decide  -- 364/490
example : infer [] (.echoEq (.num 7) (.num 7)) = some (.echo (.prod .num .num) .bool) := by decide  -- 365/490
example : infer [] (.echoEq (.num 7) (.num (-3))) = some (.echo (.prod .num .num) .bool) := by decide  -- 366/490
example : infer [] (.echoEq (.num (-3)) (.num 0)) = some (.echo (.prod .num .num) .bool) := by decide  -- 367/490
example : infer [] (.echoEq (.num (-3)) (.num 1)) = some (.echo (.prod .num .num) .bool) := by decide  -- 368/490
example : infer [] (.echoEq (.num (-3)) (.num 7)) = some (.echo (.prod .num .num) .bool) := by decide  -- 369/490
example : infer [] (.echoEq (.num (-3)) (.num (-3))) = some (.echo (.prod .num .num) .bool) := by decide  -- 370/490
example : infer [] (.echoEq (.str "") (.str "")) = some (.echo (.prod .str .str) .bool) := by decide  -- 371/490
example : infer [] (.echoEq (.str "") (.str "ab")) = some (.echo (.prod .str .str) .bool) := by decide  -- 372/490
example : infer [] (.echoEq (.str "") (.str "knot")) = some (.echo (.prod .str .str) .bool) := by decide  -- 373/490
example : infer [] (.echoEq (.str "ab") (.str "")) = some (.echo (.prod .str .str) .bool) := by decide  -- 374/490
example : infer [] (.echoEq (.str "ab") (.str "ab")) = some (.echo (.prod .str .str) .bool) := by decide  -- 375/490
example : infer [] (.echoEq (.str "ab") (.str "knot")) = some (.echo (.prod .str .str) .bool) := by decide  -- 376/490
example : infer [] (.echoEq (.str "knot") (.str "")) = some (.echo (.prod .str .str) .bool) := by decide  -- 377/490
example : infer [] (.echoEq (.str "knot") (.str "ab")) = some (.echo (.prod .str .str) .bool) := by decide  -- 378/490
example : infer [] (.echoEq (.str "knot") (.str "knot")) = some (.echo (.prod .str .str) .bool) := by decide  -- 379/490
example : infer [] (.echoEq .identity .identity) = some (.echo (.prod (.word 0) (.word 0)) .bool) := by decide  -- 380/490
example : infer [] (.echoEq .identity (.braidLit [])) = some (.echo (.prod (.word 0) (.word 0)) .bool) := by decide  -- 381/490
example : infer [] (.echoEq .identity (.braidLit [⟨0, 1⟩])) = none := by decide  -- 382/490
example : infer [] (.echoEq .identity (.braidLit [⟨1, 1⟩])) = none := by decide  -- 383/490
example : infer [] (.echoEq .identity (.braidLit [⟨1, (-1)⟩])) = none := by decide  -- 384/490
example : infer [] (.echoEq .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide  -- 385/490
example : infer [] (.echoEq .identity (.braidLit [⟨2, 1⟩])) = none := by decide  -- 386/490
example : infer [] (.echoEq .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 387/490
example : infer [] (.echoEq (.braidLit []) .identity) = some (.echo (.prod (.word 0) (.word 0)) .bool) := by decide  -- 388/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [])) = some (.echo (.prod (.word 0) (.word 0)) .bool) := by decide  -- 389/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 390/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨1, 1⟩])) = none := by decide  -- 391/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = none := by decide  -- 392/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide  -- 393/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨2, 1⟩])) = none := by decide  -- 394/490
example : infer [] (.echoEq (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 395/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) .identity) = none := by decide  -- 396/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [])) = none := by decide  -- 397/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some (.echo (.prod (.word 1) (.word 1)) .bool) := by decide  -- 398/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide  -- 399/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide  -- 400/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide  -- 401/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide  -- 402/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 403/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) .identity) = none := by decide  -- 404/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [])) = none := by decide  -- 405/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 406/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 407/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 408/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 409/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide  -- 410/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 411/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) .identity) = none := by decide  -- 412/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = none := by decide  -- 413/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 414/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 415/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 416/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 417/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide  -- 418/490
example : infer [] (.echoEq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 419/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = none := by decide  -- 420/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = none := by decide  -- 421/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 422/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 423/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 424/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some (.echo (.prod (.word 2) (.word 2)) .bool) := by decide  -- 425/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide  -- 426/490
example : infer [] (.echoEq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide  -- 427/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) .identity) = none := by decide  -- 428/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [])) = none := by decide  -- 429/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 430/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide  -- 431/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide  -- 432/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide  -- 433/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.echo (.prod (.word 3) (.word 3)) .bool) := by decide  -- 434/490
example : infer [] (.echoEq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.echo (.prod (.word 3) (.word 3)) .bool) := by decide  -- 435/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = none := by decide  -- 436/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = none := by decide  -- 437/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide  -- 438/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide  -- 439/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide  -- 440/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide  -- 441/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some (.echo (.prod (.word 3) (.word 3)) .bool) := by decide  -- 442/490
example : infer [] (.echoEq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some (.echo (.prod (.word 3) (.word 3)) .bool) := by decide  -- 443/490
example : infer [] (.lower (.echoAdd (.num 1) (.num 2))) = some .num := by decide  -- 444/490
example : infer [] (.residue (.echoAdd (.num 1) (.num 2))) = some (.prod .num .num) := by decide  -- 445/490
example : infer [] (.fst (.residue (.echoAdd (.num 1) (.num 2)))) = some .num := by decide  -- 446/490
example : infer [] (.snd (.residue (.echoEq (.str "a") (.str "b")))) = some .str := by decide  -- 447/490
example : infer [] (.residue (.echoEq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩]))) = some (.prod (.word 2) (.word 2)) := by decide  -- 448/490
example : infer [] (.pair (.num 0) (.num 0)) = some (.prod .num .num) := by decide  -- 449/490
example : infer [] (.pair (.num 1) (.num 0)) = some (.prod .num .num) := by decide  -- 450/490
example : infer [] (.pair (.num 7) (.num 0)) = some (.prod .num .num) := by decide  -- 451/490
example : infer [] (.pair (.num (-3)) (.num 0)) = some (.prod .num .num) := by decide  -- 452/490
example : infer [] (.pair (.str "") (.num 0)) = some (.prod .str .num) := by decide  -- 453/490
example : infer [] (.pair (.str "ab") (.num 0)) = some (.prod .str .num) := by decide  -- 454/490
example : infer [] (.pair (.str "knot") (.num 0)) = some (.prod .str .num) := by decide  -- 455/490
example : infer [] (.pair (.boolLit true) (.num 0)) = some (.prod .bool .num) := by decide  -- 456/490
example : infer [] (.pair (.boolLit false) (.num 0)) = some (.prod .bool .num) := by decide  -- 457/490
example : infer [] (.pair .identity (.num 0)) = some (.prod (.word 0) .num) := by decide  -- 458/490
example : infer [] (.pair (.braidLit []) (.num 0)) = some (.prod (.word 0) .num) := by decide  -- 459/490
example : infer [] (.pair (.braidLit [⟨0, 1⟩]) (.num 0)) = some (.prod (.word 1) .num) := by decide  -- 460/490
example : infer [] (.pair (.braidLit [⟨1, 1⟩]) (.num 0)) = some (.prod (.word 2) .num) := by decide  -- 461/490
example : infer [] (.pair (.braidLit [⟨1, (-1)⟩]) (.num 0)) = some (.prod (.word 2) .num) := by decide  -- 462/490
example : infer [] (.pair (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.num 0)) = some (.prod (.word 2) .num) := by decide  -- 463/490
example : infer [] (.pair (.braidLit [⟨2, 1⟩]) (.num 0)) = some (.prod (.word 3) .num) := by decide  -- 464/490
example : infer [] (.pair (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.num 0)) = some (.prod (.word 3) .num) := by decide  -- 465/490
example : infer [] (.fst (.pair (.braidLit [⟨1, 1⟩]) (.num 0))) = some (.word 2) := by decide  -- 466/490
example : infer [] (.snd (.pair (.braidLit [⟨1, 1⟩]) (.str "x"))) = some .str := by decide  -- 467/490
example : infer [] (.pair (.pair (.num 1) (.str "a")) (.boolLit true)) = some (.prod (.prod .num .str) .bool) := by decide  -- 468/490
example : infer [] (.fst (.fst (.pair (.pair (.num 1) (.str "a")) (.boolLit true)))) = some .num := by decide  -- 469/490
example : infer [] (.snd (.fst (.pair (.pair (.num 1) (.str "a")) (.boolLit true)))) = some .str := by decide  -- 470/490
example : infer [] (.lett (.num 5) (.var 0)) = some .num := by decide  -- 471/490
example : infer [] (.lett (.braidLit [⟨1, 1⟩]) (.var 0)) = some (.word 2) := by decide  -- 472/490
example : infer [] (.lett (.num 5) (.add (.var 0) (.num 1))) = some .num := by decide  -- 473/490
example : infer [] (.lett (.braidLit [⟨1, 1⟩]) (.compose (.var 0) (.var 0))) = some (.word 2) := by decide  -- 474/490
example : infer [] (.lett (.num 1) (.lett (.str "a") (.snd (.pair (.var 1) (.var 0))))) = some .str := by decide  -- 475/490
example : infer [] (.lett (.num 1) (.lett (.braidLit [⟨2, 1⟩]) (.fst (.pair (.var 0) (.var 1))))) = some (.word 3) := by decide  -- 476/490
example : infer [] (.lett (.num 1) (.lett .identity (.var 0))) = some (.word 0) := by decide  -- 477/490
example : infer [] (.lett (.num 1) (.lett (.braidLit [⟨2, 1⟩]) (.compose (.var 0) (.var 0)))) = some (.word 3) := by decide  -- 478/490
example : infer [] (.lett (.echoClose (.braidLit [⟨1, 1⟩])) (.residue (.var 0))) = some (.word 2) := by decide  -- 479/490
example : infer [] (.lett (.num 1) (.add (.var 0) (.lett (.num 2) (.var 0)))) = some .num := by decide  -- 480/490
example : infer [] (.add (.braidLit []) (.num 1)) = none := by decide  -- 481/490
example : infer [] (.compose (.num 1) (.num 2)) = none := by decide  -- 482/490
example : infer [] (.tensor (.str "a") .identity) = none := by decide  -- 483/490
example : infer [] (.lower (.num 1)) = none := by decide  -- 484/490
example : infer [] (.residue (.boolLit true)) = none := by decide  -- 485/490
example : infer [] (.fst (.num 1)) = none := by decide  -- 486/490
example : infer [] (.snd .identity) = none := by decide  -- 487/490
example : infer [] (.echoAdd (.str "a") (.num 1)) = none := by decide  -- 488/490
example : infer [] (.echoClose (.num 1)) = none := by decide  -- 489/490
example : infer [] (.eq (.num 1) (.str "a")) = none := by decide  -- 490/490
end CoreAgreement

section Divergences
-- The complete divergence catalogue.  Each pins the LEAN side; the OCaml
-- side (shown) is pinned by compiler/test/tg3 --check.  `close` is the sole
-- core boundary gateway (OCaml lifts Word→Tangle[I,I]); D2 is bool-eq.
-- D1  close(braid[s0]): OCaml Tangle[I,I] vs Lean Word[0]  [OCaml: Tangle[I, I]]
example : infer [] (.close (.braidLit [⟨0, 1⟩])) = some (.word 0) := by decide
-- D1b  pipeline(close,close): OCaml Tangle[I,I] vs Lean Word[0]  [OCaml: Tangle[I, I]]
example : infer [] (.pipeline (.close (.braidLit [⟨0, 1⟩])) (.close (.braidLit [⟨0, 1⟩]))) = some (.word 0) := by decide
-- D1c  compose(braid[s0],close): OCaml REJECT vs Lean Word[1]  [OCaml: REJECT]
example : infer [] (.compose (.braidLit [⟨0, 1⟩]) (.close (.braidLit [⟨0, 1⟩]))) = some (.word 1) := by decide
-- D1c'  compose(close,braid[s0]): OCaml REJECT vs Lean Word[1]  [OCaml: REJECT]
example : infer [] (.compose (.close (.braidLit [⟨0, 1⟩])) (.braidLit [⟨0, 1⟩])) = some (.word 1) := by decide
-- D1d  add(close,close): OCaml Tangle[I,I] vs Lean none (close⇒word 0, not num)  [OCaml: Tangle[I, I]]
example : infer [] (.add (.close (.braidLit [⟨0, 1⟩])) (.close (.braidLit [⟨0, 1⟩]))) = none := by decide
-- D2  true == false: OCaml Bool vs Lean none (no bool-eq rule)  [OCaml: Bool]
example : infer [] (.eq (.boolLit true) (.boolLit false)) = none := by decide
end Divergences