The answer-reduced decision, on blocks of bits

Piece AR-3e of planning/answer-reduction.md: the decision predicate accepts of MIPRE/Background/AnswerReduction/Predicate, rewritten as a function of the k-bit blocks a program reads (verdictB), with the field arithmetic done by the introspection stage programs: the line-versus-point check (FieldLineCheck.lineCheckProg), the seed selector, and the line representatives the sampler's third stage already uses.

• The low-degree subtests (ldB): of the seeded test's decision, only a point question against a line question of the same copy is ever checked, and there it is the line-versus-point check on the line the question describes (ldB_aline, ldB_dline).
• The five steps (sideB) are organised by what each type pair asks for: at most one comparison of two answer blocks (eqPlan), one low-degree subtest (ldPlan) and one game check (chkPlan), which are functions of the types alone. sideB_eq is side.
• The predicate (verdictB_eq) is the typed predicate typedPred, the answers parsed into blocks (parseB) and the questions' PCP halves split into their three runs.

Lists of blocks

def MIPRE.AnswerReduction.chunks {α : Type u_1} (w : ℕ) : ℕ → List α → List (List α)

A list cut into n consecutive runs of w elements.

Equations

• MIPRE.AnswerReduction.chunks w 0 x✝ = []
• MIPRE.AnswerReduction.chunks w n.succ x✝ = List.take w x✝ :: MIPRE.AnswerReduction.chunks w n (List.drop w x✝)

theorem MIPRE.AnswerReduction.chunks_eq {α : Type u_1} (w n : ℕ) (l : List α) : chunks w n l = List.ofFn fun (c : Fin n) => List.take w (List.drop (↑c * w) l)

theorem MIPRE.AnswerReduction.chunks_ofFn {α : Type u_1} (w n : ℕ) (g : Fin n → Fin w → α) : chunks w n (List.ofFn fun (r : Fin (n * w)) => g (finProdFinEquiv.symm r).1 (finProdFinEquiv.symm r).2) = List.ofFn fun (c : Fin n) => List.ofFn (g c)

The line-versus-point check

noncomputable def MIPRE.AnswerReduction.lvpB (kU : Cost.Unary) (base dir pt : List Cost.BitStr) (polys : List (List Cost.BitStr)) (vals : List Cost.BitStr) : Bool

The line-versus-point check on blocks: every codeword's polynomial, evaluated at the point's parameter on the line, gives the point's value.

Equations

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

theorem MIPRE.AnswerReduction.lineParam_eq {k : ℕ} (hk : 1 ≤ k) {m : ℕ} (u₀ w x : LIDT.Point (SAT.shoupBinField k hk).carrier m) : LIDT.CL.lineParam u₀ w x = Introspection.FieldLineCheck.parameter u₀ w x

theorem MIPRE.AnswerReduction.lvpB_eq {k : ℕ} (hk : 1 ≤ k) {m ldc d : ℕ} [NeZero ldc] (u₀ w x : LIDT.Point (SAT.shoupBinField k hk).carrier m) (f : Fin ldc → LIDT.LinePoly (SAT.shoupBinField k hk).carrier d) (a : Fin ldc → (SAT.shoupBinField k hk).carrier) : lvpB (Cost.unary k) ((SAT.shoupBinField k hk).vecBits u₀) ((SAT.shoupBinField k hk).vecBits w) ((SAT.shoupBinField k hk).vecBits x) (List.ofFn fun (j : Fin ldc) => (SAT.shoupBinField k hk).vecBits (f j)) ((SAT.shoupBinField k hk).vecBits a) = LIDT.CL.lineVsPoint u₀ w x f a

The low-degree subtests of a copy

noncomputable def MIPRE.AnswerReduction.dirB (kU : Cost.Unary) (d : StageProg.Desc) (τ : ℕ) (s : Cost.BitStr) (Y : StageProg.Blocks) : List Cost.BitStr

The direction of the line a question of test type τ describes, from its seed and its blocks: the selected axis, or the selected diagonal direction.

Equations

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

