 K \<div> \<phi>
[PROOF STEP]
by (metis a emptyrem2taut contract_closure contract_recovery valid_expansion)
[PROOF STATE]
proof (state)
this:
K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>

goal (1 subgoal):
 1. \<not> \<tturnstile> \<phi> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<tturnstile> \<phi> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
case validFalse:False
[PROOF STATE]
proof (state)
this:
\<not> \<tturnstile> \<phi>

goal (1 subgoal):
 1. \<not> \<tturnstile> \<phi> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<tturnstile> \<phi>
[PROOF STEP]
show?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> \<tturnstile> \<phi>

goal (1 subgoal):
 1. K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
proof (cases \<open>K \<turnstile> \<phi>\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tturnstile> \<phi>; K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
 2. \<lbrakk>\<not> \<tturnstile> \<phi>; \<not> K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
K \<turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>\<not> \<tturnstile> \<phi>; K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
 2. \<lbrakk>\<not> \<tturnstile> \<phi>; \<not> K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
hence b:\<open>K.\<bottom>. \<phi> \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
K \<turnstile> \<phi>

goal (1 subgoal):
 1. K.\<bottom>. \<phi> \<noteq> {}
[PROOF STEP]
using emptyrem2taut validFalse
[PROOF STATE]
proof (prove)
using this:
K \<turnstile> \<phi>
?A.\<bottom>.?\<phi> = {} \<Longrightarrow> \<tturnstile>?\<phi>
\<not> \<tturnstile> \<phi>

goal (1 subgoal):
 1. K.\<bottom>. \<phi> \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
K.\<bottom>. \<phi> \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>\<not> \<tturnstile> \<phi>; K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
 2. \<lbrakk>\<not> \<tturnstile> \<phi>; \<not> K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
have d:\<open>\<psi> \<in> K \<Longrightarrow> \<phi>.\<longrightarrow>. \<psi> \<in> K \<div> \<phi>\<close> for \<psi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<in> K \<Longrightarrow> \<phi>.\<longrightarrow>. \<psi> \<in> K \<div> \<phi>
[PROOF STEP]
using Supraclassical_logic.impI_PL Supraclassical_logic_axioms a contract_closure contract_recovery expansion_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Supraclassical_logic?Cn?true_PL?false_PL?imp_PL?not_PL?conj_PL?disj_PL?equiv_PL;?q \<in>?Cn (?A \<union> {?p})\<rbrakk> \<Longrightarrow>?imp_PL?p?q \<in>?Cn?A
Supraclassical_logic Cn \<top> \<bottom> (.\<longrightarrow>.).\<not> (.\<and>.) (.\<or>.) (.\<longleftrightarrow>.)
K = Cn A
?K = Cn?A \<Longrightarrow>?K \<div>?\<phi> = Cn (?K \<div>?\<phi>)
?K = Cn?A \<Longrightarrow>?K \<subseteq> (?K \<div>?\<phi>) \<oplus>?\<phi>
?A \<oplus>?\<phi> \<equiv> Cn (?A \<union> {?\<phi>})

goal (1 subgoal):
 1. \<psi> \<in> K \<Longrightarrow> \<phi>.\<longrightarrow>. \<psi> \<in> K \<div> \<phi>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?\<psi> \<in> K \<Longrightarrow> \<phi>.\<longrightarrow>.?\<psi> \<in> K \<div> \<phi>

goal (2 subgoals):
 1. \<lbrakk>\<not> \<tturnstile> \<phi>; K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
 2. \<lbrakk>\<not> \<tturnstile> \<phi>; \<not> K \<turnstile> \<phi>\<rbrakk> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state