Commit 0e730222 authored by litak's avatar litak

more fixes

parent 7549380b
......@@ -66,7 +66,7 @@ Notation "{ Z + G } [-- A" := (KIbox Z G A) (at level 79).
(** * Equivalence Proofs for the Translations *)
(** In this section we prove that the regular translations result in equivalent formulas.
In some parts of the proof script below, an old name for such translations as being "in the triangle" persisted. This name one can see the regular translations as lying in a triangle given by the refinement order on monotone modular ones. *)
In some parts of the proof script below, an old name for such translations as being "in the triangle" persisted. This name comes from the fact tha one can see the regular translations as lying in a triangle given by the refinement order on monotone modular ones. *)
Lemma eq_ggr_kur : forall Z f, KIbox Z [] ((ggr f) <<->> (kur f)).
Proof.
......@@ -479,6 +479,11 @@ Definition dneg_envelope (A : form) :=
Definition kuroda_envelope (Z : form) :=
forall A, KIbox Z [] ((kol A) <<->> -+! A).
(*
Definition gg_envelope (Z : form) :=
forall A, KIbox Z [] ((kol A) <<->> -+! (sub_vars_dneg A)).*)
Corollary dneg_envelope_correct:
forall A, dneg_envelope A <-> pre_envelope A /\ post_envelope A.
Proof.
......
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