[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (FinTM2.Γ tm k)
[PROOFSTEP]
rw [h]
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (FinTM2.Γ tm tm.k₀)
[PROOFSTEP]
exact s
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (FinTM2.Γ tm k)
[PROOFSTEP]
rw [h]
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (FinTM2.Γ tm tm.k₁)
[PROOFSTEP]
exact s
[GOAL]
σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c
[PROOFSTEP]
rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]
[GOAL]
α : Type
ea : FinEncoding α
x✝ : α
⊢ { steps := 1,
        evals_in_steps :=
          (_ :
            (flip bind
                    (FinTM2.step
                      { tm := idComputer ea,
                          inputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                          outputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm))^[1]
                (some
                  (initList
                    { tm := idComputer ea,
                        inputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                        outputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm
                    (List.map
                      { tm := idComputer ea,
                            inputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                            outputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.inputAlphabet.invFun
                      (Encoding.encode ea.toEncoding x✝)))) =
              (flip bind
                    (FinTM2.step
                      { tm := idComputer ea,
                          inputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                          outputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm))^[1]
                (some
                  (initList
                    { tm := idComputer ea,
                        inputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                        outputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm
                    (List.map
                      { tm := idComputer ea,
                            inputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                            outputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.inputAlphabet.invFun
                      (Encoding.encode ea.toEncoding x✝))))) }.steps ≤
    Polynomial.eval (List.length (Encoding.encode ea.toEncoding x✝)) 1
[PROOFSTEP]
simp only [Polynomial.eval_one]
