/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Computability.TuringMachine.PostTuringMachine public import Mathlib.Logic.Relation@[expose] public sectiontheorem Part.get_eq_get {σ : Type*} {a b : Part σ} (ha : a.Dom) (hb : a.get ha ∈ b) : a = b := byσ:Type u_1a:Part σb:Part σha:a.Domhb:a.get ha ∈ b⊢ a = b have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩σ:Type u_1a:Part σb:Part σha:a.Domhb:a.get ha ∈ bhb':b.Dom⊢ a = b rwa [← Part.eq_get_iff_mem hb',σ:Type u_1a:Part σb:Part σha:a.Domhb':b.Domhb:a.get ha = b.get hb'⊢ a = b Part.eq_iff_of_dom ha hb'σ:Type u_1a:Part σb:Part σha:a.Domhb':b.Domhb:a = b⊢ a = b]σ:Type u_1a:Part σb:Part σha:a.Domhb':b.Domhb:a = b⊢ a = b at hbnamespace StateTransitionlemma dom_of_apply_eq_none {σ : Type*} {f : σ → Option σ} {s : σ} (hf : f s = none) : s ∈ eval f s := byσ:Type u_1f:σ → Option σs:σhf:f s = none⊢ s ∈ eval f s apply PFun.fix_stopσ:Type u_1f:σ → Option σs:σhf:f s = none⊢ Sum.inl s ∈ Part.some ((f s).elim (Sum.inl s) Sum.inr) simp [hf]All goals completed! 🐙 theorem apply_get_eval {σ : Type*} {f : σ → Option σ} {s : σ} (H : (eval f s).Dom) : f ((eval f s).get H) = none := byσ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ f ((eval f s).get H) = none have := Part.get_mem Hσ:Type u_1f:σ → Option σs:σH:(eval f s).Domthis:(eval f s).get H ∈ eval f s⊢ f ((eval f s).get H) = none rw [mem_evalσ:Type u_1f:σ → Option σs:σH:(eval f s).Domthis:Reaches f s ((eval f s).get H) ∧ f ((eval f s).get H) = none⊢ f ((eval f s).get H) = noneσ:Type u_1f:σ → Option σs:σH:(eval f s).Domthis:Reaches f s ((eval f s).get H) ∧ f ((eval f s).get H) = none⊢ f ((eval f s).get H) = none] at thisσ:Type u_1f:σ → Option σs:σH:(eval f s).Domthis:Reaches f s ((eval f s).get H) ∧ f ((eval f s).get H) = none⊢ f ((eval f s).get H) = none exact this.rightAll goals completed! 🐙-- TODO(Paul-Lez): also prove this for `PFun.fix`/golf using the `PFun.fix` API theorem eval_get_eval {σ : Type*} {f : σ → Option σ} {s : σ} (H : (eval f s).Dom) : eval f ((eval f s).get H) = eval f s := byσ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ eval f ((eval f s).get H) = eval f s symmσ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ eval f s = eval f ((eval f s).get H) apply Part.get_eq_get H (dom_of_apply_eq_none ?_)σ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ f ((eval f s).get H) = none simp [apply_get_eval]All goals completed! 🐙 -- TODO(Paul-Lez): also prove this for `PFun.fix`/golf using the `PFun.fix` API theorem eval_eq_eval {σ : Type*} {f : σ → Option σ} {a a' : σ} (H : f a = some a'): eval f a = eval f a' := byσ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ eval f a = eval f a' apply reaches_evalσ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ Reaches f a a' apply Relation.ReflTransGen.singleσ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ a' ∈ f a rw [Hσ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ a' ∈ some a'σ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ a' ∈ some a']σ:Type u_1f:σ → Option σa:σa':σH:f a = some a'⊢ a' ∈ some a' rflAll goals completed! 🐙 -- TODO(lezeau): this should be generalized to `PFun.fix` theorem eval_dom_iff {σ : Type*} {f : σ → Option σ} {s : σ} : (∃ n, ((Option.bind · f)^[n+1] s) = none) ↔ (eval f s).Dom := byσ:Type u_1f:σ → Option σs:σ⊢ (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) ↔ (eval f s).Dom refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun H ↦ ?_⟩refine_1σ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonen:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some s) = none⊢ (eval f s).Domrefine_2σ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none ·refine_1σ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonen:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some s) = none⊢ (eval f s).Dom induction n generalizing s with | zero =>refine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[0 + 1] (some s) = none⊢ (eval f s).Dom rw [zero_add,refine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[1] (some s) = none⊢ (eval f s).Domrefine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:f s = none⊢ (eval f s).Dom Function.iterate_one,refine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(some s).bind f = none⊢ (eval f s).Domrefine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:f s = none⊢ (eval f s).Dom Option.bind_somerefine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:f s = none⊢ (eval f s).Domrefine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:f s = none⊢ (eval f s).Dom] at hnrefine_1.zeroσ:Type u_1f:σ → Option σs:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:f s = none⊢ (eval f s).Dom simpa [Part.dom_iff_mem] using ⟨s, dom_of_apply_eq_none hn⟩All goals completed! 🐙 | succ n ih =>refine_1.succσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = none⊢ (eval f s).Dom obtain ha | ⟨a', ha'⟩ := (f s).eq_none_or_eq_somerefine_1.succ.inlσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = noneha:f s = none⊢ (eval f s).Domrefine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = nonea':σha':f s = some a'⊢ (eval f s).Dom ·refine_1.succ.inlσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = noneha:f s = none⊢ (eval f s).Dom simpa [Part.dom_iff_mem] using ⟨s, dom_of_apply_eq_none ha⟩All goals completed! 🐙 ·refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = nonea':σha':f s = some a'⊢ (eval f s).Dom simp_rw [refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none) → (fun x ↦ x.bind f)^[n + 1] (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n + 1 + 1] (some s) = nonea':σha':f s = some a'⊢ (eval f s).DomFunction.iterate_succ,refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, ((fun x ↦ x.bind f)^[n] ∘ fun x ↦ x.bind f) (some s) = none) → ((fun x ↦ x.bind f)^[n] ∘ fun x ↦ x.bind f) (some s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(((fun x ↦ x.bind f)^[n] ∘ fun x ↦ x.bind f) ∘ fun x ↦ x.bind f) (some s) = nonea':σha':f s = some a'⊢ (eval f s).Dom Function.comp_apply,refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] ((some s).bind f) = none) → (fun x ↦ x.bind f)^[n] ((some s).bind f) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n] (((some s).bind f).bind f) = nonea':σha':f s = some a'⊢ (eval f s).Dom Option.bind_somerefine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n] ((f s).bind f) = nonea':σha':f s = some a'⊢ (eval f s).Dom] at hn ih simp_rw [refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonehn:(fun x ↦ x.bind f)^[n] ((f s).bind f) = nonea':σha':f s = some a'⊢ (eval f s).Domha',refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea':σha':f s = some a'hn:(fun x ↦ x.bind f)^[n] ((some a').bind fun a ↦ f a) = none⊢ (eval f s).Dom Option.bind_somerefine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea':σha':f s = some a'hn:(fun x ↦ x.bind f)^[n] (f a') = none⊢ (eval f s).Dom] at hn have ih := @ih a' ⟨n, hn⟩ hnrefine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih✝:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea':σha':f s = some a'hn:(fun x ↦ x.bind f)^[n] (f a') = noneih:(eval f a').Dom⊢ (eval f s).Dom rwa [eval_eq_eval ha'refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih✝:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea':σha':f s = some a'hn:(fun x ↦ x.bind f)^[n] (f a') = noneih:(eval f a').Dom⊢ (eval f a').Dom]refine_1.succ.inrσ:Type u_1f:σ → Option σn:ℕih✝:∀ {s : σ}, (∃ n, (fun x ↦ x.bind f)^[n] (f s) = none) → (fun x ↦ x.bind f)^[n] (f s) = none → (eval f s).Doms:σx✝:∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea':σha':f s = some a'hn:(fun x ↦ x.bind f)^[n] (f a') = noneih:(eval f a').Dom⊢ (eval f a').Dom ·refine_2σ:Type u_1f:σ → Option σs:σH:(eval f s).Dom⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none let C (s) : Prop := (eval f s).Dom → ∃ n, (Option.bind · f)^[n+1] s = nonerefine_2σ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none apply evalInduction (C := C) (a := s) (h := Part.get_mem H) _ Hσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = none⊢ ∀ (a : σ), (eval f s).get H ∈ eval f a → (∀ (a' : σ), f a = some a' → C a') → C a intro a ha h HHσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Dom⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none obtain ha | ⟨a', ha'⟩ := (f a).eq_none_or_eq_someinlσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha✝:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Domha:f a = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = noneinrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none ·inlσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha✝:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Domha:f a = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none use 0hσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha✝:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Domha:f a = none⊢ (fun x ↦ x.bind f)^[0 + 1] (some a) = none simp [ha]All goals completed! 🐙 ·inrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none obtain ⟨n, hn⟩ := h a' ha' (byσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'⊢ (eval f a').Dominrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some a') = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none rwa [← eval_eq_eval ha'σ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'⊢ (eval f a).Dominrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some a') = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none]σ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'⊢ (eval f a).Dominrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some a') = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none)inrσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some a') = none⊢ ∃ n, (fun x ↦ x.bind f)^[n + 1] (some a) = none use n + 1hσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n + 1] (some a') = none⊢ (fun x ↦ x.bind f)^[n + 1 + 1] (some a) = none simp only [Function.iterate_succ, Function.comp_apply, Option.bind_some] at hnhσ:Type u_1f:σ → Option σs:σH:(eval f s).DomC:σ → Prop := fun s ↦ (eval f s).Dom → ∃ n, (fun x ↦ x.bind f)^[n + 1] (some s) = nonea:σha:(eval f s).get H ∈ eval f ah:∀ (a' : σ), f a = some a' → C a'HH:(eval f a).Doma':σha':f a = some a'n:ℕhn:(fun x ↦ x.bind f)^[n] (f a') = none⊢ (fun x ↦ x.bind f)^[n + 1 + 1] (some a) = none simp [ha', hn]All goals completed! 🐙end StateTransition