Theory HCSCND

subsection‹HC, SC, and ND›
theory HCSCND
imports HCSC SCND NDHC
begin

theorem HCSCND:
  defines "hc F ≡ AX10 ⊢⇩H F"
  defines "nd F ≡ {} ⊢ F"
  defines "sc F ≡ {#} ⇒ {# F #}"
  shows "hc F ⟷ nd F" and "nd F ⟷ sc F" and "sc F ⟷ hc F"
using HCSC[where F=F and Γ=‹{#}›, simplified]
      SCND[where Γ=‹{#}› and Δ="{#F#}"] ND.ND.CC[where F=F and Γ="{}"]
      NDHC[where Γ="{}" and F=F]
by(simp_all add: assms) blast+

end