English
Let a be an Args. Then a.Numeric implies P124 a. This is established by well-founded structural induction on a, with case analyses P1 and P24, using IHs for the subcomponents to deduce P124.
Русский
Пусть a — аргумент типа Args. Тогда a.Numeric влечет за собой P124 a. Доказано путем хорошо основанной структурной индукции по a с разбором случаев P1 и P24, используя IH для подчастей, чтобы получить P124.
LaTeX
$$$\\\\forall a:\\\\mathrm{Args}, a.Numeric \\\\rightarrow P_{124}(a).$$$
Lean4
/-- The main chunk of Theorem 8 in [Conway2001] / Theorem 3.8 in [SchleicherStoll]. -/
theorem main (a : Args) : a.Numeric → P124 a :=
by
apply argsRel_wf.induction a
intro a ih ha
replace ih : ∀ a', ArgsRel a' a → P124 a' := fun a' hr ↦ ih a' hr (hr.numeric_closed ha)
cases a with
/- P1 -/
| P1 x y =>
rw [Args.numeric_P1] at ha
exact P1_of_ih ih ha.1 ha.2
| P24 x₁ x₂ y =>
have h₁₂ := ih₁₂ ih
have h₂₁ := ih₂₁ ih
have h4 := ih4 ih
obtain ⟨h₁₂x, h₁₂y⟩ := ih24_neg h₁₂
obtain ⟨h4x, h4y⟩ := ih4_neg h4
refine ⟨fun he ↦ Quotient.sound ?_, fun hl ↦ ?_⟩
· /- P2 -/
rw [Args.numeric_P24] at ha
exact ⟨mul_right_le_of_equiv ha.1 ha.2.1 h₁₂ h₂₁ he, mul_right_le_of_equiv ha.2.1 ha.1 h₂₁ h₁₂ (symm he)⟩
· /- P4 -/
obtain ⟨hn₁, hn₂⟩ := numeric_of_ih ih
obtain ⟨⟨h₁, -⟩, h₂, -⟩ := mulOptionsLTMul_of_numeric hn₂
obtain ⟨⟨-, h₃⟩, -, h₄⟩ := mulOptionsLTMul_of_numeric hn₁
constructor <;> intro <;> refine P3_of_lt ?_ ?_ hl <;> intro <;> apply ih3_of_ih
any_goals assumption
exacts [(ih24_neg h₁₂y).1, (ih4_neg h4y).1]
