Commit 8481b20b authored by Ralf Jung's avatar Ralf Jung

extend Löb proof comment

parent a148dd29
...@@ -204,7 +204,8 @@ Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P). ...@@ -204,7 +204,8 @@ Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed. Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
Section löb. Section löb.
(* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem *) (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
Their Ψ is called Q in our proof. *)
Lemma weak_löb P : ( P P) (True P). Lemma weak_löb P : ( P P) (True P).
Proof. Proof.
pose (flöb_pre (P Q : PROP) := ( Q P)%I). pose (flöb_pre (P Q : PROP) := ( Q P)%I).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment