Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_07 : branchClaimRootValidB 0 7 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 7).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_4_25 : branchClaimRootValidB 4 25 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (4, 25).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_28 : branchClaimRootValidB 1 28 (BranchClaim.search branchClaims1Row28) = true

Root audit for fixed branch (1, 28).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_29 : branchClaimRootValidB 1 29 (BranchClaim.search branchClaims1Row29) = true

Root audit for fixed branch (1, 29).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_28_00000 : nodeClaimChunkValidB branchClaims1Row28 0 64 = true

Node audit for fixed branch (1, 28), starting at 0.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_28_00064 : nodeClaimChunkValidB branchClaims1Row28 64 56 = true

Node audit for fixed branch (1, 28), starting at 64.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_29_00000 : nodeClaimChunkValidB branchClaims1Row29 0 32 = true

Node audit for fixed branch (1, 29), starting at 0.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_29_00032 : nodeClaimChunkValidB branchClaims1Row29 32 32 = true

Node audit for fixed branch (1, 29), starting at 32.