A question, read back

The mirror of DescriptiveComplexity.GameProg.altWin_ask: if the machine wins from the entry of a question's prefix, the question holds.

What the bridge has to say, backwards

• an arrival is a correct claim. DescriptiveComplexity.SeekArrives gives a cell whose symbol answered the test; unfolding DescriptiveComplexity.GameProg.isTarget says the symbol's bit is the claim, its region is the one the atom's copy names, and its address is the atom's arguments at the valuation. Since the tape's cell carries the bit the assignment gives it, the claim is right – and the region bookkeeping is DescriptiveComplexity.GameProg.cond_copy again, read the other way;
• the seek's test never fires on a mark, which the parametric layer had to assume and the program discharges by unfolding one existential;
• the tuple SeekArrives carries is not the one the forward direction builds, so the address it names has to be recovered from argsOf and the agreement with the phase's valuation – which is the only place the two halves of a transition's tuple are pulled apart backwards.

theorem DescriptiveComplexity.GameProg.ask_of_altWin {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (q : GameQuestion) {φ : ((K.sum B.lang).sum B.lang).Sentence} (hplays : (prog.data q).Plays φ) {r par : Bool} {jj : Fin (V + 1)} (hjj : ↑jj = 0) {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (h : CtrlCfg a₀ hdim prog.vars ρ σ (MachPh.prePh q r jj par) vv c) (hw : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c) : A ⊨ φ

A question holds, read back: if the machine wins from the entry of a question's prefix, the question's sentence is true of the two assignments the tape carries. This is the converse of DescriptiveComplexity.GameProg.altWin_ask.