Basic laws for the concrete advice fold

The list fold exposes the order of the advice bits and its exact composition law, without any distributional or size hypotheses.

theorem Algebraic.Cutwidth.Extractor.Internal.adviceFold_nil (n m L e : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) : adviceFold n m L e x y q [] = q

theorem Algebraic.Cutwidth.Extractor.Internal.adviceFold_cons (n m L e : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) (advice : List Bool) : adviceFold n m L e x y q (b :: advice) = adviceFold n m L e x y (flipFlopStep n m L e x y q b) advice

theorem Algebraic.Cutwidth.Extractor.Internal.adviceFold_append (n m L e : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) (first last : List Bool) : adviceFold n m L e x y q (first ++ last) = adviceFold n m L e x y (adviceFold n m L e x y q first) last