Commit 3e21a838 by Robbert Krebbers

Replace more occurences of /\ by unicode ∧.

parent bba7474e
 ... ... @@ -24,7 +24,7 @@ Proof. by rewrite twp_unfold /twp_pre=> ->. Qed. Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 : (∀ σ1, reducible_no_obs e1 σ1) → (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] /\ σ1 = σ2) → (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) → (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }]) ⊢ WP e1 @ s; E [{ Φ }]. ... ... @@ -61,7 +61,7 @@ Qed. Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs : (∀ σ1, reducible_no_obs e1 σ1) → (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→ (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→ (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }]) ⊢ WP e1 @ s; E [{ Φ }]. Proof. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!