Freiman.section14_s0013_coverage0005_parentidx0170_specs_0000_0008
ProvedFreiman.section14_s0013_coverage0005_parentidx0170_specs_0000_0008hall-raynumber-theory
Exact auxiliary assertion from Freiman section 14. ∀ gs ∈ (((section14State section14Catalog 13).plans[5]?.getD (⟨0,0,[],false,[]⟩ : Section14Plan)).specs.drop 0).take 8, ∀ j ∈ List.range (section14GoalBranches section14Catalog (section14Goal section14Catalog gs.1)).length, (section14Branch section14Catalog (section14Goal section14Catalog gs.1) j).2 = .automatic ∨ section14Recorded section14Catalog 13 170 gs.1 j
Preamble
import Definitions.Def_Freiman_section14Data open Freiman
Formal statement
theorem Freiman.section14_s0013_coverage0005_parentidx0170_specs_0000_0008 : ∀ gs ∈ (((section14State section14Catalog 13).plans[5]?.getD (⟨0,0,[],false,[]⟩ : Section14Plan)).specs.drop 0).take 8, ∀ j ∈ List.range (section14GoalBranches section14Catalog (section14Goal section14Catalog gs.1)).length, (section14Branch section14Catalog (section14Goal section14Catalog gs.1) j).2 = .automatic ∨ section14Recorded section14Catalog 13 170 gs.1 j := by sorry
Source
Exact finite subclaim supporting the original section14StateValid targets in Freiman M7.