File FixPoint

From MatchingLogic Require Export FreshnessManager.
From MatchingLogic.ProofMode Require Export Firstorder.

Import MatchingLogic.Logic.Notations.


Lemma mu_monotone_quantify {Σ : Signature} Γ ϕ₁ ϕ₂ X (i : ProofInfo):
  ProofInfoLe ( (ExGen := ∅, SVSubst := {[X]}, KT := true, AKT := ~~ bound_svar_is_banned_under_mus ϕ₁^{{svar:X↦0}} 0 0)) i →
  svar_has_negative_occurrence X ϕ₁ = false →
  svar_has_negative_occurrence X ϕ₂ = false →
  Γ ⊢i ϕ₁ ---> ϕ₂ using i→
  Γ ⊢i (patt_mu (ϕ₁^{{svar: X ↦ 0}})) ---> (patt_mu (ϕ₂^{{svar: X ↦ 0}}))
  using i.

Lemma mu_monotone {Σ : Signature} Γ ϕ₁ ϕ₂ X (i : ProofInfo):
  ProofInfoLe ( (ExGen := ∅, SVSubst := {[X]}, KT := true, AKT := ~~ bound_svar_is_banned_under_mus ϕ₁ 0 0)) i →
  well_formed (patt_mu ϕ₁) →
  well_formed (patt_mu ϕ₂) →
  X ∉ free_svars ϕ₁ ∪ free_svars ϕ₂ →
  Γ ⊢i ϕ₁^{svar:0↦X} ---> ϕ₂^{svar:0↦X} using i→
  Γ ⊢i (patt_mu ϕ₁) ---> (patt_mu ϕ₂)
  using i.

Lemma mu_iff_quantify {Σ : Signature} Γ ϕ₁ ϕ₂ X (i : ProofInfo):
  ProofInfoLe ( (ExGen := ∅, SVSubst := {[X]}, KT := true, AKT := true)) i →
  svar_has_negative_occurrence X ϕ₁ = false →
  svar_has_negative_occurrence X ϕ₂ = false →
  Γ ⊢i ϕ₁ <---> ϕ₂ using i→
  Γ ⊢i (patt_mu (ϕ₁^{{svar: X ↦ 0}})) <---> (patt_mu (ϕ₂^{{svar: X ↦ 0}}))
  using i.
Lemma move_mu_under_implication
  {Σ : Signature}
  Γ φ ψ :
    well_formed φ →
    well_formed (mu , ψ) →
    Γ ⊢i φ ---> (mu , ψ) ---> mu , (φ ---> ψ) using
      (ExGen := ∅,
       SVSubst := ∅,
       KT := true,
       AKT := ~~ bound_svar_is_banned_under_mus ψ 0 0).