proof

P26 Update without fixed point

Lean spine source

Declarations: P26_preserves_value_update_without_final_fixed_point

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P26_preserves_value_update_without_final_fixed_point :
    ∃ a : Bool, ToyPreservesValueUpdateOperator a ∧ ¬ ToyKnowsFinalFixedPoint a :=
  ⟨false, trivial, by decide⟩