noncomputable def MIPRE.AnswerReduction.ldB (kU : Cost.Unary) (d : StageProg.Desc) (τ : ℕ) (X Y : StageProg.Blocks) (polys : List (List Cost.BitStr)) (vals : List Cost.BitStr) : Bool

The low-degree subtest of a copy d: the point the question with blocks X carries, against the line of test type τ the question with blocks Y carries.

Equations

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

noncomputable def MIPRE.AnswerReduction.blocksV {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (x : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) : StageProg.Blocks

The three runs of blocks of a vector of V^pcp.

Equations

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

theorem MIPRE.AnswerReduction.seedOf_blocksV {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (o sz jw : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (y : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) : StageProg.seedOf (Cost.unary o, Cost.unary sz, Cost.unary jw, Cost.unary ↑c) (blocksV hk P y).2.2 = (SAT.shoupBinField k hk).toBits (y (Pcp.regsAt P o sz c h).coord)

theorem MIPRE.AnswerReduction.pt_blocksV {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (y : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) : Pcp.sliceL (List.length (Cost.unary o)) (List.length (Cost.unary sz)) (blocksV hk P y).1 = (SAT.shoupBinField k hk).vecBits ((Pcp.regsAt P o sz c h).ptOf y)

theorem MIPRE.AnswerReduction.dir_blocksV {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (y : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) : Pcp.sliceL (List.length (Cost.unary o)) (List.length (Cost.unary sz)) (blocksV hk P y).2.1 = (SAT.shoupBinField k hk).vecBits ((Pcp.regsAt P o sz c h).dirOf y)

theorem MIPRE.AnswerReduction.ldB_aline {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (o sz jw : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (hjw : jw ≤ k) (hsz2 : sz = 2 ^ jw) [NeZero sz] {hsz : sz ∣ Fintype.card (SAT.shoupBinField k hk).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField k hk).carrier sz hsz) (hχ : ∀ (a : (SAT.shoupBinField k hk).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField k hk) jw hjw a)) {ldc d : ℕ} [NeZero ldc] (xp xq : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) (av : Fin ldc → (SAT.shoupBinField k hk).carrier) (f : Fin ldc → LIDT.LinePoly (SAT.shoupBinField k hk).carrier d) : ldB (Cost.unary k) (Cost.unary o, Cost.unary sz, Cost.unary jw, Cost.unary ↑c) 1 (blocksV hk P xp) (blocksV hk P xq) (List.ofFn fun (j : Fin ldc) => (SAT.shoupBinField k hk).vecBits (f j)) ((SAT.shoupBinField k hk).vecBits av) = LIDT.CL.accepts hsz (LIDT.CL.Sample.question hsz ((Pcp.regsAt P o sz c h).sampleOf S LIDT.CL.Ty.point xp) LIDT.CL.Ty.point) (LIDT.CL.Sample.question hsz ((Pcp.regsAt P o sz c h).sampleOf S LIDT.CL.Ty.aline xq) LIDT.CL.Ty.aline) (LIDT.CL.Answer.values av) (LIDT.CL.Answer.apolys f)

The axis-parallel subtest.

theorem MIPRE.AnswerReduction.ldB_dline {k : ℕ} (hk : 1 ≤ k) (P : SAT.PcpParams) (o sz jw : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (hjw : jw ≤ k) [NeZero sz] {hsz : sz ∣ Fintype.card (SAT.shoupBinField k hk).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField k hk).carrier sz hsz) (hχ : ∀ (a : (SAT.shoupBinField k hk).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField k hk) jw hjw a)) {ldc d : ℕ} [NeZero ldc] (xp xq : Pcp.Coord P → (SAT.shoupBinField k hk).carrier) (av : Fin ldc → (SAT.shoupBinField k hk).carrier) (f : Fin ldc → LIDT.LinePoly (SAT.shoupBinField k hk).carrier (sz * d)) : ldB (Cost.unary k) (Cost.unary o, Cost.unary sz, Cost.unary jw, Cost.unary ↑c) 2 (blocksV hk P xp) (blocksV hk P xq) (List.ofFn fun (j : Fin ldc) => (SAT.shoupBinField k hk).vecBits (f j)) ((SAT.shoupBinField k hk).vecBits av) = LIDT.CL.accepts hsz (LIDT.CL.Sample.question hsz ((Pcp.regsAt P o sz c h).sampleOf S LIDT.CL.Ty.point xp) LIDT.CL.Ty.point) (LIDT.CL.Sample.question hsz ((Pcp.regsAt P o sz c h).sampleOf S LIDT.CL.Ty.dline xq) LIDT.CL.Ty.dline) (LIDT.CL.Answer.values av) (LIDT.CL.Answer.dpolys f)

The diagonal subtest.

Answers as blocks

noncomputable def MIPRE.AnswerReduction.ansB {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} (u : Ans P (SAT.shoupBinField k hk).carrier) : List Cost.BitStr

The blocks of an answer: its elements' bits.

Equations

• MIPRE.AnswerReduction.ansB hk u = List.map (MIPRE.SAT.shoupBinField k hk).toBits (MIPRE.AnswerReduction.elems (MIPRE.SAT.shoupBinField k hk) u)

theorem MIPRE.AnswerReduction.ofFn_getD {k : ℕ} (hk : 1 ≤ k) (l : List (SAT.shoupBinField k hk).carrier) {N : ℕ} (hN : l.length = N) : (List.ofFn fun (r : Fin N) => l.getD (↑r) 0) = l

theorem MIPRE.AnswerReduction.elems_ofElems {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} (t : Pcp.PcpTy) (l : List (SAT.shoupBinField k hk).carrier) (hl : l.length = cnt P t) : elems (SAT.shoupBinField k hk) (ofElems (SAT.shoupBinField k hk) t l) = l

theorem MIPRE.AnswerReduction.ansB_injective {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} {t : Pcp.PcpTy} {u v : Ans P (SAT.shoupBinField k hk).carrier} (hu : ansFmt t u = true) (hv : ansFmt t v = true) (h : ansB hk u = ansB hk v) : u = v

theorem MIPRE.AnswerReduction.ansB_ofElems {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} (t : Pcp.PcpTy) (bs : List Cost.BitStr) (hl : bs.length = cnt P t) (hw : ∀ b ∈ bs, List.length b = k) : ansB hk (ofElems (SAT.shoupBinField k hk) t (List.map (SAT.shoupBinField k hk).ofBits bs)) = bs

theorem MIPRE.AnswerReduction.ansB_val1 {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} {i : Fin 6} (hi : ↑i < 5) {u : Ans P (SAT.shoupBinField k hk).carrier} (hu : ansFmt (i, LIDT.CL.Ty.point) u = true) : ∃ (av : Fin 1 → (SAT.shoupBinField k hk).carrier), u = Sum.inl (LIDT.CL.Answer.values av) ∧ ansB hk u = (SAT.shoupBinField k hk).vecBits av ∧ val1 u = av 0

A point answer of the first five copies is one block.

theorem MIPRE.AnswerReduction.ansB_val6 {k : ℕ} (hk : 1 ≤ k) {P : SAT.PcpParams} {i : Fin 6} (hi : ↑i = 5) {u : Ans P (SAT.shoupBinField k hk).carrier} (hu : ansFmt (i, LIDT.CL.Ty.point) u = true) : ∃ (av : Fin (P.m' + 6) → (SAT.shoupBinField k hk).carrier), u = Sum.inr (LIDT.CL.Answer.values av) ∧ ansB hk u = (SAT.shoupBinField k hk).vecBits av ∧ vals6 u = av ∧ ∀ (j : Fin (P.m' + 6)), val6 j u = av j

A point answer of the sixth copy is its m' + 6 blocks.

theorem MIPRE.AnswerReduction.getD_vecBits {k : ℕ} (hk : 1 ≤ k) {N : ℕ} (v : Fin N → (SAT.shoupBinField k hk).carrier) (j : Fin N) : ((SAT.shoupBinField k hk).vecBits v).getD ↑j [] = (SAT.shoupBinField k hk).toBits (v j)

theorem MIPRE.AnswerReduction.getD_vecBits' {k : ℕ} (hk : 1 ≤ k) {N : ℕ} (v : Fin N → (SAT.shoupBinField k hk).carrier) (j : ℕ) (hj : j < N) : ((SAT.shoupBinField k hk).vecBits v).getD j [] = (SAT.shoupBinField k hk).toBits (v ⟨j, hj⟩)

theorem MIPRE.AnswerReduction.toBits_injective {k : ℕ} (hk : 1 ≤ k) : Function.Injective (SAT.shoupBinField k hk).toBits

The atoms of the five steps, for a family

def MIPRE.AnswerReduction.width (m' : ℕ) (τ : LIDT.CL.Ty) : ℕ

The number of coefficients of a polynomial of the sixth copy's line answers.

Equations

• MIPRE.AnswerReduction.width m' τ = if τ = MIPRE.LIDT.CL.Ty.aline then MIPRE.AnswerReduction.dPcp + 1 else m' * MIPRE.AnswerReduction.dPcp + 1

theorem MIPRE.AnswerReduction.atom_val6_val1 (F : PcpFamily) (n : ℕ) {i i' : Fin 6} (hi : ↑i = 5) (hi' : ↑i' < 5) {u v : Ans (F.par n) (fld (F.par n) ⋯).carrier} (hu : ansFmt (i, LIDT.CL.Ty.point) u = true) (hv : ansFmt (i', LIDT.CL.Ty.point) v = true) (j : Fin ((F.par n).m' + 6)) : decide (val6 j u = val1 v) = decide ((ansB ⋯ u).getD ↑j [] = (ansB ⋯ v).getD 0 [])

theorem MIPRE.AnswerReduction.atom_val1_val6 (F : PcpFamily) (n : ℕ) {i i' : Fin 6} (hi : ↑i < 5) (hi' : ↑i' = 5) {u v : Ans (F.par n) (fld (F.par n) ⋯).carrier} (hu : ansFmt (i, LIDT.CL.Ty.point) u = true) (hv : ansFmt (i', LIDT.CL.Ty.point) v = true) (j : Fin ((F.par n).m' + 6)) : decide (val1 u = val6 j v) = decide ((ansB ⋯ u).getD 0 [] = (ansB ⋯ v).getD ↑j [])

theorem MIPRE.AnswerReduction.ofFn_one_vecBits (F : PcpFamily) (n : ℕ) {N : ℕ} (g : Fin 1 → Fin N → (fld (F.par n) ⋯).carrier) : [(fld (F.par n) ⋯).vecBits (g 0)] = List.ofFn fun (j : Fin 1) => (fld (F.par n) ⋯).vecBits (g j)

theorem MIPRE.AnswerReduction.atom_ld1 (F : PcpFamily) (n : ℕ) (c : Fin 5) {τ' : LIDT.CL.Ty} (hτ' : τ' ≠ LIDT.CL.Ty.point) {u v : Ans (F.par n) (fld (F.par n) ⋯).carrier} (hu : ansFmt (c.castSucc, LIDT.CL.Ty.point) u = true) (hv : ansFmt (c.castSucc, τ') v = true) (x y : Pcp.Coord (F.par n) → (fld (F.par n) ⋯).carrier) : LIDT.CL.accepts ⋯ (q1 (F.sel n) c LIDT.CL.Ty.point x) (q1 (F.sel n) c τ' y) (ans1 u) (ans1 v) = ldB (Cost.unary (F.par n).k) (F.desc n c.castSucc) (StageProg.tyNat τ') (blocksV ⋯ (F.par n) x) (blocksV ⋯ (F.par n) y) [ansB ⋯ v] (ansB ⋯ u)

The low-degree subtest of a copy c ≤ 5, on blocks.

theorem MIPRE.AnswerReduction.atom_ld6 (F : PcpFamily) (n : ℕ) {i : Fin 6} (hi : ↑i = 5) {τ' : LIDT.CL.Ty} (hτ' : τ' ≠ LIDT.CL.Ty.point) {u v : Ans (F.par n) (fld (F.par n) ⋯).carrier} (hu : ansFmt (i, LIDT.CL.Ty.point) u = true) (hv : ansFmt (i, τ') v = true) (x y : Pcp.Coord (F.par n) → (fld (F.par n) ⋯).carrier) : LIDT.CL.accepts ⋯ (q6 (F.sel' n) LIDT.CL.Ty.point x) (q6 (F.sel' n) τ' y) (ans6 u) (ans6 v) = ldB (Cost.unary (F.par n).k) (F.desc n 5) (StageProg.tyNat τ') (blocksV ⋯ (F.par n) x) (blocksV ⋯ (F.par n) y) (chunks (width (F.par n).m' τ') ((F.par n).m' + 6) (ansB ⋯ v)) (ansB ⋯ u)

The low-degree subtest of the sixth copy, on blocks.

The five steps, planned by the types

def MIPRE.AnswerReduction.eqPlan (p q : ArTy) : Option (ℕ × ℕ)

The comparison of two answer blocks a type pair asks for: step 2, an oracle's Point_6 component against an isolated player's Point_v, or step 4, a copy's point against the oracle's Point_6 component.

Equations

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

def MIPRE.AnswerReduction.ldPlan (p q : ArTy) : Option (ℕ × Bool)

The low-degree subtest a type pair asks for: the copy, and whether the line answers carry m' + 6 codewords (the sixth copy).

Equations

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

def MIPRE.AnswerReduction.chkPlan (p : ArTy) : Bool

Whether a type asks for the game check: an oracle's Point_6.

Equations

• MIPRE.AnswerReduction.chkPlan p = decide (p.1 = MIPRE.Role.oracle ∧ ↑p.2.1 = 5 ∧ p.2.2 = MIPRE.LIDT.CL.Ty.point)

noncomputable def MIPRE.AnswerReduction.sideB (kU m'U : Cost.Unary) (descs : List StageProg.Desc) (chk : Bool) (p q : ArTy) (X Y : StageProg.Blocks) (A B : List Cost.BitStr) : Bool

One side of the five steps, on blocks, as its type pair plans it. chk is the game check's verdict.

Equations

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

theorem MIPRE.AnswerReduction.chk_eq {C : Prop} [Decidable C] {chk c : Bool} (h : C → chk = c) : (!decide C || chk) = if C then c else true

theorem MIPRE.AnswerReduction.getD_desc (F : PcpFamily) (n : ℕ) (c : Fin 6) : (List.ofFn (F.desc n)).getD (↑c) default = F.desc n c

theorem MIPRE.AnswerReduction.sideB_eq (F : PcpFamily) (n : ℕ) {X : Type u_1} (check : X → (Fin (F.par n).m' → Fq (F.par n) ⋯) → (Fin ((F.par n).m' + 6) → Fq (F.par n) ⋯) → Bool) (p q : Q (F.par n) (Fq (F.par n) ⋯) X) (u v : Ans (F.par n) (Fq (F.par n) ⋯)) (hu : ansFmt p.1.2 u = true) (hv : ansFmt q.1.2 v = true) (chk : Bool) (hchk : chkPlan p.1 = true → chk = check p.2.1 ((Pcp.regs6 (F.par n)).ptOf p.2.2) (vals6 u)) : sideB (Cost.unary (F.par n).k) (Cost.unary (F.par n).m') (List.ofFn (F.desc n)) chk p.1 q.1 (blocksV ⋯ (F.par n) p.2.2) (blocksV ⋯ (F.par n) q.2.2) (ansB ⋯ u) (ansB ⋯ v) = side (F.sel n) (F.sel' n) check p q u v

Parsing, and the predicate

def MIPRE.AnswerReduction.cntB (m m' : ℕ) (t : Pcp.PcpTy) : ℕ

The number of field elements of an answer of the type t, from m and m' (cnt).

Equations

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

theorem MIPRE.AnswerReduction.cnt_eq (P : SAT.PcpParams) (t : Pcp.PcpTy) : cnt P t = cntB P.m P.m' t

def MIPRE.AnswerReduction.parseB (k c : ℕ) (s : Cost.BitStr) : Option (List Cost.BitStr)

The bounded parse into blocks: a serialized list of c blocks of k bits.

Equations

• MIPRE.AnswerReduction.parseB k c s = match MIPRE.Cost.decode (MIPRE.Cost.Data.parse s) with | some bs => if bs.length = c ∧ ∀ b ∈ bs, List.length b = k then some bs else none | none => none

theorem MIPRE.AnswerReduction.parse_eq {k : ℕ} (E : SAT.BinField k) {P : SAT.PcpParams} (t : Pcp.PcpTy) (s : Cost.BitStr) : parse E t s = Option.map (fun (bs : List Cost.BitStr) => ofElems E t (List.map E.ofBits bs)) (parseB k (cnt P t) s)

theorem MIPRE.AnswerReduction.parseB_spec {k c : ℕ} {s : Cost.BitStr} {bs : List Cost.BitStr} (h : parseB k c s = some bs) : bs.length = c ∧ ∀ b ∈ bs, List.length b = k

noncomputable def MIPRE.AnswerReduction.acceptsB (kU m'U : Cost.Unary) (descs : List StageProg.Desc) (chkP chkQ : Bool) (p q : ArTy) (X Y : StageProg.Blocks) (A B : List Cost.BitStr) : Bool

The answer-reduced predicate on blocks: the equal-type check and both sides.

Equations

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

noncomputable def MIPRE.AnswerReduction.verdictB (kU m'U : Cost.Unary) (descs : List StageProg.Desc) (chkP chkQ : Bool) (p q : ArTy) (X Y : StageProg.Blocks) (a b : Cost.BitStr) : Bool

The typed predicate on bits: parse both answers into blocks, then decide.

Equations

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

theorem MIPRE.AnswerReduction.desc_zero_sz (F : PcpFamily) (n : ℕ) : List.length ((List.ofFn (F.desc n)).getD 0 default).2.1 = (F.par n).m

theorem MIPRE.AnswerReduction.verdictB_eq (F : PcpFamily) (n : ℕ) {X : Type u_1} (check : X → (Fin (F.par n).m' → Fq (F.par n) ⋯) → (Fin ((F.par n).m' + 6) → Fq (F.par n) ⋯) → Bool) (p q : Q (F.par n) (Fq (F.par n) ⋯) X) (a b : Cost.BitStr) (chkP chkQ : Bool) (hP : ∀ (u : Ans (F.par n) (fld (F.par n) ⋯).carrier), parse (fld (F.par n) ⋯) p.1.2 a = some u → chkPlan p.1 = true → chkP = check p.2.1 ((Pcp.regs6 (F.par n)).ptOf p.2.2) (vals6 u)) (hQ : ∀ (v : Ans (F.par n) (fld (F.par n) ⋯).carrier), parse (fld (F.par n) ⋯) q.1.2 b = some v → chkPlan q.1 = true → chkQ = check q.2.1 ((Pcp.regs6 (F.par n)).ptOf q.2.2) (vals6 v)) : verdictB (Cost.unary (F.par n).k) (Cost.unary (F.par n).m') (List.ofFn (F.desc n)) chkP chkQ p.1 q.1 (blocksV ⋯ (F.par n) p.2.2) (blocksV ⋯ (F.par n) q.2.2) a b = match parse (fld (F.par n) ⋯) p.1.2 a, parse (fld (F.par n) ⋯) q.1.2 b with | some u, some v => accepts (F.sel n) (F.sel' n) check p q u v | x, x_1 => false

The typed predicate is the predicate on bits: for questions whose PCP halves have the blocks blocksV, and game-check verdicts chkP, chkQ that are the game check wherever a type asks for it.