The Principia Machina/TPC-PY/gen eom corpus.py: Difference between revisions
TPC-PY source gen_eom_corpus.py (-), SHA-256 2f2a8aad7ffc1b24; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0) |
m 1 revision imported |
(No difference)
| |
Latest revision as of 02:11, 30 September 2026
# -*- coding: utf-8 -*-
"""Generator for tpc/vectors/eom_corpus.json: tpc_eom 0.1.0 (proposed), the
structure check of a kernel's equations of motion (D176.1, taken
2026-09-26, pause 0.3.0 D176 Option 1 on D176.3's slots (a)-(e); D177.1
for the D variable; standing rulings S22-S31). Specification and report:
out_R2/tpm_eom_check_0_1_0.txt (agent R2, EOM round pass 4).
THE FIXTURES are the research drafts of the EOM round with a ROLE added to
every LAW by physics (and ROLE INPUT on the Langevin noise DOF): out/A/suite
(A01-A29), out/B/work (g1-g6), out/D/examples (spring_*, corner_*),
out/E/suite (E01-E03), each in the schema 0.5.0 shape of BRIEF_COMMON_P4
section 2; ASSUMPTION and BOUNDARY dropped (not read) except in the spring,
which keeps its TrM and full TMS (not read either). Variants carry a suffix
(A03c_eomz, A13_en_constraint, A20_no_input, spring_draft_eomz,
E03_shape). The role table is in the report, section 8. Synthetic kernels
are built by K() below. Test fixtures, not physics under research.
EXPECTATIONS. A refusal and every eom_class answer is written literally by
hand in its case. Every other expectation is a literal in EXPECTED at the
end of this file, computed by an independent brute-force oracle (not in the
tree: out_R2/work/oracle_eom.py, which shares only tpc_form's parser) and
checked against the hand facts in each case (HAS: substrings the literal
must hold). The generator refuses to write the corpus if the module
disagrees with any expectation; "--unchecked" writes it without the module
(vectors first). Deterministic; no randomness. 0.1.2 (C-MS-5, increment
11): the decode/ cases tell a JSON {} from a JSON []; the corpus is written
with LF line ends on every platform (S65). 0.2.0 (increment 12,
tpm_record_functions 0.1.0 section 12.1): STATUS is one of PROVISIONAL,
ESTABLISHED, REFUTED, WITHDRAWN and HELD, the last three not standing;
VOID and STRUCK are refused, so the two VOID fixtures and the STRUCK
fixture are re-expected as refusals (hand literals), e01-record-order's
ordering fact moves to e01-record-order-withdrawn, and WITHDRAWN, NOT
GRADED and UNMARKED get their cases.
Run: cd tpc && python3 gen_eom_corpus.py (Windows: py ...)."""
import copy
import json
import os
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
import tpc_strike as S # noqa: E402
import tpc_form as F # noqa: E402
FIXTURES = {
"A01": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A02": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s y - m g_n","REFS":["m","v","k_s","y","t","g_n"],"EQUATION":"m * D(v, t) = -k_s * y - m * g_n","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A03a": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1","VALUE":"1","UNIT":"kg"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2Z","STATEMENT":"m d2z/dt2 = -m g_n","REFS":["m","z","t","g_n"],"EQUATION":"m * D(z, t, 2) = -m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_TABLE","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"the block stays on the table top z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A03b": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"N_z","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1","VALUE":"1","UNIT":"kg"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2Z","STATEMENT":"m d2z/dt2 = N_z - m g_n","REFS":["m","z","t","N_z","g_n"],"EQUATION":"m * D(z, t, 2) = N_z - m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_TABLE","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"the block stays on the table top z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A03c": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2Z","STATEMENT":"m d2z/dt2 = -m g_n","REFS":["m","z","t","g_n"],"EQUATION":"m * D(z, t, 2) = -m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_TABLE","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"the block stays on the table top z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A03c_eomz": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2Z","STATEMENT":"m d2z/dt2 = -m g_n","REFS":["m","z","t","g_n"],"EQUATION":"m * D(z, t, 2) = -m * g_n","ROLE":"EOM(z)"}],"CONSTRAINT":[{"NAME":"C_TABLE","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"the block stays on the table top z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A04a": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"C_d","DIMENSION":"1"},{"NAME":"A_ref","DIMENSION":"L2"},{"NAME":"d_ref","DIMENSION":"L1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"},{"NAME":"mu_air","DIMENSION":"M1 L-1 T-1","VALUE":"1.7894e-5","UNIT":"Pa s"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"DX","STATEMENT":"m dvx/dt = -(1/2) rho C_d A |v| vx","REFS":["m","vx","vy","t","rho_air","C_d","A_ref"],"EQUATION":"m * D(vx, t) = -0.5 * rho_air * C_d * A_ref * vx * sqrt(vx^2 + vy^2)","ROLE":"EOM(vx)"},{"NAME":"DY","STATEMENT":"m dvy/dt = -m g_n - (1/2) rho C_d A |v| vy","REFS":["m","vx","vy","t","rho_air","C_d","A_ref","g_n"],"EQUATION":"m * D(vy, t) = -m * g_n - 0.5 * rho_air * C_d * A_ref * vy * sqrt(vx^2 + vy^2)","ROLE":"EOM(vy)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A04b": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"C_d","DIMENSION":"1"},{"NAME":"A_ref","DIMENSION":"L2"},{"NAME":"d_ref","DIMENSION":"L1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"},{"NAME":"mu_air","DIMENSION":"M1 L-1 T-1","VALUE":"1.7894e-5","UNIT":"Pa s"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"DX","STATEMENT":"m dvx/dt = -(1/2) rho C_d A |v| vx","REFS":["m","vx","vy","t","rho_air","C_d","A_ref"],"EQUATION":"m * D(vx, t) = -0.5 * rho_air * C_d * A_ref * vx * sqrt(vx^2 + vy^2)","ROLE":"EOM(vx)"},{"NAME":"DY","STATEMENT":"m dvy/dt = -m g_n - (1/2) rho C_d A |v| vy","REFS":["m","vx","vy","t","rho_air","C_d","A_ref","g_n"],"EQUATION":"m * D(vy, t) = -m * g_n - 0.5 * rho_air * C_d * A_ref * vy * sqrt(vx^2 + vy^2)","ROLE":"EOM(vy)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A05": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"C_d","DIMENSION":"1"},{"NAME":"A_ref","DIMENSION":"L2"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"}],"LAW":[{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"},{"NAME":"N2","STATEMENT":"m dv/dt = -m g_n - (1/2) rho C_d A v |v|","REFS":["m","v","t","g_n","rho_air","C_d","A_ref"],"EQUATION":"m * D(v, t) = -m * g_n - 0.5 * rho_air * C_d * A_ref * v * abs(v)","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A06": {"TPK":{"DOF":[{"NAME":"theta","DIMENSION":"1"},{"NAME":"omega","DIMENSION":"T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"L_p","DIMENSION":"L1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"KIN","STATEMENT":"dtheta/dt = omega","REFS":["theta","omega","t"],"EQUATION":"D(theta, t) = omega","ROLE":"EOM(theta)"},{"NAME":"N2","STATEMENT":"L domega/dt = -g_n sin(theta)","REFS":["L_p","omega","t","g_n","theta"],"EQUATION":"L_p * D(omega, t) = -g_n * sin(theta)","ROLE":"EOM(omega)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A07": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"lam","DIMENSION":"M1 T-2"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"L_p","DIMENSION":"L1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"NX","STATEMENT":"m dvx/dt = -lam x","REFS":["m","vx","t","lam","x"],"EQUATION":"m * D(vx, t) = -lam * x","ROLE":"EOM(vx)"},{"NAME":"NY","STATEMENT":"m dvy/dt = -lam y - m g_n","REFS":["m","vy","t","lam","y","g_n"],"EQUATION":"m * D(vy, t) = -lam * y - m * g_n","ROLE":"EOM(vy)"},{"NAME":"ROD","STATEMENT":"x^2 + y^2 = L^2","REFS":["x","y","L_p"],"EQUATION":"x^2 + y^2 = L_p^2","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A08": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"mu_k","DIMENSION":"1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x - mu_k m g_n sgn(v)","REFS":["m","v","t","k_s","x","mu_k","g_n"],"EQUATION":"m * D(v, t) = -k_s * x - mu_k * m * g_n * v / abs(v)","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A09": {"TPK":{"DOF":[{"NAME":"F1","DIMENSION":"M1 L1 T-2"},{"NAME":"F2","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"W","DIMENSION":"M1 L1 T-2","VALUE":"100","UNIT":"N"},{"NAME":"alpha","DIMENSION":"1","VALUE":"0.5236","UNIT":"rad"}],"LAW":[{"NAME":"FX","STATEMENT":"F1 cos(alpha) - F2 cos(alpha) = 0","REFS":["F1","F2","alpha"],"EQUATION":"F1 * cos(alpha) - F2 * cos(alpha) = 0","ROLE":"CONSTRAINT"},{"NAME":"FY","STATEMENT":"F1 sin(alpha) + F2 sin(alpha) = W","REFS":["F1","F2","alpha","W"],"EQUATION":"F1 * sin(alpha) + F2 * sin(alpha) = W","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A10a": {"TPK":{"DOF":[{"NAME":"u","DIMENSION":"TH1"},{"NAME":"X","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"alpha_d","DIMENSION":"L2 T-1"},{"NAME":"L_rod","DIMENSION":"L1"}],"LAW":[{"NAME":"HEAT","STATEMENT":"du/dt = alpha d2u/dX2","REFS":["u","t","alpha_d","X"],"EQUATION":"D(u, t) = alpha_d * D(u, X, 2)","ROLE":"EOM(u)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A10b": {"TPK":{"DOF":[{"NAME":"u","DIMENSION":"TH1"},{"NAME":"X","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"alpha_d","DIMENSION":"L2 T-1"},{"NAME":"L_rod","DIMENSION":"L1"}],"LAW":[{"NAME":"HEAT","STATEMENT":"du/dt = alpha d2u/dX2","REFS":["u","t","alpha_d","X"],"ROLE":"EOM(u)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A11a": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"q","DIMENSION":"I1 T1"},{"NAME":"E_x","DIMENSION":"M1 L1 T-3 I-1","VALUE":"1000","UNIT":"V m-1"},{"NAME":"B_z","DIMENSION":"M1 T-2 I-1","VALUE":"0.01","UNIT":"T"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"LX","STATEMENT":"m dvx/dt = q (E_x + vy B_z)","REFS":["m","vx","t","q","E_x","vy","B_z"],"EQUATION":"m * D(vx, t) = q * (E_x + vy * B_z)","ROLE":"EOM(vx)"},{"NAME":"LY","STATEMENT":"m dvy/dt = -q vx B_z","REFS":["m","vy","t","q","vx","B_z"],"EQUATION":"m * D(vy, t) = -q * vx * B_z","ROLE":"EOM(vy)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A11b": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"q","DIMENSION":"I1 T1"},{"NAME":"E_x","DIMENSION":"M1 L1 T-3 I-1","VALUE":"1000","UNIT":"V m-1"},{"NAME":"B_z","DIMENSION":"M1 T-2 I-1","VALUE":"0.01","UNIT":"T"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"LX","STATEMENT":"m dvx/dt = q (E_x + vy B_z)","REFS":["m","vx","t","q","E_x","vy","B_z"],"EQUATION":"m * D(vx, t) = q * (E_x + vy * B_z)","ROLE":"EOM(vx)"},{"NAME":"LY","STATEMENT":"m dvy/dt = -q vx B_z","REFS":["m","vy","t","q","vx","B_z"],"EQUATION":"m * D(vy, t) = -q * vx * B_z","ROLE":"EOM(vy)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A12": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A13": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"E_0","DIMENSION":"M1 L2 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EN","STATEMENT":"m v^2 / 2 + k_s x^2 / 2 = E_0","REFS":["m","v","k_s","x","E_0"],"EQUATION":"0.5 * m * v^2 + 0.5 * k_s * x^2 = E_0","ROLE":"INVARIANT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A13_en_constraint": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"E_0","DIMENSION":"M1 L2 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EN","STATEMENT":"m v^2 / 2 + k_s x^2 / 2 = E_0","REFS":["m","v","k_s","x","E_0"],"EQUATION":"0.5 * m * v^2 + 0.5 * k_s * x^2 = E_0","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A14": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"c_d","DIMENSION":"M1 T-1"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"N2D","STATEMENT":"m dv/dt = -k_s x - c_d v","REFS":["m","v","k_s","x","t","c_d"],"EQUATION":"m * D(v, t) = -k_s * x - c_d * v","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A15": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s y - m g","REFS":["m","v","k_s","y","t"],"ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A16": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s y - m g","REFS":["m","v","k_s","y","t"],"EQUATION":"m * D(v, t) = -k_s * y - m * g","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A16b": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s y - m g","REFS":["m","v","k_s","y","t","g"],"EQUATION":"m * D(v, t) = -k_s * y - m * g","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A17a": {"TPK":{"DOF":[{"NAME":"h","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"m_r","DIMENSION":"M1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"u_e","DIMENSION":"L1 T-1"},{"NAME":"mdot","DIMENSION":"M1 T-1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"KIN","STATEMENT":"dh/dt = v","REFS":["h","v","t"],"EQUATION":"D(h, t) = v","ROLE":"EOM(h)"},{"NAME":"BURN","STATEMENT":"dm/dt = -mdot","REFS":["m_r","t","mdot"],"EQUATION":"D(m_r, t) = -mdot","ROLE":"EOM(m_r)"},{"NAME":"THRUST","STATEMENT":"m dv/dt = u_e mdot - m g_n","REFS":["m_r","v","t","u_e","mdot","g_n"],"EQUATION":"m_r * D(v, t) = u_e * mdot - m_r * g_n","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A17b": {"TPK":{"DOF":[{"NAME":"h","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"m_r","DIMENSION":"M1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"mdot","DIMENSION":"M1 T-1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"KIN","STATEMENT":"dh/dt = v","REFS":["h","v","t"],"EQUATION":"D(h, t) = v","ROLE":"EOM(h)"},{"NAME":"BURN","STATEMENT":"dm/dt = -mdot","REFS":["m_r","t","mdot"],"EQUATION":"D(m_r, t) = -mdot","ROLE":"EOM(m_r)"},{"NAME":"THRUST","STATEMENT":"d(m v)/dt = -m g_n","REFS":["m_r","v","t","g_n"],"EQUATION":"m_r * D(v, t) + v * D(m_r, t) = -m_r * g_n","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A18": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"e_r","DIMENSION":"1","VALUE":"0.8","UNIT":"1"}],"LAW":[{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"},{"NAME":"FALL","STATEMENT":"dv/dt = -g_n","REFS":["v","t","g_n"],"EQUATION":"D(v, t) = -g_n","ROLE":"EOM(v)"},{"NAME":"IMPACT","STATEMENT":"when y reaches 0 with v < 0, v is replaced by -e_r v","REFS":["y","v","e_r"],"ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A19": {"TPK":{"DOF":[{"NAME":"w1","DIMENSION":"T-1"},{"NAME":"w2","DIMENSION":"T-1"},{"NAME":"w3","DIMENSION":"T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"I1","DIMENSION":"M1 L2"},{"NAME":"I2","DIMENSION":"M1 L2"},{"NAME":"I3","DIMENSION":"M1 L2"}],"LAW":[{"NAME":"E1","STATEMENT":"I1 dw1/dt = (I2 - I3) w2 w3","REFS":["I1","w1","t","I2","I3","w2","w3"],"EQUATION":"I1 * D(w1, t) = (I2 - I3) * w2 * w3","ROLE":"EOM(w1)"},{"NAME":"E2","STATEMENT":"I2 dw2/dt = (I3 - I1) w3 w1","REFS":["I1","w1","t","I2","I3","w2","w3"],"EQUATION":"I2 * D(w2, t) = (I3 - I1) * w3 * w1","ROLE":"EOM(w2)"},{"NAME":"E3","STATEMENT":"I3 dw3/dt = (I1 - I2) w1 w2","REFS":["I1","w1","t","I2","I3","w2","w3"],"EQUATION":"I3 * D(w3, t) = (I1 - I2) * w1 * w2","ROLE":"EOM(w3)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A20": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"xi","DIMENSION":"M1 L1 T-2","ROLE":"INPUT"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"gamma_d","DIMENSION":"M1 T-1"},{"NAME":"k_B","DIMENSION":"M1 L2 T-2 TH-1"},{"NAME":"T_b","DIMENSION":"TH1"}],"LAW":[{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2","STATEMENT":"m dv/dt = -gamma v + xi","REFS":["m","v","t","gamma_d","xi"],"EQUATION":"m * D(v, t) = -gamma_d * v + xi","ROLE":"EOM(v)"},{"NAME":"NOISE","STATEMENT":"xi is Gaussian white noise, <xi(t) xi(s)> = 2 gamma k_B T delta(t - s)","REFS":["xi","gamma_d","k_B","T_b"],"ROLE":"CONSTITUTIVE"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A20_no_input": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"xi","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"gamma_d","DIMENSION":"M1 T-1"},{"NAME":"k_B","DIMENSION":"M1 L2 T-2 TH-1"},{"NAME":"T_b","DIMENSION":"TH1"}],"LAW":[{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2","STATEMENT":"m dv/dt = -gamma v + xi","REFS":["m","v","t","gamma_d","xi"],"EQUATION":"m * D(v, t) = -gamma_d * v + xi","ROLE":"EOM(v)"},{"NAME":"NOISE","STATEMENT":"xi is Gaussian white noise, <xi(t) xi(s)> = 2 gamma k_B T delta(t - s)","REFS":["xi","gamma_d","k_B","T_b"],"ROLE":"CONSTITUTIVE"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A21": {"TPK":{"DOF":[{"NAME":"X","DIMENSION":"1"},{"NAME":"V","DIMENSION":"1"},{"NAME":"tau","DIMENSION":"1"}],"LAW":[{"NAME":"KIN","STATEMENT":"dX/dtau = V","REFS":["X","V","tau"],"EQUATION":"D(X, tau) = V","ROLE":"EOM(X)"},{"NAME":"N2","STATEMENT":"dV/dtau = -X","REFS":["X","V","tau"],"EQUATION":"D(V, tau) = -X","ROLE":"EOM(V)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A22": {"TPK":{"DOF":[{"NAME":"a_r","DIMENSION":"1"},{"NAME":"a_i","DIMENSION":"1"},{"NAME":"b_r","DIMENSION":"1"},{"NAME":"b_i","DIMENSION":"1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"Om","DIMENSION":"T-1"}],"LAW":[{"NAME":"S1","STATEMENT":"d a_r/dt = (Om/2) b_i","REFS":["a_r","t","Om","b_i"],"EQUATION":"D(a_r, t) = 0.5 * Om * b_i","ROLE":"EOM(a_r)"},{"NAME":"S2","STATEMENT":"d a_i/dt = -(Om/2) b_r","REFS":["a_i","t","Om","b_r"],"EQUATION":"D(a_i, t) = -0.5 * Om * b_r","ROLE":"EOM(a_i)"},{"NAME":"S3","STATEMENT":"d b_r/dt = (Om/2) a_i","REFS":["b_r","t","Om","a_i"],"EQUATION":"D(b_r, t) = 0.5 * Om * a_i","ROLE":"EOM(b_r)"},{"NAME":"S4","STATEMENT":"d b_i/dt = -(Om/2) a_r","REFS":["b_i","t","Om","a_r"],"EQUATION":"D(b_i, t) = -0.5 * Om * a_r","ROLE":"EOM(b_i)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A23": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"a_r","DIMENSION":"T-1"},{"NAME":"tau_d","DIMENSION":"T1"}],"LAW":[{"NAME":"DDE","STATEMENT":"dx/dt = -a_r x(t - tau_d)","REFS":["x","t","a_r","tau_d"],"ROLE":"EOM(x)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A24": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"},{"NAME":"vx","DIMENSION":"L1 T-1"},{"NAME":"vy","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"Om_f","DIMENSION":"T-1"}],"LAW":[{"NAME":"KX","STATEMENT":"dx/dt = vx","REFS":["x","vx","t"],"EQUATION":"D(x, t) = vx","ROLE":"EOM(x)"},{"NAME":"KY","STATEMENT":"dy/dt = vy","REFS":["y","vy","t"],"EQUATION":"D(y, t) = vy","ROLE":"EOM(y)"},{"NAME":"RX","STATEMENT":"dvx/dt = 2 Om vy + Om^2 x","REFS":["vx","t","Om_f","vy","x"],"EQUATION":"D(vx, t) = 2 * Om_f * vy + Om_f^2 * x","ROLE":"EOM(vx)"},{"NAME":"RY","STATEMENT":"dvy/dt = -2 Om vx + Om^2 y","REFS":["vy","t","Om_f","vx","y"],"EQUATION":"D(vy, t) = -2 * Om_f * vx + Om_f^2 * y","ROLE":"EOM(vy)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A25": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_0","DIMENSION":"L1","VALUE":"0.01","UNIT":"m"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"IC","STATEMENT":"x(0) = x_0","REFS":["x","x_0"],"EQUATION":"x = x_0","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A26": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"w","DIMENSION":"T-1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A27a": {"TPK":{"DOF":[{"NAME":"a","DIMENSION":"L1"},{"NAME":"b","DIMENSION":"L1"},{"NAME":"c","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"L_0","DIMENSION":"L1"},{"NAME":"L_1","DIMENSION":"L1"},{"NAME":"L_2","DIMENSION":"L1"}],"LAW":[{"NAME":"P1","STATEMENT":"a + b + c = L_0","REFS":["a","b","c","L_0"],"EQUATION":"a + b + c = L_0","ROLE":"CONSTRAINT"},{"NAME":"P2","STATEMENT":"a = L_1","REFS":["a","L_1"],"EQUATION":"a = L_1","ROLE":"CONSTRAINT"},{"NAME":"P3","STATEMENT":"2 a = L_2","REFS":["a","L_2"],"EQUATION":"2 * a = L_2","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A27b": {"TPK":{"DOF":[{"NAME":"a","DIMENSION":"L1"},{"NAME":"b","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"L_0","DIMENSION":"L1"},{"NAME":"L_1","DIMENSION":"L1"}],"LAW":[{"NAME":"P1","STATEMENT":"a + b = L_0","REFS":["a","b","L_0"],"EQUATION":"a + b = L_0","ROLE":"CONSTRAINT"},{"NAME":"P2","STATEMENT":"2 a + 2 b = L_1","REFS":["a","b","L_1"],"EQUATION":"2 * a + 2 * b = L_1","ROLE":"CONSTRAINT"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A28": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x"],"ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v"],"ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z"],"ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"A29": {"TPK":{"DOF":[{"NAME":"y","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"R_s","DIMENSION":"L1"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"},{"NAME":"mu_air","DIMENSION":"M1 L-1 T-1","VALUE":"1.7894e-5","UNIT":"Pa s"},{"NAME":"pi_c","DIMENSION":"1","VALUE":"3.14159265358979","UNIT":"1"}],"LAW":[{"NAME":"KIN","STATEMENT":"dy/dt = v","REFS":["y","v","t"],"EQUATION":"D(y, t) = v","ROLE":"EOM(y)"},{"NAME":"N2","STATEMENT":"m dv/dt = -m g_n - 6 pi mu R v","REFS":["m","v","t","g_n","pi_c","mu_air","R_s"],"EQUATION":"m * D(v, t) = -m * g_n - 6 * pi_c * mu_air * R_s * v","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g1": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = -g_n","REFS":["z","t","g_n"],"EQUATION":"D(z, t, 2) = -g_n","ROLE":"EOM(z)"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g2": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"EOM(z)"},{"NAME":"GRAV_Z","STATEMENT":"d2z/dt2 = -g_n","REFS":["z","t","g_n"],"EQUATION":"D(z, t, 2) = -g_n","ROLE":"EOM(z)"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g2b": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"EOM(z)"},{"NAME":"GRAV_Z","STATEMENT":"d2z/dt2 = -g_n","REFS":["z","t","g_n"],"EQUATION":"D(z, t, 2) = -g_n","ROLE":"EOM(z)"}],"CONSTRAINT":[]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g2c": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"EOM(z)"},{"NAME":"GRAV_Z","STATEMENT":"m d2z/dt2 = -m g_n","REFS":["z","t","g_n","m"],"EQUATION":"m * D(z, t, 2) = -m * g_n","ROLE":"EOM(z)"}],"CONSTRAINT":[]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g3": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"N_z","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2_Z","STATEMENT":"m d2z/dt2 = N_z - m g_n","REFS":["z","t","g_n","m","N_z"],"EQUATION":"m * D(z, t, 2) = N_z - m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g3b": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"},{"NAME":"N_z","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2_Z","STATEMENT":"m d2z/dt2 = N_z - m g_n","REFS":["z","t","g_n","m","N_z"],"EQUATION":"m * D(z, t, 2) = N_z - m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g4": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"},{"NAME":"C_d","DIMENSION":"1"},{"NAME":"A_ref","DIMENSION":"L2"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x - (1/2) rho_air C_d A_ref |v| v","REFS":["m","v","k_s","x","t","rho_air","C_d","A_ref"],"EQUATION":"m * D(v, t) = -k_s * x - 0.5 * rho_air * C_d * A_ref * abs(v) * v","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g5": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"rho_air","DIMENSION":"M1 L-3","VALUE":"1.225","UNIT":"kg m-3"},{"NAME":"C_d","DIMENSION":"1"},{"NAME":"A_ref","DIMENSION":"L1"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x - (1/2) rho_air C_d A_ref |v| v","REFS":["m","v","k_s","x","t","rho_air","C_d","A_ref"],"EQUATION":"m * D(v, t) = -k_s * x - 0.5 * rho_air * C_d * A_ref * abs(v) * v","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = 0","REFS":["z","t"],"EQUATION":"D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"g6": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"FREE_Z","STATEMENT":"d2z/dt2 = -g (gravity)","REFS":["z","t"],"ROLE":"EOM(z)"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"motion confined to z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_draft": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"ASSUMPTION":[{"NAME":"A_kpos","PROPOSITION":"k_s is positive","REFS":["k_s"]},{"NAME":"A_mpos","PROPOSITION":"m is positive","REFS":["m"]}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}],"BOUNDARY":[{"NAME":"B_small","PREDICATE":"|x| < x_max","REFS":["x","x_max"],"CONDITION":"abs(x) < x_max"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_draft_eomz": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"EOM(z)"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_gravity_unbound": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = -m g_n","REFS":["m","z","t","g_n"],"EQUATION":"m * D(z, t, 2) = -m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_ic2_gap": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"y","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"},{"NAME":"EOM_Y","STATEMENT":"m d2y/dt2 = 0","REFS":["m","y","t"],"EQUATION":"m * D(y, t, 2) = 0","ROLE":"EOM(y)"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_mistakes_final": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"},{"NAME":"C_OFF","TARGET":"z","ACTION":"FIX","VALUE":"2","UNIT":"cm","STATEMENT":"only motion on the line z = 2 cm is described"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_mistakes_gravity": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"d2z/dt2 = -g_n","REFS":["z","t","g_n"],"EQUATION":"D(z, t, 2) = -g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_mistakes_tpk": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"LT-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"s","STATEMENT":"only motion on the spring axis is described: z = 0"}]}},
"spring_respelled": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"T-1 L1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"5e-2","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m*D(v,t)=-k_s*x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t, 1) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m1","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_succ_damped": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"c_d","DIMENSION":"M1 T-1"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x - c_d v","REFS":["m","v","k_s","x","t","c_d"],"EQUATION":"m * D(v, t) = -k_s * x - c_d * v","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"spring_track_draft": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"F_n","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = F_n - m g_n","REFS":["m","z","t","F_n","g_n"],"EQUATION":"m * D(z, t, 2) = F_n - m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"corner_coulomb": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"},{"NAME":"F_n","DIMENSION":"M1 L1 T-2"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"g_n","DIMENSION":"L1 T-2","VALUE":"9.80665","UNIT":"m s-2"},{"NAME":"mu_k","DIMENSION":"1"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x - mu_k F_n v/|v|","REFS":["m","v","k_s","x","t","mu_k","F_n"],"EQUATION":"m * D(v, t) = -k_s * x - mu_k * F_n * v / abs(v)","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = F_n - m g_n","REFS":["m","z","t","F_n","g_n"],"EQUATION":"m * D(z, t, 2) = F_n - m * g_n","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"corner_fix_t": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"EOM_X","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"},{"NAME":"C_T","TARGET":"t","ACTION":"FIX","VALUE":"0","UNIT":"s","STATEMENT":"t = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"corner_no_eom_x": {"TPK":{"DOF":[{"NAME":"t","DIMENSION":"T1"},{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"z","DIMENSION":"L1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"EOM_Z","STATEMENT":"m d2z/dt2 = 0","REFS":["m","z","t"],"EQUATION":"m * D(z, t, 2) = 0","ROLE":"CONSTRAINT"}],"CONSTRAINT":[{"NAME":"C_NOZ","TARGET":"z","ACTION":"FIX","VALUE":"0","UNIT":"m","STATEMENT":"only motion on the spring axis is described: z = 0"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"E01": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"ACTION","STATEMENT":"the action, the time integral of m v^2 / 2 - k_s x^2 / 2, is stationary under variations of x with fixed end points","REFS":["m","v","k_s","x","t"],"ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"E02": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"},{"NAME":"w0","DIMENSION":"T-1"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"W0DEF","STATEMENT":"k_s = m w0^2","REFS":["k_s","m","w0"],"EQUATION":"k_s = m * w0^2","ROLE":"DEFINITION"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"E03": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2B","STATEMENT":"dv/dt = -k_s x / m","REFS":["v","k_s","x","m","t"],"EQUATION":"D(v, t) = -k_s * x / m","ROLE":"EOM(v)"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
"E03_shape": {"TPK":{"DOF":[{"NAME":"x","DIMENSION":"L1"},{"NAME":"v","DIMENSION":"L1 T-1"},{"NAME":"t","DIMENSION":"T1"}],"CONSTANT":[{"NAME":"m","DIMENSION":"M1"},{"NAME":"k_s","DIMENSION":"M1 T-2"},{"NAME":"x_max","DIMENSION":"L1","VALUE":"0.05","UNIT":"m","UNCERTAINTY":"0.001"}],"LAW":[{"NAME":"N2","STATEMENT":"m dv/dt = -k_s x","REFS":["m","v","k_s","x","t"],"EQUATION":"m * D(v, t) = -k_s * x","ROLE":"EOM(v)"},{"NAME":"KIN","STATEMENT":"dx/dt = v","REFS":["x","v","t"],"EQUATION":"D(x, t) = v","ROLE":"EOM(x)"},{"NAME":"N2B","STATEMENT":"dv/dt = -k_s x / m","REFS":["v","k_s","x","m","t"],"EQUATION":"D(v, t) = -k_s * x / m","ROLE":"CONSTITUTIVE"}]},"TMS":{"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10}}},
}
SPRING_TRM = {"HEADER":{"ENVIRONMENT_INVENTORY":[{"ENVIRONMENT_QUANTITY":"time","DIMENSION":"T1"},{"ENVIRONMENT_QUANTITY":"position","DIMENSION":"L1"},{"ENVIRONMENT_QUANTITY":"velocity","DIMENSION":"L1 T-1"},{"ENVIRONMENT_QUANTITY":"transverse_position","DIMENSION":"L1"}],"SIGNATURE":[{"NAME":"time_derivative","OVER":["x","v","t"],"IMAGE":"d/dt maps position to velocity","FORM":"D(x, t) = v","IMAGE_FORM":"D(position, time) = velocity"}],"TRANSFORMATIONS":[{"NAME":"time_translation","STATEMENT":"t -> t + t0"}]},"ENTRIES":[{"NAME":"E_t","DOF":"t","DOMAIN":"always","ENVIRONMENT_QUANTITY":"time","IDENTIFICATION":"t is the reading of a laboratory clock from an arbitrary origin","FALSIFIER":"a second clock whose readings differ from t by more than a constant offset beyond the stated uncertainty","FALSIFIER_CLASS":"F3","BEARS":[],"DIMENSION":"T1"},{"NAME":"E_x","DOF":"x","DOMAIN":"|x| < x_max","ENVIRONMENT_QUANTITY":"position","IDENTIFICATION":"x is the displacement of the mass along the spring axis from the point where the spring exerts no force","FALSIFIER":"a measured spring force not proportional to x inside the domain","FALSIFIER_CLASS":"F3","BEARS":["EOM_X","KIN"],"DIMENSION":"L1"},{"NAME":"E_v","DOF":"v","DOMAIN":"|x| < x_max","ENVIRONMENT_QUANTITY":"velocity","IDENTIFICATION":"v is the rate of change of x with t","FALSIFIER":"a measured velocity that differs from the rate of change of the measured x beyond uncertainty","FALSIFIER_CLASS":"F2","BEARS":["KIN"],"DIMENSION":"L1 T-1"},{"NAME":"E_z","DOF":"z","DOMAIN":"always","ENVIRONMENT_QUANTITY":"transverse_position","IDENTIFICATION":"z is the displacement of the mass perpendicular to the spring axis","FALSIFIER":"a measured z different from 0 beyond its uncertainty","FALSIFIER_CLASS":"F3","BEARS":["EOM_Z","C_NOZ"],"DIMENSION":"L1"}]}
SPRING_TMS = {"PARAMETERS":{"STEP_CONVENTION":"one application of an inference rule or algebraic identity is one step","K":"2","N_X":2,"S_MAX":10},"CONSTANTS":[{"NAME":"w_a","VALUE":"1"},{"NAME":"w_s","VALUE":"0.5"}],"YARDSTICKS":[{"NAME":"combined_distance","KEY":["SR1","WSUM:w_a*A;w_s*S","S"],"LIMITING":[]}]}
# Cross-check (agent R4, increment 10 partial 0.4.0): a kernel whose forms use two or more D
# variables declares D_VARIABLES SEVERAL, or T1 refuses it (D177.1); A10a, the research draft,
# predates the switch. tpc_eom reads no D_VARIABLES (RD-R2-2), so no answer moves.
FIXTURES["A10a"]["TPK"] = dict([("PARAMETERS", {"D_VARIABLES": "SEVERAL"})] + list(FIXTURES["A10a"]["TPK"].items()))
STD_PARAMS = {"STEP_CONVENTION": "one application of an inference rule or algebraic identity is one step",
"K": "2", "N_X": 2, "S_MAX": 10}
cases = []
_ids = set()
def case(cid, fn, inp, hand=None, note=None):
"""hand: a literal expectation (str), or ("HAS", [substrings]) the
oracle's literal must hold, or None."""
cid = "eom/" + cid
assert cid not in _ids, cid
_ids.add(cid)
cs = {"id": cid, "fn": fn, "input": inp}
if note:
cs["note"] = note
cases.append((cs, hand))
def c(o):
return copy.deepcopy(o)
def R(reason):
return "[REFUSED," + reason + "]"
def HAS(*subs):
return ("HAS", list(subs))
REG = "[STRUCTURE,structurally regular]"
def NV(*reasons):
return "[STRUCTURE,Structure not Validated at Inception,[" + ",".join(reasons) + "]]"
def K(dofs, consts, laws, cons=(), tpk_params=None, sc=None):
"""A synthetic TFK in the schema 0.5.0 shape. dofs: "x:L1" or
"xi:M1 L1 T-2:INPUT"; consts: "m:M1" or "g_n:L1 T-2=9.80665 m s-2";
laws: (NAME, ROLE, EQUATION) or (NAME, ROLE, None, [REFS]); cons:
(NAME, "FIX", TARGET, VALUE, UNIT) or (NAME, "REMOVE", TARGET)."""
tpk = {}
if tpk_params is not None:
tpk["PARAMETERS"] = tpk_params
tpk["DOF"] = []
for d in dofs:
p = d.split(":")
e = {"NAME": p[0], "DIMENSION": p[1]}
if len(p) > 2:
e["ROLE"] = p[2]
tpk["DOF"].append(e)
tpk["CONSTANT"] = []
for s in consts:
n, rest = s.split(":", 1)
if "=" in rest:
dim, vu = rest.split("=")
v, u = vu.split(" ", 1)
tpk["CONSTANT"].append({"NAME": n, "DIMENSION": dim, "VALUE": v, "UNIT": u})
else:
tpk["CONSTANT"].append({"NAME": n, "DIMENSION": rest})
tpk["LAW"] = []
for l in laws:
if l[2] is None:
tpk["LAW"].append({"NAME": l[0], "STATEMENT": "stated in prose", "REFS": list(l[3]), "ROLE": l[1]})
else:
r = F.form_names(l[2], "equation")
refs = r[1] if r[0] == "OK" else []
tpk["LAW"].append({"NAME": l[0], "STATEMENT": l[2], "REFS": refs, "ROLE": l[1], "EQUATION": l[2]})
if cons:
tpk["CONSTRAINT"] = []
for cn in cons:
e = {"NAME": cn[0], "TARGET": cn[2], "ACTION": cn[1], "STATEMENT": "a constraint"}
if cn[1] == "FIX":
e["VALUE"], e["UNIT"] = cn[3], cn[4]
tpk["CONSTRAINT"].append(e)
params = dict(STD_PARAMS)
if sc is not None:
params["STRUCTURE_CHECK"] = sc
return {"TPK": tpk, "TMS": {"PARAMETERS": params}}
def with_sc(tfk, sc):
t = c(tfk)
t["TMS"]["PARAMETERS"]["STRUCTURE_CHECK"] = sc
return t
def MAP(cid, tfk, hand=None, note=None):
case("map/" + cid, "eom_map", {"tfk": tfk}, hand, note)
def FND(cid, tfk, hand=None, note=None):
case("findings/" + cid, "eom_findings", {"tfk": tfk}, hand, note)
def CLS(cid, tfk, hand, note=None):
case("class/" + cid, "eom_class", {"tfk": tfk}, hand, note)
def REGT(cid, tfk, records, hand=None, note=None):
case("register/" + cid, "eom_register_test", {"tfk": tfk, "records": records}, hand, note)
SPRING = c(FIXTURES["spring_draft"])
SPRING["TrM"] = c(SPRING_TRM)
SPRING["TMS"] = c(SPRING_TMS)
X = FIXTURES
# ==== A: the research drafts, each with its ROLEs ======================================
REFUSED_FIX = {
"A16": "LAW:N2: EQUATION names g, which is not a DOF or CONSTANT",
"A16b": "LAW:N2: EQUATION names g, which is not a DOF or CONSTANT",
"spring_mistakes_tpk": "CONSTANT:x max: NAME x max is not an identifier",
}
CLASS_OF = {
"A01": REG, "A02": REG, "A03a": REG, "A03b": REG, "A03c": NV("FINDINGS"), "A03c_eomz": NV("FINDINGS"),
"A04a": REG, "A04b": REG, "A05": REG, "A06": REG, "A07": REG, "A08": REG, "A09": REG,
"A10a": NV("PDE"), "A10b": NV("PROSE", "NO FORM"), "A11a": REG, "A11b": REG, "A12": NV("FINDINGS"),
"A13": REG, "A13_en_constraint": NV("FINDINGS"), "A14": NV("FINDINGS"), "A15": NV("FINDINGS", "PROSE"),
"A17a": REG, "A17b": REG, "A18": NV("PROSE"), "A19": REG, "A20": REG,
"A20_no_input": NV("FINDINGS", "PROSE"), "A21": REG, "A22": REG, "A23": NV("PROSE", "NO FORM"),
"A24": REG, "A25": NV("FINDINGS"), "A26": NV("FINDINGS"), "A27a": NV("FINDINGS"), "A27b": REG,
"A28": NV("PROSE", "NO FORM"), "A29": REG,
"g1": NV("FINDINGS"), "g2": NV("FINDINGS"), "g2b": NV("FINDINGS"), "g2c": NV("FINDINGS"), "g3": REG,
"g3b": REG, "g4": REG, "g5": REG, "g6": NV("FINDINGS"),
"spring_draft": REG, "spring_draft_eomz": NV("FINDINGS"), "spring_gravity_unbound": NV("FINDINGS"),
"spring_ic2_gap": REG, "spring_mistakes_final": REG, "spring_mistakes_gravity": REG,
"spring_respelled": REG, "spring_succ_damped": REG, "spring_track_draft": REG, "corner_coulomb": REG,
"corner_fix_t": REG, "corner_no_eom_x": NV("FINDINGS"), "E01": NV("FINDINGS", "PROSE"),
"E02": NV("FINDINGS"), "E03": NV("FINDINGS"), "E03_shape": NV("FINDINGS"),
}
# the findings each draft must list (class and subject), hand-derived; "" = none
FIND_OF = {
"A03c": ["[CLOSED,N2Z,[m],"], "A03c_eomz": ["[CLOSED,N2Z,[m],", "[ROLE MISMATCH,N2Z,z,KNOWN,"],
"A10a": ["[PDE,[X,t],PDE: not analyzed]"], "A10b": ["[PROSE,HEAT,[X,t,u],", "[NO FORM,[X,t,u],"],
"A12": ["[UNDER,x,[v,x],[N2],"], "A13_en_constraint": ["[OVER,[EN,KIN,N2],[v,x],"],
"A14": ["[OVER-EOM,v,[N2,N2D],"], "A15": ["[UNDER,v,[v,y],[KIN],", "[PROSE,N2,[v,y],"],
"A18": ["[PROSE,IMPACT,[v,y],"], "A20_no_input": ["[UNDER,xi,", "[PROSE,NOISE,[xi],"],
"A23": ["[PROSE,DDE,[t,x],", "[NO FORM,[t,x],"], "A25": ["[OVER,[IC,KIN,N2],[v,x],"],
"A26": ["[UNDER,w,[w],[],"], "A27a": ["[UNDER,c,[b,c],[P1],", "[OVER,[P2,P3],[a],"],
"A28": ["[PROSE,KIN,[v,x],", "[PROSE,N2,[v,x],", "[NO FORM,[v,x],"],
"g1": ["[ROLE MISMATCH,FREE_Z,z,KNOWN,"],
"g2": ["[OVER-EOM,z,[FREE_Z,GRAV_Z],", "[ROLE MISMATCH,FREE_Z,z,KNOWN,", "[ROLE MISMATCH,GRAV_Z,z,KNOWN,"],
"g2b": ["[OVER-EOM,z,[FREE_Z,GRAV_Z],"], "g2c": ["[OVER-EOM,z,[FREE_Z,GRAV_Z],"],
"g6": ["[ROLE MISMATCH,FREE_Z,z,KNOWN,"], "spring_draft_eomz": ["[ROLE MISMATCH,EOM_Z,z,KNOWN,"],
"spring_gravity_unbound": ["[CLOSED,EOM_Z,[m],"], "corner_no_eom_x": ["[UNDER,v,[v,x],[KIN],"],
"E01": ["[UNDER,v,[v,x],[KIN],", "[PROSE,ACTION,[v,x],"], "E02": ["[CLOSED,W0DEF,[k_s,m,w0],"],
"E03": ["[OVER-EOM,v,[N2,N2B],"], "E03_shape": ["[OVER-EOM,v,[N2,N2B],"],
}
MAP_OF = {
"A07": ["[INDEX,3]", "[INITIAL_VALUES,2]", "[lam,DETERMINED,NX]", "[t,INDEPENDENT,]"],
"A09": ["[INDEX,1]", "[INITIAL_VALUES,0]", "[D_VARIABLES,[]]"],
"A01": ["[INDEX,0]", "[INITIAL_VALUES,2]", "[z,FIXED,]", "[CLOSED,[[FREE_Z,ZERO]]]"],
"A03b": ["[N_z,DETERMINED,N2Z]", "[INDEX,1]"], "A03c": ["[CLOSED,[[N2Z,UNBOUND]]]"],
"A10a": ["[ANALYSIS,PDE]", "[D_VARIABLES,[X,t]]", "[u,NOT ANALYZED,]", "[INDEX,NONE]"],
"A10b": ["[ANALYSIS,NO FORM]", "[u,NO LAW,]", "[PROSE,[[HEAT,[X,t,u]]]]"],
"A12": ["[x,NO LAW,]", "[v,UNDER,N2]", "[PARTS,[UNDER,[v,x],[N2]]"],
"A13": ["[INVARIANT,[EN]]", "[INDEX,0]", "[INITIAL_VALUES,2]"],
"A17a": ["[INITIAL_VALUES,3]"], "A20": ["[xi,INPUT,]", "[INITIAL_VALUES,2]"],
"A20_no_input": ["[xi,NO LAW,]"], "A21": ["[tau,INDEPENDENT,]", "[D_VARIABLES,[tau]]"],
"A25": ["[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[IC,KIN,N2]]]"],
"A26": ["[w,NO LAW,]"], "A27a": ["[a,OVER,P2]", "[b,UNDER,P1]", "[c,NO LAW,]"],
"A28": ["[ANALYSIS,NO FORM]", "[z,FIXED,]"], "g2": ["[CLOSED,[[FREE_Z,ZERO],[GRAV_Z,BOUND]]]"],
"spring_draft": ["[x,DETERMINED,KIN]", "[v,DETERMINED,EOM_X]", "[CLOSED,[[EOM_Z,ZERO]]]"],
"spring_ic2_gap": ["[y,DETERMINED,EOM_Y]", "[INITIAL_VALUES,4]"],
"spring_track_draft": ["[F_n,DETERMINED,EOM_Z]"], "corner_fix_t": ["[t,FIXED,]"],
"E01": ["[PROSE,[[ACTION,[v,x]]]]", "[v,NO LAW,]"], "E02": ["[CLOSED,[[W0DEF,UNBOUND]]]"],
}
MAPSET = ["A01", "A03b", "A03c", "A07", "A09", "A10a", "A10b", "A12", "A13", "A14", "A15", "A17a", "A18",
"A20", "A20_no_input", "A21", "A23", "A25", "A26", "A27a", "A28", "g2", "g2c", "g6",
"spring_draft", "spring_draft_eomz", "spring_gravity_unbound", "spring_ic2_gap",
"spring_mistakes_final", "spring_track_draft", "corner_coulomb", "corner_fix_t",
"corner_no_eom_x", "E01", "E02", "E03", "E03_shape"]
for fid in FIXTURES:
tfk = SPRING if fid == "spring_draft" else X[fid]
if fid in REFUSED_FIX:
MAP(fid, tfk, R(REFUSED_FIX[fid]))
FND(fid, tfk, R(REFUSED_FIX[fid]))
if "TMS" in tfk:
CLS(fid, tfk, R(REFUSED_FIX[fid]))
else:
CLS(fid, tfk, R("TMS: zone is not an object"), note="the TMS is read before the TPK")
continue
FND(fid, tfk, HAS(*FIND_OF[fid]) if fid in FIND_OF else "[OK,[]]")
CLS(fid, tfk, CLASS_OF[fid])
if fid in MAPSET:
MAP(fid, tfk, HAS(*MAP_OF[fid]) if fid in MAP_OF else None)
assert set(CLASS_OF) | set(REFUSED_FIX) == set(FIXTURES)
# ==== B: the switch (STRUCTURE_CHECK, a TMS parameter; absent = ON) ===================
CLS("switch/on-explicit", with_sc(SPRING, "ON"), REG)
CLS("switch/off-regular-kernel", with_sc(SPRING, "OFF"), NV("CHECK OFF"))
CLS("switch/off-under-kernel", with_sc(X["A12"], "OFF"), NV("CHECK OFF"), note="CHECK OFF alone")
CLS("switch/off-pde-kernel", with_sc(X["A10a"], "OFF"), NV("CHECK OFF"))
CLS("switch/off-noform-kernel", with_sc(X["A28"], "OFF"), NV("CHECK OFF"))
t = with_sc(SPRING, "OFF"); t["TPK"] = "not a zone"
CLS("switch/off-tpk-not-read", t, NV("CHECK OFF"), note="under OFF the TPK is not read")
t = with_sc(SPRING, "ON"); t["TPK"] = "not a zone"
CLS("switch/on-tpk-read", t, R("TPK: zone is not an object"))
for tag, v, why in [("lower", "on", "TMS: STRUCTURE_CHECK on is not ON or OFF"),
("empty", "", "TMS: STRUCTURE_CHECK is not ON or OFF"),
("space", "OFF ", "TMS: STRUCTURE_CHECK OFF is not ON or OFF"),
("integer", 1, "TMS: field STRUCTURE_CHECK has the wrong type"),
("list", ["OFF"], "TMS: field STRUCTURE_CHECK has the wrong type")]:
CLS("switch/bad-" + tag, with_sc(SPRING, v), R(why))
t = with_sc(SPRING, "OF\u202eF")
CLS("switch/bad-bidi", t, R("TMS: STRUCTURE_CHECK OF<U+202E>F is not ON or OFF"))
t = c(SPRING); t["TMS"]["PARAMETERS"]["STRUCTURE_CHECK"] = None
CLS("switch/bad-null", t, R("TMS: field STRUCTURE_CHECK has the wrong type"))
t = c(SPRING); del t["TMS"]
CLS("switch/tms-missing", t, R("TMS: zone is not an object"))
t = c(SPRING); t["TMS"] = "x"
CLS("switch/tms-string", t, R("TMS: zone is not an object"))
t = c(SPRING); del t["TMS"]["PARAMETERS"]
CLS("switch/params-missing", t, R("TMS: part PARAMETERS is not an object"))
t = c(SPRING); t["TMS"]["PARAMETERS"] = "OFF"
CLS("switch/params-string", t, R("TMS: part PARAMETERS is not an object"))
CLS("switch/tfk-string", "x", R("TFK is not an object"))
FND("switch/off-not-read", with_sc(X["A12"], "OFF"), HAS("[UNDER,x,[v,x],[N2],"),
note="eom_findings reads no switch (S26: the preview shows the map whatever the switch says)")
MAP("switch/off-not-read", with_sc(SPRING, "OFF"), HAS("[x,DETERMINED,KIN]"))
# ==== C: the D variable (D177.1; the TPK PARAMETERS part is not read here) ===========
t = c(X["A10a"]); t["TPK"] = dict([("PARAMETERS", {"D_VARIABLES": "SEVERAL"})] + list(t["TPK"].items()))
MAP("dvar/several-pde", t, HAS("[ANALYSIS,PDE]"))
CLS("dvar/several-pde", t, NV("PDE"))
t = c(SPRING); t["TPK"] = dict([("PARAMETERS", {"D_VARIABLES": "SEVERAL"})] + list(t["TPK"].items()))
CLS("dvar/several-one-variable", t, REG, note="SEVERAL with one D variable is analysed as under ONE")
t = c(X["A10a"]); t["TPK"]["PARAMETERS"] = {"D_VARIABLES": "ONE"}
CLS("dvar/one-with-two", t, NV("PDE"), note="T1 refuses this TPK; the check itself reads no D_VARIABLES")
t = c(SPRING); t["TPK"]["PARAMETERS"] = "not read"
CLS("dvar/params-not-read", t, REG)
PDE3 = K(["u:TH1", "X:L1", "Y:L1", "t:T1"], ["a_d:L2 T-1"],
[("HEAT", "EOM(u)", "D(u, t) = a_d * D(u, X, 2) + a_d * D(u, Y, 2)")], tpk_params={"D_VARIABLES": "SEVERAL"})
MAP("dvar/three-variables", PDE3, HAS("[D_VARIABLES,[X,Y,t]]", "[X,INDEPENDENT,]"))
FND("dvar/three-variables", PDE3, HAS("[PDE,[X,Y,t],PDE: not analyzed]"))
PDEX = K(["u:TH1", "X:L1", "t:T1", "w:L1", "q:L1"], ["a_d:L2 T-1", "k:1"],
[("HEAT", "EOM(u)", "D(u, t) = a_d * D(u, X, 2)"), ("QL", "EOM(q)", "q = k * X"),
("WL", "EOM(w)", None, ["w", "k"]), ("DUP1", "EOM(u)", "D(u, t) = a_d * D(u, X, 2)")],
tpk_params={"D_VARIABLES": "SEVERAL"})
FND("dvar/pde-per-law-checks", PDEX,
HAS("[ROLE MISMATCH,QL,q,NO DERIVATIVE,", "[PROSE,WL,[w],", "[PDE,[X,t],"),
note="under PDE only ROLE MISMATCH and PROSE run beside the PDE line; no OVER-EOM for DUP1")
DCON = K(["x:L1", "v:L1 T-1"], ["k:T1"], [("KIN", "EOM(x)", "D(x, k) = v"), ("N2", "EOM(v)", "D(v, k) = -x")])
MAP("dvar/constant-variable", DCON, HAS("[D_VARIABLES,[k]]", "[x,DETERMINED,KIN]"),
note="T1 refuses a D variable that is no DOF; the check reads k as known")
CLS("dvar/constant-variable", DCON, REG)
MAP("dvar/scaled-time", X["A21"], HAS("[tau,INDEPENDENT,]"))
# ==== D: zero propagation ===============================================================
ZD = ["x:L1", "v:L1 T-1", "t:T1", "z:L1"]
ZC = ["m:M1", "k:M1 T-2", "g_n:L1 T-2=9.80665 m s-2"]
ZL = [("KIN", "EOM(x)", "D(x, t) = v"), ("N2", "EOM(v)", "m * D(v, t) = -k * x")]
def ZK(eq, fixv="0", extra_dofs=(), extra_cons=(), role="CONSTRAINT", consts=ZC):
return K(ZD + list(extra_dofs), consts, ZL + [("L", role, eq)],
[("C_Z", "FIX", "z", fixv, "m")] + list(extra_cons))
for tag, eq, fixv, kind in [
("value-zero-product", "k * z = 0", "0", "ZERO"),
("value-zero-spelled", "k * z = 0", "0.000e3", "ZERO"),
("value-minus-zero", "k * z = 0", "-0", "ZERO"),
("value-nonzero-product", "k * z = 0", "2", "UNBOUND"),
("value-nonzero-bound", "g_n * z = 0", "2", "BOUND"),
("value-zero-alone", "z = 0", "0", "ZERO"),
("value-one-alone", "z = 0", "1", "BOUND"),
("derivative-times", "k * D(z, t) = 0", "3", "ZERO"),
("derivative-over", "D(z, t) / k = 0", "3", "ZERO"),
("divide-by-derivative", "k / D(z, t) = 0", "3", "UNBOUND"),
("functions-to-zero", "sin(D(z, t)) + abs(D(z, t)) + sqrt(D(z, t)) - tan(D(z, t)) = -D(z, t, 2)", "3",
"ZERO"),
("cos-of-zero", "cos(D(z, t)) = 1", "3", "BOUND"),
("exp-of-zero", "exp(D(z, t)) = 0", "3", "BOUND"),
("ln-of-zero", "ln(D(z, t)) = k", "3", "UNBOUND"),
("power-positive", "D(z, t)^2 = 0", "3", "ZERO"),
("power-root", "D(z, t)^(1/2) = 0", "3", "ZERO"),
("power-negative", "D(z, t)^(-1) = k", "3", "UNBOUND"),
("power-of-sum", "(D(z, t) - D(z, t, 2))^3 = -D(z, t)", "3", "ZERO"),
("literal-zero-times-unknown", "0 * v = g_n", "3", "BOUND"),
("literal-zero-spelled", "0.0 * v = 0", "3", "ZERO"),
("sum-not-zero", "k * D(z, t) + g_n = 0", "3", "BOUND")]:
MAP("zero/" + tag, ZK(eq, fixv), HAS("[CLOSED,[[L," + kind + "]]]"))
FND("zero/value-nonzero-product", ZK("k * z = 0", "2"), HAS("[CLOSED,L,[k],"))
FND("zero/value-zero-product", ZK("k * z = 0", "0"), "[OK,[]]")
FND("zero/divide-by-derivative", ZK("k / D(z, t) = 0", "3"), HAS("[CLOSED,L,[k],"))
FND("zero/cos-of-zero", ZK("cos(D(z, t)) = 1", "3"), "[OK,[]]", note="fully bound: T3's ground fragment")
t = ZK("k * z = 0", "0", extra_cons=[("C_Z2", "FIX", "z", "2", "m")])
MAP("zero/two-fixes-one-nonzero", t, HAS("[CLOSED,[[L,UNBOUND]]]"),
note="the value propagates as zero only when every FIX of the DOF is zero (T3 refuses two values)")
t = ZK("k * D(z, t) = F_n", "3", extra_dofs=["F_n:M1 L1 T-2"])
MAP("zero/multiplier-kept", t, HAS("[F_n,DETERMINED,L]"))
t = ZK("D(w, t) = 0", "3", extra_dofs=["w:L1"], extra_cons=[("C_W", "REMOVE", "w")])
MAP("zero/removed-derivative", t, HAS("[CLOSED,[[L,UNBOUND]]]", "[w,REMOVED,]"))
FND("zero/removed-derivative", t, HAS("[CLOSED,L,[t,w],"))
t = ZK("xi = 0", "3", extra_dofs=["xi:M1 L1 T-2:INPUT"])
FND("zero/input-in-closed-law", t, HAS("[CLOSED,L,[xi],"))
t = ZK("g_n * t = 0", "3")
FND("zero/variable-in-closed-law", t, HAS("[CLOSED,L,[t],"),
note="the D variable is known and unbound: listed as CLOSED (RD-R2-8)")
t = ZK("k * D(z, t) = 0", "3", role="INVARIANT")
MAP("zero/invariant-not-closed", t, HAS("[CLOSED,[]]", "[INVARIANT,[L]]"))
# ==== E: ROLE MISMATCH ==================================================================
RM = K(["x:L1", "v:L1 T-1", "t:T1"], ["m:M1", "k:M1 T-2"],
[("KIN", "EOM(x)", "D(x, t) = v"), ("L", "EOM(v)", "k * x + m * v / t = 0")])
FND("role/no-derivative", RM, HAS("[ROLE MISMATCH,L,v,NO DERIVATIVE,"))
MAP("role/no-derivative", RM, HAS("[v,DETERMINED,L]"))
RMK = K(["x:L1", "v:L1 T-1", "t:T1", "z:L1", "w:L1", "xi:M1 L1 T-2:INPUT"], ["m:M1", "k:M1 T-2"],
[("KIN", "EOM(x)", "D(x, t) = v"), ("N2", "EOM(v)", "m * D(v, t) = -k * x + xi"),
("LZ", "EOM(z)", "D(z, t, 2) = 0"), ("LW", "EOM(w)", "D(w, t) = 0"),
("LXI", "EOM(xi)", "D(xi, t) = 0"), ("LT", "EOM(t)", "t = t")],
[("C_Z", "FIX", "z", "0", "m"), ("C_W", "REMOVE", "w")])
FND("role/known-kinds", RMK,
HAS("[ROLE MISMATCH,LT,t,NO DERIVATIVE,", "[ROLE MISMATCH,LT,t,KNOWN,LAW LT declares ROLE EOM(t), but t is "
"known (INDEPENDENT)", "[ROLE MISMATCH,LW,w,KNOWN,", "(REMOVED)", "[ROLE MISMATCH,LXI,xi,KNOWN,",
"(INPUT)", "[ROLE MISMATCH,LZ,z,KNOWN,", "(FIXED)"))
CLS("role/known-kinds", RMK, NV("FINDINGS"))
RMP = K(["x:L1", "v:L1 T-1", "t:T1", "z:L1"], ["m:M1", "k:M1 T-2"],
[("KIN", "EOM(x)", "D(x, t) = v"), ("N2", "EOM(v)", "m * D(v, t) = -k * x"),
("PZ", "EOM(z)", None, ["z", "t"])], [("C_Z", "FIX", "z", "0", "m")])
FND("role/prose-known", RMP, HAS("[ROLE MISMATCH,PZ,z,KNOWN,"), note="ROLE is read on a prose law too")
FND("role/multiplier-no-finding", X["A07"], "[OK,[]]",
note="lam, determined by NX and NY with ROD CONSTRAINT, is a multiplier: no finding")
# ==== F: OVER-EOM (ROLE clause and the equation-of-motion shape) =======================
OD = ["x:L1", "v:L1 T-1", "t:T1"]
OC = ["m:M1", "M:M1", "k:M1 T-2"]
OB = [("KIN", "EOM(x)", "D(x, t) = v"), ("N2", "EOM(v)", "m * D(v, t) = -k * x")]
def OK2(eq, role="CONSTITUTIVE", name="L2", extra=()):
return K(OD, OC, OB + [(name, role, eq)] + list(extra))
for tag, eq, shape in [
("shape-plain", "D(v, t) = -k * x / m", True),
("shape-negated-factor", "-m * D(v, t) = k * x", True),
("shape-negated-product", "-(m * D(v, t)) = k * x", True),
("shape-denominator", "D(v, t) / m = -k * x / m^2", True),
("shape-constant-sum", "(m + M) * D(v, t) = -k * x", True),
("shape-right-side", "-k * x = m * D(v, t)", True),
("shape-parenthesized", "((m) * (D(v, t))) = -k * x", True),
("no-shape-dof-factor", "x * D(v, t) = -k * x", False),
("no-shape-two-derivatives", "D(v, t) * D(x, t) = -k * x / m", False),
("no-shape-sum", "D(v, t) + k * x / m = 0", False),
("no-shape-derivative-in-denominator", "m / D(v, t) = -k * x", False),
("no-shape-other-order", "D(v, t, 2) = -k * v / m", False)]:
FND("overeom/" + tag, OK2(eq), HAS("[OVER-EOM,v,[L2,N2],") if shape else HAS("[OVER,"))
FND("overeom/invariant-excluded", OK2("D(v, t) = -k * x / m", role="INVARIANT"), "[OK,[]]")
FND("overeom/role-three", OK2("D(v, t) = -k * x / m", role="EOM(v)",
extra=[("L3", "EOM(v)", "k * x + m * D(v, t) = 0")]), HAS("[OVER-EOM,v,[L2,L3,N2],"))
CLS("overeom/role-three", OK2("D(v, t) = -k * x / m", role="EOM(v)",
extra=[("L3", "EOM(v)", "k * x + m * D(v, t) = 0")]), NV("FINDINGS"))
FND("overeom/role-no-shape", OK2("k * x + m * D(v, t) = 0", role="EOM(v)"), HAS("[OVER-EOM,v,[L2,N2],"),
note="the ROLE clause needs no shape")
FND("overeom/role-and-extra-redundancy",
K(OD, OC + ["x_0:L1"], OB + [("N2B", "EOM(v)", "D(v, t) = -k * x / m"), ("IC", "CONSTRAINT", "x = x_0")]),
HAS("[OVER-EOM,v,[N2,N2B],", "[OVER,[IC,KIN,N2],[v,x],"),
note="OVER-EOM sets N2B aside; the redundancy left is OVER")
FND("overeom/two-groups",
K(OD, OC, OB + [("KIN2", "EOM(x)", "D(x, t) = v"), ("N2B", "EOM(v)", "D(v, t) = -k * x / m")]),
HAS("[OVER-EOM,v,[N2,N2B],", "[OVER-EOM,x,[KIN,KIN2],"))
FND("overeom/shape-on-known-not-listed",
K(OD + ["z:L1"], OC, OB + [("Z1", "CONSTRAINT", "D(z, t, 2) = 0"), ("Z2", "CONSTRAINT", "m * D(z, t, 2) = 0")],
[("C_Z", "FIX", "z", "0", "m")]), "[OK,[]]",
note="the shape clause reads unknowns only; both laws reduce to 0 = 0")
# ==== G: UNDER ==========================================================================
UD = K(["a:L1", "b:L1", "c:L1", "d:L1"], ["k:L1"], [("P1", "CONSTRAINT", "a + b = k"), ("P2", "CONSTRAINT", "c + d = k")])
FND("under/two-blocks", UD, HAS("[UNDER,b,[a,b],[P1],", "[UNDER,d,[c,d],[P2],"))
MAP("under/two-blocks", UD, HAS("[a,UNDER,P1]", "[c,UNDER,P2]"))
UR = K(["x:L1", "v:L1", "t:T1"], ["k:L1 T-1"], [("L", "EOM(x)", "D(x, t) + D(v, t) = k")])
FND("under/role-tier", UR, HAS("[UNDER,v,"), note="sigma ties (1, 1); the ROLE EOM(x) keeps x")
UR2 = K(["x:L1", "v:L1", "t:T1"], ["k:L1 T-1"], [("L", "CONSTRAINT", "D(x, t) + D(v, t) = k")])
FND("under/name-tier", UR2, HAS("[UNDER,x,"), note="sigma and ROLE tie; NAME order gives L to v")
UR3 = K(["x:L1", "v:L1 T-1", "t:T1"], ["k:L1 T-2"], [("L", "EOM(v)", "D(x, t, 2) + D(v, t) = k")])
FND("under/sigma-tier", UR3, HAS("[UNDER,v,"), note="the higher derivative order wins over the ROLE")
UA = K(["x:L1", "z:L1", "t:T1"], ["m:M1"], [("LZ", "CONSTRAINT", "m * D(z, t, 2) = 0")], [("C_Z", "FIX", "z", "0", "m")])
FND("under/all-closed", UA, HAS("[UNDER,x,[x],[],unknown x is named by no law with a declared form"))
UI = K(["x:L1", "t:T1"], ["k:L1 T-1"], [("I", "INVARIANT", "D(x, t) = k")])
FND("under/invariant-only", UI, HAS("[UNDER,x,[x],[],"), note="a formed INVARIANT law: not NO FORM; leaves the matching")
# ==== H: OVER ===========================================================================
OV = K(["a:L1", "b:L1"], ["k:L1", "h:L1", "j:L1"],
[("P1", "CONSTRAINT", "a = k"), ("P2", "CONSTRAINT", "a = h"), ("P3", "CONSTRAINT", "b = k"),
("P4", "CONSTRAINT", "b = j")])
FND("over/two-blocks", OV, HAS("[OVER,[P1,P2],[a],", "[OVER,[P3,P4],[b],"))
MAP("over/two-blocks", OV, HAS("[a,OVER,P1]", "[b,OVER,P3]"))
# ==== I: Pryce's offsets, the index and the initial-value count ========================
IX2 = K(["x:L1", "y:L1 T-1", "t:T1"], ["k:L1"], [("K", "EOM(x)", "D(x, t) = y"), ("C", "CONSTRAINT", "x = k * sin(t)")])
MAP("pryce/index-two", IX2, HAS("[INDEX,2]", "[INITIAL_VALUES,0]"))
IO2 = K(["x:L1", "t:T1"], ["m:M1", "k:M1 T-2"], [("N2", "EOM(x)", "m * D(x, t, 2) = -k * x")])
MAP("pryce/second-order", IO2, HAS("[INDEX,0]", "[INITIAL_VALUES,2]", "[OFFSETS,[[N2,0]],[[x,2]]]"))
IO3 = K(["x:L1", "t:T1"], ["k:T-3"], [("J", "EOM(x)", "D(x, t, 3) = -k * x")])
MAP("pryce/third-order", IO3, HAS("[INITIAL_VALUES,3]"))
MAP("pryce/empty-square", X["A12"], HAS("[INDEX,0]", "[INITIAL_VALUES,0]", "[OFFSETS,[],[]]"))
# ==== J: NO FORM and prose ==============================================================
NF = K(["z:L1"], ["m:M1"], [("PZ", "EOM(z)", None, ["z", "m"])], [("C_Z", "FIX", "z", "0", "m")])
FND("noform/no-unknown", NF, HAS("[ROLE MISMATCH,PZ,z,KNOWN,", "[NO FORM,[],no LAW carries an EQUATION and the "
"kernel has no unknown: is that intended?]"))
CLS("noform/no-unknown", NF, NV("FINDINGS", "NO FORM"))
NL = K(["x:L1"], [], [])
del NL["TPK"]["LAW"]
FND("noform/no-law-kind", NL, HAS("[NO FORM,[x],"))
MAP("noform/no-law-kind", NL, HAS("[x,NO LAW,]"))
PI = K(["x:L1", "v:L1 T-1", "t:T1"], ["m:M1", "k:M1 T-2"],
OB[:1] + [("N2", "EOM(v)", "m * D(v, t) = -k * x"), ("PI", "INVARIANT", None, ["x", "v", "m", "k"]),
("PC", "CONSTITUTIVE", None, ["m", "k"])])
MAP("prose/invariant-and-constant-only", PI, HAS("[INVARIANT,[PI]]", "[PROSE,[]]"))
FND("prose/invariant-and-constant-only", PI, "[OK,[]]",
note="an INVARIANT prose law and a prose law naming no unknown print nothing")
CLS("prose/invariant-and-constant-only", PI, REG)
# ==== K: what is not read ===============================================================
t = c(SPRING); t["TPK"]["ASSUMPTION"] = "x"; t["TPK"]["BOUNDARY"] = 5; t["TrM"] = 7
MAP("unread/other-kinds", t, HAS("[x,DETERMINED,KIN]"), note="ASSUMPTION, BOUNDARY and the TrM are not read")
t = c(SPRING); del t["TPK"]["DOF"][0]["DIMENSION"]; del t["TPK"]["LAW"][0]["STATEMENT"]
del t["TPK"]["LAW"][0]["REFS"]
CLS("unread/fields", t, REG, note="DIMENSION, STATEMENT and a formed law's REFS are not read")
t = c(SPRING); t["TPK"]["CONSTRAINT"][0]["UNIT"] = 5; t["TPK"]["CONSTRAINT"][0]["NAME"] = 5
CLS("unread/constraint-fields", t, REG)
t = c(X["A25"]); t["TPK"]["CONSTRAINT"] = [{"NAME": "C_R", "TARGET": "x", "ACTION": "REMOVE", "VALUE": 5,
"STATEMENT": "s"}]
MAP("unread/remove-value", t, HAS("[x,REMOVED,]"), note="a REMOVE's VALUE is not read (T1 forbids it)")
# ==== L: the later test (STRUCTURE TEST WITH REGISTER) =================================
def rec(i, status="PROVISIONAL", role=None, eq=None):
r = {"ID": i, "STATUS": status}
if role is not None:
r["ROLE"] = role
if eq is not None:
r["EQUATION"] = eq
return r
E01 = X["E01"]
RV = rec("RR-1", role="EOM(v)", eq="m * D(v, t) = -k_s * x")
REGT("e01-settled", E01, [RV], HAS("[USED,[RR-1]],[SETTLED,[v]],[OPEN,[]]", "[v,DETERMINED,RR-1]",
"[PROSE,ACTION,[v,x],"),
note="E01: v's equation of motion is derived in the register; EOM-0 settles; the prose ACTION stays listed")
REGT("e01-no-records", E01, [], HAS("[USED,[]],[SETTLED,[]],[OPEN,[v]]", "[UNDER,v,"))
for st in ["HELD", "REFUTED", "WITHDRAWN"]:
REGT("e01-stale-" + st.lower(), E01, [rec("RR-1", st, "EOM(v)", "m * D(v, t) = -k_s * x")],
HAS("[USED,[]],[SETTLED,[]],[OPEN,[v]]"), note="a record that does not stand is ignored (S24)")
for st in ["STRUCK", "VOID"]:
REGT("e01-stale-" + st.lower(), E01, [rec("RR-1", st, "EOM(v)", "m * D(v, t) = -k_s * x")],
R("RECORD:RR-1: STATUS " + st + " is not a status word"),
note="STRUCK is retired and VOID is no status (tpm_record_schema 0.2.0, 6.9): refused (12.1)")
REGT("e01-standing-words", E01, [rec("RR-3", "ESTABLISHED", "EOM(v)", "m * D(v, t) = -k_s * x"),
rec("RR-4", "HELD", "EOM(x)", "D(x, t) = v")],
HAS("[USED,[RR-3]],[SETTLED,[v]],[OPEN,[]]"),
note="PROVISIONAL and ESTABLISHED stand; HELD, REFUTED and WITHDRAWN do not (12.1)")
REGT("e01-no-role", E01, [rec("RR-2", eq="m * D(v, t) = -k_s * x")], HAS("[USED,[]]", "[OPEN,[v]]"),
note="a record declaring no ROLE enters nothing (S23)")
REGT("e01-invariant-role", E01, [rec("RR-2", role="INVARIANT", eq="m * D(v, t) = -k_s * x")],
HAS("[USED,[]]", "[OPEN,[v]]"), note="INVARIANT does not enter the matching")
REGT("e01-no-equation", E01, [rec("RR-2", role="EOM(v)")], HAS("[USED,[]]", "[OPEN,[v]]"),
note="a record without a declared form enters nothing")
REGT("e01-initial-value-assumption", E01, [RV, rec("RR-7", eq="x = x_max")],
HAS("[USED,[RR-1]]", "[SETTLED,[v]]"), note="an initial value's ASSUMPTION record declares no ROLE (S23)")
REGT("e01-initial-value-with-role", E01, [RV, rec("RR-7", role="CONSTRAINT", eq="x = x_max")],
HAS("[USED,[RR-1,RR-7]]", "[OVER,[KIN,RR-1,RR-7],[v,x],", "[SETTLED,[v]]"),
note="an initial value given a ROLE over-determines (the A25 false OVER that S23 avoids)")
REGT("e01-duplicate-eom", E01, [RV, rec("RR-2", role="EOM(v)", eq="D(v, t) = -k_s * x / m")],
HAS("[OVER-EOM,v,[RR-1,RR-2],", "[SETTLED,[v]]"))
REGT("e01-record-order", E01, [rec("RR-10", role="DEFINITION", eq="k_s = m * k_s / m"),
rec("RR-9", role="EOM(v)", eq="m * D(v, t) = -k_s * x"),
rec("AB-3", role="CONSTITUTIVE", eq="x_max = x_max"),
rec("RR-2", "VOID", "EOM(v)", "D(v, t) = 0")],
R("RECORD:RR-2: STATUS VOID is not a status word"), note="VOID is no status: refused (12.1)")
REGT("e01-record-order-withdrawn", E01, [rec("RR-10", role="DEFINITION", eq="k_s = m * k_s / m"),
rec("RR-9", role="EOM(v)", eq="m * D(v, t) = -k_s * x"),
rec("AB-3", role="CONSTITUTIVE", eq="x_max = x_max"),
rec("RR-2", "WITHDRAWN", "EOM(v)", "D(v, t) = 0")],
HAS("[USED,[AB-3,RR-9,RR-10]]"), note="IDs sorted by prefix, then n numerically; a WITHDRAWN record ignored")
REGT("e01-record-pde", E01, [RV, rec("RR-5", role="CONSTRAINT", eq="D(x, k_s) = v")],
HAS("[ANALYSIS,PDE]", "[SETTLED,[]],[OPEN,[v]]"), note="a second D variable: not analyzed, nothing settled")
REGT("a12-settled", X["A12"], [rec("RR-1", role="EOM(x)", eq="D(x, t) = v")],
HAS("[SETTLED,[x]],[OPEN,[]]"))
REGT("a27a-settled-by-other", X["A27a"], [rec("RR-1", role="CONSTRAINT", eq="b = L_2")],
HAS("[SETTLED,[c]],[OPEN,[]]", "[OVER,[P2,P3],[a],"),
note="c is settled when the under part empties, whichever unknown the record names")
UD3 = K(["a:L1", "b:L1", "c:L1", "d:L1"], ["k:L1"], [("P1", "CONSTRAINT", "a + b + c = k")])
REGT("under-block-partial", UD3, [rec("RR-1", role="CONSTRAINT", eq="a = k")],
HAS("[SETTLED,[]],[OPEN,[b,c,d]]"),
note="settled means outside the combined under part: the TFK's UNDER list is b, c, d; a record naming a "
"leaves b, c under-determined and d unnamed, so none settles")
REGT("spring-regular-unchanged", SPRING, [rec("RR-1", role="EOM(v)", eq="m * D(v, t) = -k_s * x")],
HAS("[OVER-EOM,v,[EOM_X,RR-1],", "[SETTLED,[]],[OPEN,[]]"))
REGT("a10a-pde-tfk", X["A10a"], [rec("RR-1", role="EOM(u)", eq="D(u, t) = 0")], HAS("[ANALYSIS,PDE]", "[OPEN,[]]"))
REGT("record-undeclared-variable", E01, [rec("RR-1", role="EOM(v)", eq="D(v, D_) = 0")],
R("RECORD:RR-1: EQUATION names D_, which is not a DOF or CONSTANT"))
REGT("a23-noform-with-records", X["A23"], [rec("RR-1", role="EOM(x)", eq="D(x, t) = -a_r * x")],
HAS("[ANALYSIS,RUN]", "[USED,[RR-1]]", "[SETTLED,[]],[OPEN,[]]", "[PROSE,DDE,[x],"),
note="the TFK alone has no form, so no UNDER list; the record gives the analysis its form")
REGT("stale-malformed-still-read", E01, [rec("RR-1", "HELD", "EOM(v)", "m * D(v, t) = -k_s * g")],
R("RECORD:RR-1: EQUATION names g, which is not a DOF or CONSTANT"),
note="every record is read whole, standing or not")
# ==== M: refusals (malformed shapes; never an exception) ===============================
def SPR():
return c(SPRING)
def tpk_set(path, value):
t = SPR()
o = t["TPK"]
for p in path[:-1]:
o = o[p]
o[path[-1]] = value
return t
def tpk_del(path):
t = SPR()
o = t["TPK"]
for p in path[:-1]:
o = o[p]
del o[path[-1]]
return t
REF = [
("tfk-string", "x", "TFK is not an object"),
("tfk-null", None, "TFK is not an object"),
("tfk-list", [1], "TFK is not an object"),
("tfk-integer", 7, "TFK is not an object"),
]
for tag, tfk, why in REF:
MAP("refuse/" + tag, tfk, R(why))
t = SPR(); del t["TPK"]
MAP("refuse/tpk-missing", t, R("TPK: zone is not an object"))
t = SPR(); t["TPK"] = "x"
MAP("refuse/tpk-string", t, R("TPK: zone is not an object"))
FND("refuse/tpk-string", t, R("TPK: zone is not an object"))
REFT = [
("dof-kind-string", tpk_set(["DOF"], "x"), "TPK kind DOF is not a list"),
("dof-kind-null", tpk_set(["DOF"], None), "TPK kind DOF is not a list"),
("dof-entry-string", tpk_set(["DOF", 0], "t"), "TPK kind DOF: entry is not an object"),
("dof-name-missing", tpk_del(["DOF", 1, "NAME"]), "DOF:?: missing field NAME"),
("dof-name-integer", tpk_set(["DOF", 1, "NAME"], 5), "DOF:?: field NAME has the wrong type"),
("dof-name-space", tpk_set(["DOF", 1, "NAME"], "x y"), "DOF:x y: NAME x y is not an identifier"),
("dof-name-bidi", tpk_set(["DOF", 1, "NAME"], "x\u202e"), "DOF:x<U+202E>: NAME x<U+202E> is not an identifier"),
("dof-role-integer", tpk_set(["DOF", 1, "ROLE"], 1), "DOF:x: field ROLE has the wrong type"),
("dof-role-lower", tpk_set(["DOF", 1, "ROLE"], "input"), "DOF:x: ROLE input is not INPUT"),
("dof-role-output", tpk_set(["DOF", 1, "ROLE"], "OUTPUT"), "DOF:x: ROLE OUTPUT is not INPUT"),
("const-kind-string", tpk_set(["CONSTANT"], "m"), "TPK kind CONSTANT is not a list"),
("const-entry-list", tpk_set(["CONSTANT", 0], ["m"]), "TPK kind CONSTANT: entry is not an object"),
("const-name-missing", tpk_del(["CONSTANT", 0, "NAME"]), "CONSTANT:?: missing field NAME"),
("const-value-integer", tpk_set(["CONSTANT", 2, "VALUE"], 5), "CONSTANT:x_max: field VALUE has the wrong type"),
("law-kind-string", tpk_set(["LAW"], "KIN"), "TPK kind LAW is not a list"),
("law-entry-integer", tpk_set(["LAW", 1], 3), "TPK kind LAW: entry is not an object"),
("law-name-missing", tpk_del(["LAW", 1, "NAME"]), "LAW:?: missing field NAME"),
("law-name-digit", tpk_set(["LAW", 1, "NAME"], "1KIN"), "LAW:1KIN: NAME 1KIN is not an identifier"),
("dupe-dof-law", tpk_set(["LAW", 1, "NAME"], "x"), "TPK: duplicate name x"),
("dupe-dof-const", tpk_set(["CONSTANT", 0, "NAME"], "v"), "TPK: duplicate name v"),
("dupe-law-law", tpk_set(["LAW", 2, "NAME"], "KIN"), "TPK: duplicate name KIN"),
("cons-kind-string", tpk_set(["CONSTRAINT"], "C"), "TPK kind CONSTRAINT is not a list"),
("cons-entry-string", tpk_set(["CONSTRAINT", 0], "C"), "TPK kind CONSTRAINT: entry is not an object"),
("cons-target-missing", tpk_del(["CONSTRAINT", 0, "TARGET"]), "CONSTRAINT:C_NOZ: missing field TARGET"),
("cons-target-integer", tpk_set(["CONSTRAINT", 0, "TARGET"], 5), "CONSTRAINT:C_NOZ: field TARGET has the wrong type"),
("cons-action-missing", tpk_del(["CONSTRAINT", 0, "ACTION"]), "CONSTRAINT:C_NOZ: missing field ACTION"),
("cons-action-lower", tpk_set(["CONSTRAINT", 0, "ACTION"], "fix"), "CONSTRAINT:C_NOZ: ACTION fix is not REMOVE or FIX"),
("cons-target-constant", tpk_set(["CONSTRAINT", 0, "TARGET"], "m"), "CONSTRAINT:C_NOZ: TARGET m is not a DOF"),
("cons-target-unknown", tpk_set(["CONSTRAINT", 0, "TARGET"], "q"), "CONSTRAINT:C_NOZ: TARGET q is not a DOF"),
("cons-fix-no-value", tpk_del(["CONSTRAINT", 0, "VALUE"]), "CONSTRAINT:C_NOZ: FIX requires VALUE"),
("cons-value-integer", tpk_set(["CONSTRAINT", 0, "VALUE"], 0), "CONSTRAINT:C_NOZ: field VALUE has the wrong type"),
("cons-value-word", tpk_set(["CONSTRAINT", 0, "VALUE"], "zero"), "CONSTRAINT:C_NOZ: VALUE zero is not a decimal"),
("law-role-missing", tpk_del(["LAW", 1, "ROLE"]), "LAW:KIN: missing field ROLE"),
("law-role-integer", tpk_set(["LAW", 1, "ROLE"], 5), "LAW:KIN: field ROLE has the wrong type"),
("law-role-space", tpk_set(["LAW", 1, "ROLE"], "EOM (x)"), "LAW:KIN: ROLE EOM (x) is not a role"),
("law-role-inner-space", tpk_set(["LAW", 1, "ROLE"], "EOM( x)"), "LAW:KIN: ROLE EOM( x) is not a role"),
("law-role-lower", tpk_set(["LAW", 1, "ROLE"], "eom(x)"), "LAW:KIN: ROLE eom(x) is not a role"),
("law-role-empty-eom", tpk_set(["LAW", 1, "ROLE"], "EOM()"), "LAW:KIN: ROLE EOM() is not a role"),
("law-role-trailing-lf", tpk_set(["LAW", 1, "ROLE"], "CONSTRAINT\n"), "LAW:KIN: ROLE CONSTRAINT\n is not a role"),
("law-role-input", tpk_set(["LAW", 1, "ROLE"], "INPUT"), "LAW:KIN: ROLE INPUT is not a role"),
("law-role-eom-constant", tpk_set(["LAW", 1, "ROLE"], "EOM(k_s)"), "LAW:KIN: ROLE EOM(k_s): k_s is not a DOF"),
("law-role-eom-nothing", tpk_set(["LAW", 1, "ROLE"], "EOM(q)"), "LAW:KIN: ROLE EOM(q): q is not a DOF"),
("law-role-eom-law", tpk_set(["LAW", 1, "ROLE"], "EOM(EOM_X)"), "LAW:KIN: ROLE EOM(EOM_X): EOM_X is not a DOF"),
("law-equation-integer", tpk_set(["LAW", 1, "EQUATION"], 5), "LAW:KIN: field EQUATION has the wrong type"),
("law-equation-null", tpk_set(["LAW", 1, "EQUATION"], None), "LAW:KIN: field EQUATION has the wrong type"),
("law-equation-no-eq", tpk_set(["LAW", 1, "EQUATION"], "D(x, t) - v"),
"LAW:KIN: EQUATION does not parse: the equation has no ="),
("law-equation-bidi", tpk_set(["LAW", 1, "EQUATION"], "D(x, t) = v\u202e"),
"LAW:KIN: EQUATION does not parse: unexpected character <U+202E> at 12"),
("law-equation-undeclared", tpk_set(["LAW", 1, "EQUATION"], "D(x, t) = v + g"),
"LAW:KIN: EQUATION names g, which is not a DOF or CONSTANT"),
("law-equation-undeclared-variable", tpk_set(["LAW", 1, "EQUATION"], "D(x, tau) = v"),
"LAW:KIN: EQUATION names tau, which is not a DOF or CONSTANT"),
("law-equation-names-law", tpk_set(["LAW", 1, "EQUATION"], "D(x, t) = v + EOM_Z"),
"LAW:KIN: EQUATION names EOM_Z, which is not a DOF or CONSTANT"),
("law-equation-long", tpk_set(["LAW", 1, "EQUATION"], "D(x, t) = v" + " " * 4090),
"LAW:KIN: EQUATION does not parse: the form is longer than 4096 code points"),
]
for tag, t, why in REFT:
MAP("refuse/" + tag, t, R(why))
FND("refuse/law-role-space", tpk_set(["LAW", 1, "ROLE"], "EOM (x)"), R("LAW:KIN: ROLE EOM (x) is not a role"))
CLS("refuse/law-role-space", tpk_set(["LAW", 1, "ROLE"], "EOM (x)"), R("LAW:KIN: ROLE EOM (x) is not a role"))
t = c(E01); del t["TPK"]["LAW"][1]["REFS"]
MAP("refuse/prose-refs-missing", t, R("LAW:ACTION: missing field REFS"))
t = c(E01); t["TPK"]["LAW"][1]["REFS"] = "v"
MAP("refuse/prose-refs-string", t, R("LAW:ACTION: field REFS has the wrong type"))
t = c(E01); t["TPK"]["LAW"][1]["REFS"] = ["v", 1]
MAP("refuse/prose-refs-member", t, R("LAW:ACTION: field REFS has the wrong type"))
# order: the first problem in reading order refuses
t = tpk_set(["DOF", 1, "NAME"], 5); t["TPK"]["CONSTANT"] = "m"
MAP("refuse/order-dof-before-constant", t, R("DOF:?: field NAME has the wrong type"))
t = tpk_set(["CONSTANT", 0, "VALUE"], 5); t["TPK"]["LAW"][0]["NAME"] = 5
MAP("refuse/order-constant-before-law", t, R("CONSTANT:m: field VALUE has the wrong type"))
t = tpk_set(["LAW", 0, "NAME"], "x"); t["TPK"]["CONSTRAINT"] = "C"
MAP("refuse/order-duplicate-before-constraint", t, R("TPK: duplicate name x"))
t = tpk_set(["CONSTRAINT", 0, "ACTION"], "fix"); t["TPK"]["LAW"][0]["ROLE"] = "EOM"
MAP("refuse/order-constraint-before-role", t, R("CONSTRAINT:C_NOZ: ACTION fix is not REMOVE or FIX"))
t = tpk_set(["LAW", 2, "ROLE"], "EOM"); t["TPK"]["LAW"][1]["EQUATION"] = "D(x, t) = g"
MAP("refuse/order-law-list-order", t, R("LAW:KIN: EQUATION names g, which is not a DOF or CONSTANT"))
t = tpk_set(["LAW", 1, "EQUATION"], "D(x, t) = v + h + g")
MAP("refuse/order-least-name", t, R("LAW:KIN: EQUATION names g, which is not a DOF or CONSTANT"))
t = tpk_set(["LAW", 1, "NAME"], "x"); t["TPK"]["LAW"][2]["NAME"] = "v"
MAP("refuse/order-least-duplicate", t, R("TPK: duplicate name v"))
# records
RRF = [
("records-string", "RR-1", "records is not a list"),
("records-null", None, "records is not a list"),
("records-entry-string", ["RR-1"], "records: entry is not an object"),
("id-missing", [{"STATUS": "PROVISIONAL"}], "RECORD:?: missing field ID"),
("id-integer", [{"ID": 1, "STATUS": "PROVISIONAL"}], "RECORD:?: field ID has the wrong type"),
("id-no-number", [rec("RR")], "RECORD:RR: ID RR is not a record identifier"),
("id-zero", [rec("RR-0")], "RECORD:RR-0: ID RR-0 is not a record identifier"),
("id-leading-zero", [rec("RR-01")], "RECORD:RR-01: ID RR-01 is not a record identifier"),
("id-space", [rec("R R-1")], "RECORD:R R-1: ID R R-1 is not a record identifier"),
("id-suffix", [rec("RR-1a")], "RECORD:RR-1a: ID RR-1a is not a record identifier"),
("id-no-prefix", [rec("-1")], "RECORD:-1: ID -1 is not a record identifier"),
("id-bib", [rec("RR-BIB1")], "RECORD:RR-BIB1: ID RR-BIB1 is not a record identifier"),
("id-duplicate", [rec("RR-1"), rec("RR-1", "HELD")], "records: duplicate ID RR-1"),
("status-missing", [{"ID": "RR-1"}], "RECORD:RR-1: missing field STATUS"),
("status-integer", [rec("RR-1", 1)], "RECORD:RR-1: field STATUS has the wrong type"),
("status-lower", [rec("RR-1", "held")], "RECORD:RR-1: STATUS held is not a status word"),
("status-empty", [rec("RR-1", "")], "RECORD:RR-1: STATUS is not a status word"),
("status-not-graded", [rec("RR-1", "NOT GRADED")], "RECORD:RR-1: STATUS NOT GRADED is not a status word"),
("status-unmarked", [rec("RR-1", "UNMARKED")], "RECORD:RR-1: STATUS UNMARKED is not a status word"),
("status-struck", [rec("RR-1", "STRUCK")], "RECORD:RR-1: STATUS STRUCK is not a status word"),
("role-integer", [rec("RR-1", role=5, eq="D(x, t) = v")], "RECORD:RR-1: field ROLE has the wrong type"),
("role-bad", [rec("RR-1", role="EOM v", eq="D(x, t) = v")], "RECORD:RR-1: ROLE EOM v is not a role"),
("role-eom-constant", [rec("RR-1", role="EOM(m)", eq="D(x, t) = v")], "RECORD:RR-1: ROLE EOM(m): m is not a DOF"),
("equation-integer", [rec("RR-1", role="EOM(v)", eq=5)], "RECORD:RR-1: field EQUATION has the wrong type"),
("equation-parse", [rec("RR-1", role="EOM(v)", eq="D(v, t) == 0")],
"RECORD:RR-1: EQUATION does not parse: unexpected token = at 10"),
("equation-undeclared", [rec("RR-1", role="EOM(v)", eq="D(v, t) = g")],
"RECORD:RR-1: EQUATION names g, which is not a DOF or CONSTANT"),
("second-record", [rec("RR-1", role="EOM(v)", eq="m * D(v, t) = -k_s * x"), rec("RR-2", "held")],
"RECORD:RR-2: STATUS held is not a status word"),
]
for tag, recs, why in RRF:
REGT("refuse-" + tag, E01, recs, R(why))
t = c(E01); t["TPK"]["LAW"][0]["ROLE"] = "EOM"
REGT("refuse-tfk-first", t, "RR-1", R("LAW:KIN: ROLE EOM is not a role"), note="the TFK is read before the records")
# ==== EXPECTED: literals from the independent oracle (out_R2/work/oracle_eom.py) ====
EXPECTED = {
'eom/findings/A03c': '[OK,[[CLOSED,N2Z,[m],LAW N2Z names no unknown once the fixed DOFs are applied, and depends on m, which the kernel does not bind: does it hold for every value of m, or is a force or an unknown missing?]]]',
'eom/findings/A03c_eomz': '[OK,[[CLOSED,N2Z,[m],LAW N2Z names no unknown once the fixed DOFs are applied, and depends on m, which the kernel does not bind: does it hold for every value of m, or is a force or an unknown missing?],[ROLE MISMATCH,N2Z,z,KNOWN,LAW N2Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/A10a': '[OK,[[PDE,[X,t],PDE: not analyzed]]]',
'eom/findings/A10b': '[OK,[[PROSE,HEAT,[X,t,u],LAW HEAT (ROLE EOM(u)) has no EQUATION and names the unknowns X, t, u: its equation is outside the analysis; can it be declared in form?],[NO FORM,[X,t,u],no LAW carries an EQUATION: which laws give the equations of the unknowns X, t, u?]]]',
'eom/findings/A12': '[OK,[[UNDER,x,[v,x],[N2],unknown x is determined by no law with a declared form (LAW N2 leaves v, x under-determined): which equation determines x?]]]',
'eom/findings/A13_en_constraint': '[OK,[[OVER,[EN,KIN,N2],[v,x],LAWs EN, KIN, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/A14': '[OK,[[OVER-EOM,v,[N2,N2D],LAWs N2, N2D each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/A15': '[OK,[[UNDER,v,[v,y],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, y under-determined): which equation determines v?],[PROSE,N2,[v,y],LAW N2 (ROLE EOM(v)) has no EQUATION and names the unknowns v, y: its equation is outside the analysis; can it be declared in form?]]]',
'eom/findings/A18': '[OK,[[PROSE,IMPACT,[v,y],LAW IMPACT (ROLE CONSTRAINT) has no EQUATION and names the unknowns v, y: its equation is outside the analysis; can it be declared in form?]]]',
'eom/findings/A20_no_input': '[OK,[[UNDER,xi,[v,x,xi],[KIN,N2],unknown xi is determined by no law with a declared form (LAWs KIN, N2 leave v, x, xi under-determined): which equation determines xi?],[PROSE,NOISE,[xi],LAW NOISE (ROLE CONSTITUTIVE) has no EQUATION and names the unknown xi: its equation is outside the analysis; can it be declared in form?]]]',
'eom/findings/A23': '[OK,[[PROSE,DDE,[t,x],LAW DDE (ROLE EOM(x)) has no EQUATION and names the unknowns t, x: its equation is outside the analysis; can it be declared in form?],[NO FORM,[t,x],no LAW carries an EQUATION: which laws give the equations of the unknowns t, x?]]]',
'eom/findings/A25': '[OK,[[OVER,[IC,KIN,N2],[v,x],LAWs IC, KIN, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/A26': '[OK,[[UNDER,w,[w],[],unknown w is named by no law with a declared form: which equation determines w?]]]',
'eom/findings/A27a': '[OK,[[UNDER,c,[b,c],[P1],unknown c is determined by no law with a declared form (LAW P1 leaves b, c under-determined): which equation determines c?],[OVER,[P2,P3],[a],LAWs P2, P3 give more equations than the unknown a they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/A28': '[OK,[[PROSE,KIN,[v,x],LAW KIN (ROLE EOM(x)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?],[PROSE,N2,[v,x],LAW N2 (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?],[NO FORM,[v,x],no LAW carries an EQUATION: which laws give the equations of the unknowns v, x?]]]',
'eom/findings/E01': '[OK,[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]]]',
'eom/findings/E02': '[OK,[[CLOSED,W0DEF,[k_s,m,w0],LAW W0DEF names no unknown once the fixed DOFs are applied, and depends on k_s, m, w0, which the kernel does not bind: does it hold for every value of k_s, m, w0, or is a force or an unknown missing?]]]',
'eom/findings/E03': '[OK,[[OVER-EOM,v,[N2,N2B],LAWs N2, N2B each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/E03_shape': '[OK,[[OVER-EOM,v,[N2,N2B],LAWs N2, N2B each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/corner_no_eom_x': '[OK,[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?]]]',
'eom/findings/dvar/pde-per-law-checks': '[OK,[[ROLE MISMATCH,QL,q,NO DERIVATIVE,LAW QL declares ROLE EOM(q), but its EQUATION has no derivative of q: which ROLE does it have?],[PROSE,WL,[w],LAW WL (ROLE EOM(w)) has no EQUATION and names the unknown w: its equation is outside the analysis; can it be declared in form?],[PDE,[X,t],PDE: not analyzed]]]',
'eom/findings/dvar/three-variables': '[OK,[[PDE,[X,Y,t],PDE: not analyzed]]]',
'eom/findings/g1': '[OK,[[ROLE MISMATCH,FREE_Z,z,KNOWN,LAW FREE_Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/g2': '[OK,[[OVER-EOM,z,[FREE_Z,GRAV_Z],LAWs FREE_Z, GRAV_Z each state the motion of z: are they one equation, or is one to be removed?],[ROLE MISMATCH,FREE_Z,z,KNOWN,LAW FREE_Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?],[ROLE MISMATCH,GRAV_Z,z,KNOWN,LAW GRAV_Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/g2b': '[OK,[[OVER-EOM,z,[FREE_Z,GRAV_Z],LAWs FREE_Z, GRAV_Z each state the motion of z: are they one equation, or is one to be removed?]]]',
'eom/findings/g2c': '[OK,[[OVER-EOM,z,[FREE_Z,GRAV_Z],LAWs FREE_Z, GRAV_Z each state the motion of z: are they one equation, or is one to be removed?]]]',
'eom/findings/g6': '[OK,[[ROLE MISMATCH,FREE_Z,z,KNOWN,LAW FREE_Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/noform/no-law-kind': '[OK,[[NO FORM,[x],no LAW carries an EQUATION: which law gives the equation of the unknown x?]]]',
'eom/findings/noform/no-unknown': '[OK,[[ROLE MISMATCH,PZ,z,KNOWN,LAW PZ declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?],[NO FORM,[],no LAW carries an EQUATION and the kernel has no unknown: is that intended?]]]',
'eom/findings/over/two-blocks': '[OK,[[OVER,[P1,P2],[a],LAWs P1, P2 give more equations than the unknown a they determine: which law is implied by the others, or is one an independent claim?],[OVER,[P3,P4],[b],LAWs P3, P4 give more equations than the unknown b they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/no-shape-derivative-in-denominator': '[OK,[[OVER,[KIN,L2,N2],[v,x],LAWs KIN, L2, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/no-shape-dof-factor': '[OK,[[OVER,[KIN,L2,N2],[v,x],LAWs KIN, L2, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/no-shape-other-order': '[OK,[[OVER,[KIN,L2,N2],[v,x],LAWs KIN, L2, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/no-shape-sum': '[OK,[[OVER,[KIN,L2,N2],[v,x],LAWs KIN, L2, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/no-shape-two-derivatives': '[OK,[[OVER,[KIN,L2,N2],[v,x],LAWs KIN, L2, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/role-and-extra-redundancy': '[OK,[[OVER-EOM,v,[N2,N2B],LAWs N2, N2B each state the motion of v: are they one equation, or is one to be removed?],[OVER,[IC,KIN,N2],[v,x],LAWs IC, KIN, N2 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?]]]',
'eom/findings/overeom/role-no-shape': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/role-three': '[OK,[[OVER-EOM,v,[L2,L3,N2],LAWs L2, L3, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-constant-sum': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-denominator': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-negated-factor': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-negated-product': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-parenthesized': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-plain': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/shape-right-side': '[OK,[[OVER-EOM,v,[L2,N2],LAWs L2, N2 each state the motion of v: are they one equation, or is one to be removed?]]]',
'eom/findings/overeom/two-groups': '[OK,[[OVER-EOM,v,[N2,N2B],LAWs N2, N2B each state the motion of v: are they one equation, or is one to be removed?],[OVER-EOM,x,[KIN,KIN2],LAWs KIN, KIN2 each state the motion of x: are they one equation, or is one to be removed?]]]',
'eom/findings/role/known-kinds': '[OK,[[CLOSED,LT,[t],LAW LT names no unknown once the fixed DOFs are applied, and depends on t, which the kernel does not bind: does it hold for every value of t, or is a force or an unknown missing?],[CLOSED,LW,[t,w],LAW LW names no unknown once the fixed DOFs are applied, and depends on t, w, which the kernel does not bind: does it hold for every value of t, w, or is a force or an unknown missing?],[CLOSED,LXI,[t,xi],LAW LXI names no unknown once the fixed DOFs are applied, and depends on t, xi, which the kernel does not bind: does it hold for every value of t, xi, or is a force or an unknown missing?],[ROLE MISMATCH,LT,t,NO DERIVATIVE,LAW LT declares ROLE EOM(t), but its EQUATION has no derivative of t: which ROLE does it have?],[ROLE MISMATCH,LT,t,KNOWN,LAW LT declares ROLE EOM(t), but t is known (INDEPENDENT): which ROLE does it have?],[ROLE MISMATCH,LW,w,KNOWN,LAW LW declares ROLE EOM(w), but w is known (REMOVED): which ROLE does it have?],[ROLE MISMATCH,LXI,xi,KNOWN,LAW LXI declares ROLE EOM(xi), but xi is known (INPUT): which ROLE does it have?],[ROLE MISMATCH,LZ,z,KNOWN,LAW LZ declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/role/no-derivative': '[OK,[[ROLE MISMATCH,L,v,NO DERIVATIVE,LAW L declares ROLE EOM(v), but its EQUATION has no derivative of v: which ROLE does it have?]]]',
'eom/findings/role/prose-known': '[OK,[[ROLE MISMATCH,PZ,z,KNOWN,LAW PZ declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/spring_draft_eomz': '[OK,[[ROLE MISMATCH,EOM_Z,z,KNOWN,LAW EOM_Z declares ROLE EOM(z), but z is known (FIXED): which ROLE does it have?]]]',
'eom/findings/spring_gravity_unbound': '[OK,[[CLOSED,EOM_Z,[m],LAW EOM_Z names no unknown once the fixed DOFs are applied, and depends on m, which the kernel does not bind: does it hold for every value of m, or is a force or an unknown missing?]]]',
'eom/findings/switch/off-not-read': '[OK,[[UNDER,x,[v,x],[N2],unknown x is determined by no law with a declared form (LAW N2 leaves v, x under-determined): which equation determines x?]]]',
'eom/findings/under/all-closed': '[OK,[[UNDER,x,[x],[],unknown x is named by no law with a declared form: which equation determines x?]]]',
'eom/findings/under/invariant-only': '[OK,[[UNDER,x,[x],[],unknown x is named by no law with a declared form: which equation determines x?]]]',
'eom/findings/under/name-tier': '[OK,[[UNDER,x,[v,x],[L],unknown x is determined by no law with a declared form (LAW L leaves v, x under-determined): which equation determines x?]]]',
'eom/findings/under/role-tier': '[OK,[[UNDER,v,[v,x],[L],unknown v is determined by no law with a declared form (LAW L leaves v, x under-determined): which equation determines v?]]]',
'eom/findings/under/sigma-tier': '[OK,[[UNDER,v,[v,x],[L],unknown v is determined by no law with a declared form (LAW L leaves v, x under-determined): which equation determines v?]]]',
'eom/findings/under/two-blocks': '[OK,[[UNDER,b,[a,b],[P1],unknown b is determined by no law with a declared form (LAW P1 leaves a, b under-determined): which equation determines b?],[UNDER,d,[c,d],[P2],unknown d is determined by no law with a declared form (LAW P2 leaves c, d under-determined): which equation determines d?]]]',
'eom/findings/zero/divide-by-derivative': '[OK,[[CLOSED,L,[k],LAW L names no unknown once the fixed DOFs are applied, and depends on k, which the kernel does not bind: does it hold for every value of k, or is a force or an unknown missing?]]]',
'eom/findings/zero/input-in-closed-law': '[OK,[[CLOSED,L,[xi],LAW L names no unknown once the fixed DOFs are applied, and depends on xi, which the kernel does not bind: does it hold for every value of xi, or is a force or an unknown missing?]]]',
'eom/findings/zero/removed-derivative': '[OK,[[CLOSED,L,[t,w],LAW L names no unknown once the fixed DOFs are applied, and depends on t, w, which the kernel does not bind: does it hold for every value of t, w, or is a force or an unknown missing?]]]',
'eom/findings/zero/value-nonzero-product': '[OK,[[CLOSED,L,[k],LAW L names no unknown once the fixed DOFs are applied, and depends on k, which the kernel does not bind: does it hold for every value of k, or is a force or an unknown missing?]]]',
'eom/findings/zero/variable-in-closed-law': '[OK,[[CLOSED,L,[t],LAW L names no unknown once the fixed DOFs are applied, and depends on t, which the kernel does not bind: does it hold for every value of t, or is a force or an unknown missing?]]]',
'eom/map/A01': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[FREE_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A03b': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[N_z,DETERMINED,N2Z],[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[N_z,v,x],[KIN,N2,N2Z]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0],[N2Z,0]],[[N_z,0],[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A03c': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[N2Z,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A07': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[lam,DETERMINED,NX],[t,INDEPENDENT,],[vx,DETERMINED,KX],[vy,DETERMINED,NY],[x,DETERMINED,ROD],[y,DETERMINED,KY]]],[PARTS,[UNDER,[],[]],[SQUARE,[lam,vx,vy,x,y],[KX,KY,NX,NY,ROD]],[OVER,[],[]]],[INDEX,3],[INITIAL_VALUES,2],[OFFSETS,[[KX,1],[KY,1],[NX,0],[NY,0],[ROD,2]],[[lam,0],[vx,1],[vy,1],[x,2],[y,2]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A09': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[F1,DETERMINED,FX],[F2,DETERMINED,FY]]],[PARTS,[UNDER,[],[]],[SQUARE,[F1,F2],[FX,FY]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,0],[OFFSETS,[[FX,0],[FY,0]],[[F1,0],[F2,0]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A10a': '[OK,[[ANALYSIS,PDE],[D_VARIABLES,[X,t]],[MAP,[[X,INDEPENDENT,],[t,INDEPENDENT,],[u,NOT ANALYZED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A10b': '[OK,[[ANALYSIS,NO FORM],[D_VARIABLES,[]],[MAP,[[X,NO LAW,],[t,NO LAW,],[u,NO LAW,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[HEAT,[X,t,u]]]]]]',
'eom/map/A12': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,UNDER,N2],[x,NO LAW,]]],[PARTS,[UNDER,[v,x],[N2]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A13': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[EN]],[PROSE,[]]]]',
'eom/map/A14': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,N2],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[KIN,N2,N2D]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A15': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[y,UNDER,KIN]]],[PARTS,[UNDER,[v,y],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[N2,[v,y]]]]]]',
'eom/map/A17a': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[h,DETERMINED,KIN],[m_r,DETERMINED,BURN],[t,INDEPENDENT,],[v,DETERMINED,THRUST]]],[PARTS,[UNDER,[],[]],[SQUARE,[h,m_r,v],[BURN,KIN,THRUST]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,3],[OFFSETS,[[BURN,0],[KIN,0],[THRUST,0]],[[h,1],[m_r,1],[v,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A18': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,FALL],[y,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,y],[FALL,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[FALL,0],[KIN,0]],[[v,1],[y,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[IMPACT,[v,y]]]]]]',
'eom/map/A20': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[xi,INPUT,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A20_no_input': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,UNDER,N2],[x,UNDER,KIN],[xi,NO LAW,]]],[PARTS,[UNDER,[v,x,xi],[KIN,N2]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[NOISE,[xi]]]]]]',
'eom/map/A21': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[tau]],[MAP,[[V,DETERMINED,N2],[X,DETERMINED,KIN],[tau,INDEPENDENT,]]],[PARTS,[UNDER,[],[]],[SQUARE,[V,X],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[V,1],[X,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A23': '[OK,[[ANALYSIS,NO FORM],[D_VARIABLES,[]],[MAP,[[t,NO LAW,],[x,NO LAW,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[DDE,[t,x]]]]]]',
'eom/map/A25': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,N2],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[IC,KIN,N2]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A26': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[w,NO LAW,],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[w],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A27a': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[a,OVER,P2],[b,UNDER,P1],[c,NO LAW,]]],[PARTS,[UNDER,[b,c],[P1]],[SQUARE,[],[]],[OVER,[a],[P2,P3]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/A28': '[OK,[[ANALYSIS,NO FORM],[D_VARIABLES,[]],[MAP,[[v,NO LAW,],[x,NO LAW,],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[KIN,[v,x]],[N2,[v,x]]]]]]',
'eom/map/E01': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]]]',
'eom/map/E02': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[W0DEF,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/E03': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,N2],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[KIN,N2,N2B]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/E03_shape': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,N2],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[KIN,N2,N2B]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/corner_coulomb': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[F_n,DETERMINED,EOM_Z],[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[F_n,v,x],[EOM_X,EOM_Z,KIN]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[EOM_Z,0],[KIN,0]],[[F_n,0],[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/corner_fix_t': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,FIXED,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/corner_no_eom_x': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN],[z,FIXED,]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/dvar/constant-variable': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[k]],[MAP,[[v,DETERMINED,N2],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/dvar/scaled-time': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[tau]],[MAP,[[V,DETERMINED,N2],[X,DETERMINED,KIN],[tau,INDEPENDENT,]]],[PARTS,[UNDER,[],[]],[SQUARE,[V,X],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[V,1],[X,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/dvar/several-pde': '[OK,[[ANALYSIS,PDE],[D_VARIABLES,[X,t]],[MAP,[[X,INDEPENDENT,],[t,INDEPENDENT,],[u,NOT ANALYZED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/dvar/three-variables': '[OK,[[ANALYSIS,PDE],[D_VARIABLES,[X,Y,t]],[MAP,[[X,INDEPENDENT,],[Y,INDEPENDENT,],[t,INDEPENDENT,],[u,NOT ANALYZED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/g2': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[FREE_Z,ZERO],[GRAV_Z,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/g2c': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,OVER,FREE_Z]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[z],[FREE_Z,GRAV_Z]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/g6': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/noform/no-law-kind': '[OK,[[ANALYSIS,NO FORM],[D_VARIABLES,[]],[MAP,[[x,NO LAW,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/over/two-blocks': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[a,OVER,P1],[b,OVER,P3]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[a,b],[P1,P2,P3,P4]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/prose/invariant-and-constant-only': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[PI]],[PROSE,[]]]]',
'eom/map/pryce/empty-square': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,UNDER,N2],[x,NO LAW,]]],[PARTS,[UNDER,[v,x],[N2]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/pryce/index-two': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[x,DETERMINED,C],[y,DETERMINED,K]]],[PARTS,[UNDER,[],[]],[SQUARE,[x,y],[C,K]],[OVER,[],[]]],[INDEX,2],[INITIAL_VALUES,0],[OFFSETS,[[C,1],[K,0]],[[x,1],[y,0]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/pryce/second-order': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[x,DETERMINED,N2]]],[PARTS,[UNDER,[],[]],[SQUARE,[x],[N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[N2,0]],[[x,2]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/pryce/third-order': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[x,DETERMINED,J]]],[PARTS,[UNDER,[],[]],[SQUARE,[x],[J]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,3],[OFFSETS,[[J,0]],[[x,3]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/role/no-derivative': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,L],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,L]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,1],[OFFSETS,[[KIN,0],[L,0]],[[v,0],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_draft': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_draft_eomz': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_gravity_unbound': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_ic2_gap': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[y,DETERMINED,EOM_Y],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x,y],[EOM_X,EOM_Y,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,4],[OFFSETS,[[EOM_X,0],[EOM_Y,0],[KIN,0]],[[v,1],[x,1],[y,2]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_mistakes_final': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/spring_track_draft': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[F_n,DETERMINED,EOM_Z],[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[F_n,v,x],[EOM_X,EOM_Z,KIN]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[EOM_Z,0],[KIN,0]],[[F_n,0],[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/switch/off-not-read': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/under/two-blocks': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[a,UNDER,P1],[b,NO LAW,],[c,UNDER,P2],[d,NO LAW,]]],[PARTS,[UNDER,[a,b,c,d],[P1,P2]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/unread/other-kinds': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,EOM_X],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[EOM_X,KIN]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[EOM_X,0],[KIN,0]],[[v,1],[x,1]]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/unread/remove-value': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,N2],[x,REMOVED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v],[KIN,N2]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[[IC,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/cos-of-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/derivative-over': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/derivative-times': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/divide-by-derivative': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/exp-of-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/functions-to-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/invariant-not-closed': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[L]],[PROSE,[]]]]',
'eom/map/zero/literal-zero-spelled': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/literal-zero-times-unknown': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/ln-of-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/multiplier-kept': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[F_n,DETERMINED,L],[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[F_n,v,x],[KIN,L,N2]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[L,0],[N2,0]],[[F_n,0],[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/power-negative': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/power-of-sum': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/power-positive': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/power-root': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/removed-derivative': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[w,REMOVED,],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/sum-not-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/two-fixes-one-nonzero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-minus-zero': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-nonzero-bound': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-nonzero-product': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,UNBOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-one-alone': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,BOUND]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-zero-alone': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-zero-product': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/map/zero/value-zero-spelled': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,N2]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[N2,0]],[[v,1],[x,1]]],[CLOSED,[[L,ZERO]]],[INVARIANT,[]],[PROSE,[]]]]',
'eom/register/a10a-pde-tfk': '[OK,[[ANALYSIS,PDE],[D_VARIABLES,[X,t]],[MAP,[[X,INDEPENDENT,],[t,INDEPENDENT,],[u,NOT ANALYZED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]],[[PDE,[X,t],PDE: not analyzed]],[USED,[RR-1]],[SETTLED,[]],[OPEN,[]]]',
'eom/register/a12-settled': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,N2],[x,DETERMINED,RR-1]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[N2,RR-1]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[N2,0],[RR-1,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]],[],[USED,[RR-1]],[SETTLED,[x]],[OPEN,[]]]',
'eom/register/a23-noform-with-records': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[x,DETERMINED,RR-1]]],[PARTS,[UNDER,[],[]],[SQUARE,[x],[RR-1]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,1],[OFFSETS,[[RR-1,0]],[[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[DDE,[x]]]]],[[PROSE,DDE,[x],LAW DDE (ROLE EOM(x)) has no EQUATION and names the unknown x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-1]],[SETTLED,[]],[OPEN,[]]]',
'eom/register/a27a-settled-by-other': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[a,OVER,P2],[b,DETERMINED,RR-1],[c,DETERMINED,P1]]],[PARTS,[UNDER,[],[]],[SQUARE,[b,c],[P1,RR-1]],[OVER,[a],[P2,P3]]],[INDEX,1],[INITIAL_VALUES,0],[OFFSETS,[[P1,0],[RR-1,0]],[[b,0],[c,0]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]],[[OVER,[P2,P3],[a],LAWs P2, P3 give more equations than the unknown a they determine: which law is implied by the others, or is one an independent claim?]],[USED,[RR-1]],[SETTLED,[c]],[OPEN,[]]]',
'eom/register/e01-duplicate-eom': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,RR-1],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[KIN,RR-1,RR-2]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[OVER-EOM,v,[RR-1,RR-2],RECORDs RR-1, RR-2 each state the motion of v: are they one equation, or is one to be removed?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-1,RR-2]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/e01-initial-value-assumption': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,RR-1],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,RR-1]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[RR-1,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-1]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/e01-initial-value-with-role': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,RR-1],[x,OVER,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[KIN,RR-1,RR-7]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[OVER,[KIN,RR-1,RR-7],[v,x],LAW KIN and RECORDs RR-1, RR-7 give more equations than the unknowns v, x they determine: which law is implied by the others, or is one an independent claim?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-1,RR-7]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/e01-invariant-role': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-no-equation': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-no-records': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-no-role': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-record-order-withdrawn': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,RR-9],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,RR-9]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[RR-9,0]],[[v,1],[x,1]]],[CLOSED,[[AB-3,BOUND],[RR-10,UNBOUND]]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[CLOSED,RR-10,[k_s,m],RECORD RR-10 names no unknown once the fixed DOFs are applied, and depends on k_s, m, which the kernel does not bind: does it hold for every value of k_s, m, or is a force or an unknown missing?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[AB-3,RR-9,RR-10]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/e01-record-pde': '[OK,[[ANALYSIS,PDE],[D_VARIABLES,[k_s,t]],[MAP,[[t,INDEPENDENT,],[v,NOT ANALYZED,],[x,NOT ANALYZED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,NONE],[INITIAL_VALUES,NONE],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?],[PDE,[k_s,t],PDE: not analyzed]],[USED,[RR-1,RR-5]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-settled': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,RR-1],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,RR-1]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[RR-1,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-1]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/e01-stale-held': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-stale-withdrawn': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-stale-refuted': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,NO LAW,],[x,UNDER,KIN]]],[PARTS,[UNDER,[v,x],[KIN]],[SQUARE,[],[]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[UNDER,v,[v,x],[KIN],unknown v is determined by no law with a declared form (LAW KIN leaves v, x under-determined): which equation determines v?],[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[]],[SETTLED,[]],[OPEN,[v]]]',
'eom/register/e01-standing-words': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,DETERMINED,RR-3],[x,DETERMINED,KIN]]],[PARTS,[UNDER,[],[]],[SQUARE,[v,x],[KIN,RR-3]],[OVER,[],[]]],[INDEX,0],[INITIAL_VALUES,2],[OFFSETS,[[KIN,0],[RR-3,0]],[[v,1],[x,1]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[[ACTION,[v,x]]]]],[[PROSE,ACTION,[v,x],LAW ACTION (ROLE EOM(v)) has no EQUATION and names the unknowns v, x: its equation is outside the analysis; can it be declared in form?]],[USED,[RR-3]],[SETTLED,[v]],[OPEN,[]]]',
'eom/register/spring-regular-unchanged': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[t]],[MAP,[[t,INDEPENDENT,],[v,OVER,EOM_X],[x,OVER,KIN],[z,FIXED,]]],[PARTS,[UNDER,[],[]],[SQUARE,[],[]],[OVER,[v,x],[EOM_X,KIN,RR-1]]],[INDEX,0],[INITIAL_VALUES,0],[OFFSETS,[],[]],[CLOSED,[[EOM_Z,ZERO]]],[INVARIANT,[]],[PROSE,[]]],[[OVER-EOM,v,[EOM_X,RR-1],LAW EOM_X and RECORD RR-1 each state the motion of v: are they one equation, or is one to be removed?]],[USED,[RR-1]],[SETTLED,[]],[OPEN,[]]]',
'eom/register/under-block-partial': '[OK,[[ANALYSIS,RUN],[D_VARIABLES,[]],[MAP,[[a,DETERMINED,RR-1],[b,UNDER,P1],[c,NO LAW,],[d,NO LAW,]]],[PARTS,[UNDER,[b,c,d],[P1]],[SQUARE,[a],[RR-1]],[OVER,[],[]]],[INDEX,1],[INITIAL_VALUES,0],[OFFSETS,[[RR-1,0]],[[a,0]]],[CLOSED,[]],[INVARIANT,[]],[PROSE,[]]],[[UNDER,c,[b,c],[P1],unknown c is determined by no law with a declared form (LAW P1 leaves b, c under-determined): which equation determines c?],[UNDER,d,[d],[],unknown d is named by no law with a declared form: which equation determines d?]],[USED,[RR-1]],[SETTLED,[]],[OPEN,[b,c,d]]]',
}
# ---- 0.1.2 (C-MS-5; increment 11): a JSON {} and a JSON [] are told apart -------------
# Expectations by hand from tpc_eom's readers (_read, _kind, _read_records, eom_class's
# switch reading): the first shape problem refuses. Each case is one an assoc-array
# reading answered otherwise, or a valid empty object.
_X = {"NAME": "x", "DIMENSION": "L1"}
case("decode/map-tpk-list", "eom_map", {"tfk": {"TPK": []}}, R("TPK: zone is not an object"))
case("decode/map-kind-object", "eom_map", {"tfk": {"TPK": {"DOF": {}}}}, R("TPK kind DOF is not a list"))
case("decode/map-kind-zero-keyed", "eom_map", {"tfk": {"TPK": {"DOF": {"0": _X}}}}, R("TPK kind DOF is not a list"))
case("decode/map-entry-list", "eom_map", {"tfk": {"TPK": {"DOF": [[]]}}}, R("TPK kind DOF: entry is not an object"))
case("decode/findings-kind-object", "eom_findings", {"tfk": {"TPK": {"DOF": [_X], "LAW": {}}}},
R("TPK kind LAW is not a list"))
case("decode/map-tfk-list", "eom_map", {"tfk": []}, R("TFK is not an object"))
case("decode/class-tms-list", "eom_class", {"tfk": {"TPK": {}, "TMS": []}}, R("TMS: zone is not an object"))
case("decode/class-parameters-list", "eom_class", {"tfk": {"TPK": {}, "TMS": {"PARAMETERS": []}}},
R("TMS: part PARAMETERS is not an object"))
case("decode/class-parameters-empty-object", "eom_class", {"tfk": {"TPK": {}, "TMS": {"PARAMETERS": {}}}},
"[STRUCTURE,Structure not Validated at Inception,[NO FORM]]",
note="an empty PARAMETERS object: STRUCTURE_CHECK absent, so ON; the empty kernel carries no form, so it "
"is not structurally regular (S30: forms present)")
case("decode/class-parameters-zero-keyed", "eom_class", {"tfk": {"TPK": {}, "TMS": {"PARAMETERS": {"0": "OFF"}}}},
"[STRUCTURE,Structure not Validated at Inception,[NO FORM]]",
note="a key 0 is not STRUCTURE_CHECK, so ON (it read as a list and was refused)")
case("decode/register-records-object", "eom_register_test", {"tfk": {"TPK": {"DOF": [_X]}}, "records": {}},
R("records is not a list"))
case("decode/register-records-zero-keyed", "eom_register_test",
{"tfk": {"TPK": {"DOF": [_X]}}, "records": {"0": {"ID": "RR-1", "STATUS": "PROVISIONAL"}}},
R("records is not a list"))
case("decode/register-record-entry-list", "eom_register_test", {"tfk": {"TPK": {"DOF": [_X]}}, "records": [[]]},
R("records: entry is not an object"))
def dispatch(fn, i):
import tpc_eom as E
if fn == "eom_map":
return E.eom_map(i["tfk"])
if fn == "eom_findings":
return E.eom_findings(i["tfk"])
if fn == "eom_class":
return E.eom_class(i["tfk"])
if fn == "eom_register_test":
return E.eom_register_test(i["tfk"], i["records"])
raise KeyError(fn)
def expectation(cs, hand):
cid = cs["id"]
if isinstance(hand, str):
assert cid not in EXPECTED, "a hand literal and a table literal for " + cid
return hand
exp = EXPECTED[cid]
if hand is not None:
for sub in hand[1]:
assert sub in exp, "hand fact %r missing from the literal of %s" % (sub, cid)
return exp
if __name__ == "__main__":
unchecked = "--unchecked" in sys.argv
out, bad = [], 0
for cs, hand in cases:
cs = dict(cs)
cs["expect"] = expectation(cs, hand)
if not unchecked:
try:
got = S.canon(dispatch(cs["fn"], cs["input"]))
except Exception as e:
got = "ERROR: %s" % e
if got != cs["expect"]:
bad += 1
print("MISMATCH", cs["id"], "\n expect", cs["expect"], "\n got ", got)
out.append(cs)
unused = set(EXPECTED) - set(cs["id"] for cs, _ in cases)
assert not unused, sorted(unused)
if bad:
sys.exit("refusing to write: %d mismatches" % bad)
corpus = {
"meta": {
"name": "tpc_eom_corpus", "version": "0.2.0",
"status": "PROPOSED 2026-09-26 (D176.1 and D177.1, taken 2026-09-26; standing rulings S22-S31); "
"awaiting the supervisor's verification",
"conforms_tps": "0.2.0 (v15), with the schema 0.5.0 contract of BRIEF_COMMON_P4 section 2 and the "
"D-variable rules of its section 3",
"module": "tpc_eom 0.1.1 (proposed with TPC-PY 0.2.0; reads with tpc_zone's helpers and tpc_form's public form_tree, S32)",
"note": ("A refusal and every eom_class answer is hand-derived; every other expectation comes from an "
"independent brute-force oracle and holds the hand facts of its case. The fixtures are the "
"EOM round's research drafts with a ROLE on every LAW (role table: tpm_eom_check 0.1.0, "
"section 8) and synthetic kernels; test fixtures, not physics under research. T1, T3, T4 "
"and the zone checks are not re-run here: some fixtures are ones the gate refuses, which "
"the notes say. Both residences MUST reproduce every expect. 0.1.1 (agent R4, the "
"cross-check): every fixture tpc_zone 0.5.0 refused that is not refused on purpose now "
"passes it zone by zone: A10a and the synthetic three-variable and per-law PDE kernels "
"declare D_VARIABLES SEVERAL (D177.1); dvar/one-with-two sets ONE explicitly. The fixtures "
"still outside tpc_zone are refused on purpose: the refusal cases, corner_fix_t (a FIXed "
"clock), a CONSTANT as D variable, ONE with two D variables, and the what-is-not-read and "
"switch cases whose TPK or fields are malformed. No expectation moves. 0.1.2 (C-MS-5, "
"increment 11, 2026-09-28): 13 decode/ cases, hand-derived, a JSON {} and [] and an object "
"keyed 0 read as written in both residences; no earlier expectation moves.")
},
"cases": out,
}
open(os.path.join(HERE, "vectors", "eom_corpus.json"), "w", encoding="utf-8", newline="\n").write(
json.dumps(corpus, indent=1, ensure_ascii=True) + "\n")
print("wrote", len(out), "eom cases;", "UNCHECKED (vectors first)" if unchecked else
"all match the module")