The actual matched-width look-ahead output law

Push the conditionally factored source through the concrete three-call look-ahead program. Retain the transcript, the entire right state, and both honest and tampered first outputs together with the honest second output. The two inputs on each side may be arbitrary functions of that side state.

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopLookAheadWeight (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) : ((Z × B) × (Fin (matchedBlockSeedBits L) → Bool) × (Fin (matchedBlockSeedBits L) → Bool)) × (Fin (matchedBlockSeedBits L) → Bool) → ℝ

The actual second output with the full right state and both first outputs retained.

Equations

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