Theory SCND

subsection‹SC to ND›
theory SCND
imports SC ND
begin

lemma SCND: "Γ ⇒ Δ ⟹ (set_mset Γ) ∪ Not ` (set_mset Δ) ⊢ ⊥"
proof(induction Γ Δ rule: SCp.induct)
  case BotL thus ?case by (simp add: ND.Ax)
next
  case Ax thus ?case by (meson ND.Ax NotE UnCI image_iff)
next
  case NotL thus ?case by (simp add: NotI)
next
  case (NotR F Γ Δ) thus ?case by (simp add: Not2IE)
next
  case (AndL F G Γ Δ) thus ?case by (simp add: AndL_sim)
next
  case (AndR Γ F Δ G) thus ?case by(simp add: AndR_sim)
next
  case OrL thus ?case by (simp add: OrL_sim)
next
  case OrR thus ?case using OrR_sim[where 'a='a] by (simp add: insert_commute)
next
  case (ImpL Γ F Δ G) from ImpL.IH show ?case by (simp add: ImpL_sim)
next
  case ImpR from ImpR.IH show ?case by (simp add: ImpR_sim)
qed

end