Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_02 : branchClaimRootValidB 0 2 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 2).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_4_20 : branchClaimRootValidB 4 20 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (4, 20).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_08 : branchClaimRootValidB 1 8 (BranchClaim.search branchClaims1Row8) = true

Root audit for fixed branch (1, 8).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_09 : branchClaimRootValidB 1 9 (BranchClaim.search branchClaims1Row9) = true

Root audit for fixed branch (1, 9).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_08_00000 : nodeClaimChunkValidB branchClaims1Row8 0 64 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_08_00064 : nodeClaimChunkValidB branchClaims1Row8 64 64 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_08_00128 : nodeClaimChunkValidB branchClaims1Row8 128 18 = true

Node audit for fixed branch (1, 8), starting at 128.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_09_00000 : nodeClaimChunkValidB branchClaims1Row9 0 64 = true

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