Polynomial-time numbers and tests — one-bit flags

The string facts behind the comparison, connective and case rules of Complexitylib.Classes.P.Unary. Cobham's toolkit already computes the length comparison, the Boolean connectives and a selection by a leading bit in polynomial time; on one-bit strings each of them is the corresponding operation on Bool, which is what lets a verdict be carried as a Bool.

Contents

• lenLeFlag_eq_decide — the length comparison as a decided proposition
• andBit_singleton, orBit_singleton, notBit_singleton — the connectives on one-bit strings
• selectHead_singleton — selection by a one-bit string is an if

theorem Complexity.lenLeFlag_eq_decide (a b : List Bool) : Cobham.lenLeFlag a b = [decide (b.length ≤ a.length)]

The length comparison |b| ≤ |a| outputs its verdict as one bit.

theorem Complexity.andBit_singleton (b c : Bool) : andBit [b] [c] = [b && c]

Conjunction of one-bit strings.

theorem Complexity.orBit_singleton (b c : Bool) : orBit [b] [c] = [b || c]

Disjunction of one-bit strings.

theorem Complexity.notBit_singleton (b : Bool) : notBit [b] = [!b]

Negation of a one-bit string.

theorem Complexity.selectHead_singleton (b : Bool) (x y : List Bool) : Cobham.selectHead [b] x y = if b = true then x else y

Selection by a one-bit string picks the first branch on true and the second on false.