The actual scheduled extractor on Boolean source and seed coordinates

Supply both input and seed as fixed-length Boolean vectors, run the actual bit program, and read the output in block order. The seed vector has exactly the previously specified total seed width. This definition invokes no semantic field enumeration or abstract extractor map.

def Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor (n h Q E ell : ℕ) (x : Fin n → Bool) (seed : Fin (scheduledBlockSeedBits n h Q E ell) → Bool) (i : Fin (recursiveBlockCount 1 h)) (j : Fin ell) : Bool

Read the actual scheduled program's output blocks at a Boolean source and seed vector.

Equations

• One or more equations did not get rendered due to their size.