Documentation

MIPRE.TM.Interp.Run

The run of the interpreter #

The inputs of U (uInput), the initialization (init_run), the simulation of a run of the evaluation machine (sim_run), and the acceptance theorem: on the inputs (π’Ÿ, n, T, x, y, a, b) with |a|, |b| ≀ T, U accepts (halts having output 1) iff π’Ÿ accepts (n, x, y, a, b) within cost T, and then within an explicit polynomial number of steps.

The inputs #

source
def MIPRE.TM.Interp.uInput (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
Fin 7 β†’ List Sym

The seven inputs of U: the program, n, the budget T in unary, x, y as the bits of their encodings, and the answers a, b as raw bit strings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_PROG (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b PROG = S D.toData
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_N (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b N = S (Cost.encode n)
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_T (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b T = List.replicate Tb Sym.one
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_XS (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b XS = S (Cost.encode x)
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_YS (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b YS = S (Cost.encode y)
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_A (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b A = bits a
    source
    @[simp]
    theorem MIPRE.TM.Interp.uInput_B (D : Cost.Prog) (n Tb : β„•) (x y a b : Cost.BitStr) :
    uInput D n Tb x y a b B = bits b
    source
    theorem MIPRE.TM.Interp.mem_bits (l : List Bool) (s : Sym) :
    s ∈ bits l β†’ s = Sym.zero ∨ s = Sym.one
    source
    theorem MIPRE.TM.Interp.map_boolOf_bits (l : List Bool) :
    List.map boolOf (bits l) = l
    source
    theorem MIPRE.TM.Interp.answerBits_bits (l : Cost.BitStr) :
    answerBits (bits l) = S (Cost.encode l)
    source
    theorem MIPRE.TM.Interp.encode_prod {Ξ± : Type u_1} {Ξ² : Type u_2} [Cost.SizedEncoding Ξ±] [Cost.SizedEncoding Ξ²] (p : Ξ± Γ— Ξ²) :
    Cost.encode p = (Cost.encode p.1).cons (Cost.encode p.2)

    Input heads #

    source
    def MIPRE.TM.Interp.InPos {input : Fin 7 β†’ List Sym} (c : Cfg input) (f : IT β†’ β„•) :
    Prop

    The input heads are at the positions f.

    Equations
    Instances For
      source
      theorem MIPRE.TM.Interp.InPos.of_untouched {input : Fin 7 β†’ List Sym} {c c' : Cfg input} {f : IT β†’ β„•} (h : InPos c f) {SW : List WT} (hu : Untouched c c' [] SW) :
      InPos c' f
      source
      theorem MIPRE.TM.Interp.Desc.of_untouched_inputs {input : Fin 7 β†’ List Sym} {c c' : Cfg input} {q : Option Ctl} {ds : WT β†’ TapeSt} (hd : Desc c q ds) {SI : List IT} (hu : Untouched c c' SI []) {q' : Option Ctl} (hs : c'.state = q') :
      Desc c' q' ds

      A run touching only input heads leaves the descriptions.

      source
      theorem MIPRE.TM.Interp.InPos.update {input : Fin 7 β†’ List Sym} {c c' : Cfg input} {f : IT β†’ β„•} (h : InPos c f) {j : IT} {SW : List WT} (hu : Untouched c c' [j] SW) {v : β„•} (hv : ↑(c'.inputPos j) = v) :
      InPos c' (Function.update f j v)
      source
      theorem MIPRE.TM.Interp.InPos.updateβ‚‚ {input : Fin 7 β†’ List Sym} {c c' : Cfg input} {f : IT β†’ β„•} (h : InPos c f) {j j' : IT} {SW : List WT} (hu : Untouched c c' [j, j'] SW) {v v' : β„•} (hv : ↑(c'.inputPos j) = v) (hv' : ↑(c'.inputPos j') = v') (hjj : j β‰  j') :
      InPos c' (Function.update (Function.update f j v) j' v')
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_N :
      PROG β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_T :
      PROG β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_XS :
      PROG β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_YS :
      PROG β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_A :
      PROG β‰  A
      source
      @[simp]
      theorem MIPRE.TM.Interp.PROG_ne_B :
      PROG β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_PROG :
      N β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_T :
      N β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_XS :
      N β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_YS :
      N β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_A :
      N β‰  A
      source
      @[simp]
      theorem MIPRE.TM.Interp.N_ne_B :
      N β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_PROG :
      T β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_N :
      T β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_XS :
      T β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_YS :
      T β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_A :
      T β‰  A
      source
      @[simp]
      theorem MIPRE.TM.Interp.T_ne_B :
      T β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_PROG :
      XS β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_N :
      XS β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_T :
      XS β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_YS :
      XS β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_A :
      XS β‰  A
      source
      @[simp]
      theorem MIPRE.TM.Interp.XS_ne_B :
      XS β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_PROG :
      YS β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_N :
      YS β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_T :
      YS β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_XS :
      YS β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_A :
      YS β‰  A
      source
      @[simp]
      theorem MIPRE.TM.Interp.YS_ne_B :
      YS β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_PROG :
      A β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_N :
      A β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_T :
      A β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_XS :
      A β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_YS :
      A β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.A_ne_B :
      A β‰  B
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_PROG :
      B β‰  PROG
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_N :
      B β‰  N
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_T :
      B β‰  T
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_XS :
      B β‰  XS
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_YS :
      B β‰  YS
      source
      @[simp]
      theorem MIPRE.TM.Interp.B_ne_A :
      B β‰  A

      The input routines on descriptions #

      source
      theorem MIPRE.TM.Interp.I_jump {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {target : ProgId} (hins : instrAt k pc = Instr.jump target) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) :
      βˆƒ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (at_ target ⟨0, I_jump._proof_1⟩) ds ∧ InPos c' f
      source
      theorem MIPRE.TM.Interp.Desc.of_weff_end {input : Fin 7 β†’ List Sym} {c : Cfg input} {ds : WT β†’ TapeSt} {q : Option Ctl} (hd : Desc c q ds) {c' : Cfg input} {dst : WT} {SI : List IT} (hu : Untouched c c' SI [dst]) {q' : Option Ctl} (hs : c'.state = q') {w : List Sym} (hw : WEff dst c c' w) (hp : (ds dst).p = (ds dst).l.length) :
      Desc c' q' (Function.update ds dst { l := (ds dst).l ++ w, p := ((ds dst).l ++ w).length })

      A written effect on dst at the end of its content, as a description.

      source
      theorem MIPRE.TM.Interp.I_write_end {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {t : WT} {s : Sym} (hins : instrAt k pc = Instr.write t s) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : (ds t).p = (ds t).l.length) (hi : InPos c f) :
      βˆƒ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l ++ [s], p := ((ds t).l ++ [s]).length }) ∧ InPos c' f
      source
      theorem MIPRE.TM.Interp.I_copyUnary_end {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.copyUnary j dst) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) (hj : f j = 1) (hp : (ds dst).p = (ds dst).l.length) :
      βˆƒ (c' : Cfg input), Reach c ((input j).length + 1) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds dst { l := (ds dst).l ++ List.replicate (input j).length Sym.one, p := ((ds dst).l ++ List.replicate (input j).length Sym.one).length }) ∧ InPos c' (Function.update f j ((input j).length + 1))
      source
      theorem MIPRE.TM.Interp.I_copyInputBits_end {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.copyInputBits j dst) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) (hj : f j = 1) (hp : (ds dst).p = (ds dst).l.length) :
      βˆƒ (c' : Cfg input), Reach c ((input j).length + 1) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds dst { l := (ds dst).l ++ input j, p := ((ds dst).l ++ input j).length }) ∧ InPos c' (Function.update f j ((input j).length + 1))
      source
      theorem MIPRE.TM.Interp.I_buildAnswer_end {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.buildAnswer j dst) (hpc : ↑pc + 1 < maxPc) (hbits : βˆ€ s ∈ input j, s = Sym.zero ∨ s = Sym.one) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) (hj : f j = 1) (hp : (ds dst).p = (ds dst).l.length) :
      βˆƒ n ≀ 4 * (input j).length + 1, βˆƒ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds dst { l := (ds dst).l ++ answerBits (input j), p := ((ds dst).l ++ answerBits (input j)).length }) ∧ InPos c' (Function.update f j ((input j).length + 1))
      source
      theorem MIPRE.TM.Interp.I_checkLen {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j ref : IT} (hins : instrAt k pc = Instr.checkLen j ref) (hpc : ↑pc + 1 < maxPc) (hjr : j β‰  ref) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) (hj : f j = 1) (hr : f ref = 1) (hlen : (input j).length ≀ (input ref).length) :
      βˆƒ (c' : Cfg input), Reach c ((input j).length + 1) c' [] ∧ Desc c' (next_ k pc hpc) ds ∧ InPos c' (Function.update (Function.update f j ((input j).length + 1)) ref ((input j).length + 1))
      source
      theorem MIPRE.TM.Interp.I_rewindInput {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j : IT} (hins : instrAt k pc = Instr.rewindInput j) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) :
      βˆƒ n ≀ f j + 2, βˆƒ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) ds ∧ InPos c' (Function.update f j 0)
      source
      theorem MIPRE.TM.Interp.I_moveInput_right {input : Fin 7 β†’ List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT β†’ TapeSt} {f : IT β†’ β„•} {j : IT} (hins : instrAt k pc = Instr.moveInput j true) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hi : InPos c f) (hlt : f j < (input j).length + 1) :
      βˆƒ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) ds ∧ InPos c' (Function.update f j (f j + 1))

      The initialization #

      source
      def MIPRE.TM.Interp.initBound (D : Cost.Prog) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) :
      β„•

      The bound on the steps of the initialization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.TM.Interp.desc_initCfg (input : Fin 7 β†’ List Sym) :
        Desc (Turing.MultiInputTM.initCfg input) (at_ ProgId.init 0) fun (x : WT) => { l := [], p := 0 }

        The initial configuration is described by empty tapes.

        source
        theorem MIPRE.TM.Interp.inPos_initCfg (input : Fin 7 β†’ List Sym) :
        InPos (Turing.MultiInputTM.initCfg input) fun (x : IT) => 1
        source
        theorem MIPRE.TM.Interp.init_run (D : Cost.Prog) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) (ha : List.length a ≀ Tb) (hb : List.length b ≀ Tb) :
        βˆƒ m ≀ initBound D n x y a b Tb, βˆƒ (c : Cfg (uInput D n Tb x y a b)) (ds : WT β†’ TapeSt), Reach (Turing.MultiInputTM.initCfg (uInput D n Tb x y a b)) m c [] ∧ Desc c (at_ ProgId.dispatch 0) ds ∧ RepOf ds { ctrl := Cost.Machine.Ctrl.ev D, env := [Cost.encode (n, x, y, a, b)], kont := [] } Tb (ctrlRepr (Cost.Machine.Ctrl.ev D)).length 0 ∧ (ds X).l.length = 0

        The initialization: from the initial configuration on the inputs (π’Ÿ, n, T, x, y, a, b) with |a|, |b| ≀ T, U reaches the dispatcher representing ⟨ev π’Ÿ, [encode (n, x, y, a, b)], []⟩ with budget Tb and an empty scratch tape.

        The size of a bounded representation #

        source
        def MIPRE.TM.Interp.szBound (V L P K : β„•) :
        β„•

        A bound on sz from CfgBound V L P K.

        Equations
        Instances For
          source
          theorem MIPRE.TM.Interp.length_envRepr_le {V L : β„•} (env : Cost.Env) (hL : List.length env ≀ L) (hV : βˆ€ v ∈ env, v.size ≀ V) :
          (envRepr env).length ≀ L * V + L
          source
          theorem MIPRE.TM.Interp.length_kontRepr_le {V L P K : β„•} (k : List Cost.Machine.Frame) (hK : k.length ≀ K) (hf : βˆ€ f ∈ k, Cost.Machine.FrameBound V L P f) :
          (kontRepr k).length ≀ K * (V + P + L * V + L + 4)
          source
          theorem MIPRE.TM.Interp.sz_le {V L P K : β„•} {m : Cost.Machine.Cfg} (h : Cost.Machine.CfgBound V L P K m) :
          sz m ≀ szBound V L P K

          The simulation of a run #

          source
          def MIPRE.TM.Interp.stepB (Z xl : β„•) :
          β„•

          The bound on the steps of U for one step of the machine, from representations of size at most Z with a scratch tape of length at most xl.

          Equations
          Instances For
            source
            theorem MIPRE.TM.Interp.stepBound_le {m : Cost.Machine.Cfg} {Z xl xl' : β„•} (hZ : sz m ≀ Z) (hx : xl ≀ xl') :
            stepBound m xl ≀ stepB Z xl'
            source
            theorem MIPRE.TM.Interp.stepB_mono (Z : β„•) {xl xl' : β„•} (hx : xl ≀ xl') :
            stepB Z xl ≀ stepB Z xl'
            source
            theorem MIPRE.TM.Interp.costSum_succ (m : Cost.Machine.Cfg) (N : β„•) :
            Cost.Machine.costSum m (N + 1) = Cost.Machine.costSum m N + Cost.Machine.stepCost (Cost.Machine.step^[N] m)
            source
            theorem MIPRE.TM.Interp.costSum_mono (m : Cost.Machine.Cfg) {a b : β„•} (h : a ≀ b) :
            Cost.Machine.costSum m a ≀ Cost.Machine.costSum m b
            source
            theorem MIPRE.TM.Interp.sim_run {input : Fin 7 β†’ List Sym} (Z N : β„•) (m : Cost.Machine.Cfg) (c : Cfg input) (ds : WT β†’ TapeSt) (r : β„•) :
            Desc c (at_ ProgId.dispatch 0) ds β†’ RepOf ds m r (ctrlRepr m.ctrl).length (kontRepr m.kont).length β†’ (βˆ€ i < N, sz (Cost.Machine.step^[i] m) ≀ Z) β†’ (βˆ€ i < N, βˆ€ (v : Cost.Data), (Cost.Machine.step^[i] m).ctrl = Cost.Machine.Ctrl.ret v β†’ (Cost.Machine.step^[i] m).kont β‰  []) β†’ Cost.Machine.costSum m N ≀ r β†’ βˆƒ (n : β„•), N ≀ n ∧ n ≀ N * stepB Z ((ds X).l.length + N * Z) ∧ βˆƒ (c' : Cfg input) (ds' : WT β†’ TapeSt), Reach c n c' [] ∧ Desc c' (at_ ProgId.dispatch 0) ds' ∧ RepOf ds' (Cost.Machine.step^[N] m) (r - Cost.Machine.costSum m N) (ctrlRepr (Cost.Machine.step^[N] m).ctrl).length (kontRepr (Cost.Machine.step^[N] m).kont).length ∧ (ds' X).l.length ≀ (ds X).l.length + N * Z

            The simulation: N steps of the machine, none of them from a final configuration, with their total cost covered by the budget, are simulated by at least N and at most N Β· stepB Z (xl + N Z) steps of U.

            Acceptance #

            source
            theorem MIPRE.TM.Interp.no_accept_of_haltsIn {input : Fin 7 β†’ List Sym} {c : Cfg input} {n : β„•} (h : HaltsIn c n) (S : β„•) :
            U.outputString c S β‰  [Sym.one]
            source
            theorem MIPRE.TM.Interp.AcceptsFrom.acceptsIn {input : Fin 7 β†’ List Sym} {c : Cfg input} {n : β„•} (h : AcceptsFrom c n) {S : β„•} (hS : n ≀ S) :
            (Turing.MultiInputTM.configs c S).state = none ∧ U.outputString c S = [Sym.one]
            source
            @[reducible, inline]
            abbrev MIPRE.TM.Interp.vSize (n : β„•) (x y a b : Cost.BitStr) :
            β„•

            The value of the encoded input.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev MIPRE.TM.Interp.V0 (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) :
              β„•

              The size bound on the machine's values along the run.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev MIPRE.TM.Interp.Z0 (D : Cost.Prog) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) :
                β„•

                The size bound on the representations along the run.

                Equations
                Instances For
                  source
                  def MIPRE.TM.Interp.runBound (D : Cost.Prog) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) :
                  β„•

                  The bound on the accepting run of U.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem MIPRE.TM.Interp.cfgBound_init (D : Cost.Prog) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) :
                    Cost.Machine.CfgBound (V0 n x y a b Tb) 1 (Cost.esize D) 0 { ctrl := Cost.Machine.Ctrl.ev D, env := [Cost.encode (n, x, y, a, b)], kont := [] }
                    source
                    theorem MIPRE.TM.Interp.step_fixed_of_final {r : Cost.Data} {e : Cost.Env} (n : β„•) :
                    Cost.Machine.step^[n] { ctrl := Cost.Machine.Ctrl.ret r, env := e, kont := [] } = { ctrl := Cost.Machine.Ctrl.ret r, env := e, kont := [] }

                    Final configurations are fixed by step.

                    source
                    theorem MIPRE.TM.Interp.accepts_of_acceptsWithin (D : Decider) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) (ha : List.length a ≀ Tb) (hb : List.length b ≀ Tb) (h : D.AcceptsWithin n x y a b Tb) :
                    βˆƒ m ≀ runBound D.prog n x y a b Tb, AcceptsFrom (Turing.MultiInputTM.initCfg (uInput D.prog n Tb x y a b)) m

                    Completeness: if π’Ÿ accepts (n, x, y, a, b) within cost T (and |a|, |b| ≀ T), U accepts the inputs (π’Ÿ, n, T, x, y, a, b) within runBound steps.

                    source
                    theorem MIPRE.TM.Interp.acceptsWithin_of_accepts (D : Decider) (n : β„•) (x y a b : Cost.BitStr) (Tb : β„•) (ha : List.length a ≀ Tb) (hb : List.length b ≀ Tb) (S : β„•) (hS : (Turing.MultiInputTM.configs (Turing.MultiInputTM.initCfg (uInput D.prog n Tb x y a b)) S).state = none ∧ U.outputString (Turing.MultiInputTM.initCfg (uInput D.prog n Tb x y a b)) S = [Sym.one]) :
                    D.AcceptsWithin n x y a b Tb

                    Soundness: if U accepts the inputs (π’Ÿ, n, T, x, y, a, b) (with |a|, |b| ≀ T) at some time S, π’Ÿ accepts (n, x, y, a, b) within cost T.