Theory DEAK_SE

theory (*calc_name_se-BEGIN*)DEAK_SE(*calc_name_se-END*)
imports Main (*calc_name_core_se-BEGIN*)DEAK_Core_SE(*calc_name_core_se-END*)
begin

datatype Locale = (*(*uncommentL?Formula?RuleCut-BEGIN*)*)(*uncommentL?Formula?RuleCut-END*)
                  CutFormula Formula |
                  (*uncommentR?Formula?RuleCut-BEGIN*)(*(*uncommentR?Formula?RuleCut-END*)*)
                  (*(*uncommentL?Sequent-BEGIN*)*)(*uncommentL?Sequent-END*)
                  Premise Sequent |
                  (*uncommentR?Sequent-BEGIN*)(*(*uncommentR?Sequent-END*)*)
                  (*(*uncommentL?Structure-BEGIN*)*)(*uncommentL?Structure-END*)
                  Part Structure |
                  (*uncommentR?Structure-BEGIN*)(*(*uncommentR?Structure-END*)*)
                  (*(*uncommentL?Action?Agent-BEGIN*)*)(*uncommentL?Action?Agent-END*)
                  RelAKA "Action ⇒ Agent ⇒ Action list" | 
                  (*uncommentR?Action?Agent-BEGIN*)(*(*uncommentR?Action?Agent-END*)*)
                  (*(*uncommentL?Action?Formula-BEGIN*)*)(*uncommentL?Action?Formula-END*)
                  PreFormula Action Formula |
                  (*uncommentR?Action?Formula-BEGIN*)(*(*uncommentR?Action?Formula-END*)*)
                  (*(*uncommentL?Agent-BEGIN*)*)(*uncommentL?Agent-END*)
                  LAgent Agent |
                  (*uncommentR?Agent-BEGIN*)(*(*uncommentR?Agent-END*)*)
                  Empty


(*(*uncommentL?Atprop?Formula?Formula_Atprop?Formula_Action_Formula-BEGIN*)*)(*uncommentL?Atprop?Formula?Formula_Atprop?Formula_Action_Formula-END*)
fun is_act_mod :: "Structure ⇒ Atprop option" where
"is_act_mod (Structure_Formula (Formula_Atprop p)) = Some p"|
"is_act_mod (Structure_ForwA _ s) = is_act_mod s"|
"is_act_mod (Structure_BackA _ s) = is_act_mod s"|

"is_act_mod _ = None"

fun atom :: "Sequent ⇒ bool" where
"atom (l ⊢⇩S r) = ( (is_act_mod l) ≠ None ∧ (is_act_mod l) = (is_act_mod r) )"
(*uncommentR?Atprop?Formula?Formula_Atprop?Formula_Action_Formula-BEGIN*)(*(*uncommentR?Atprop?Formula?Formula_Atprop?Formula_Action_Formula-END*)*)


fun pairs :: "'a list ⇒ 'b list ⇒ ('a × 'b) list" where
"pairs [] [] = []" |
"pairs [] Y = []" |
"pairs X [] = []" |
"pairs (X#Xs) (Y#Ys) = (X, Y)#(pairs Xs Ys)"

(*calc_structure_rules_se-BEGIN*)
inductive derivable :: "Locale list ⇒ Sequent ⇒ bool"  (infix "⊢d" 300) where
Bigcomma_Nil_R2: "l ⊢d (Y ⊢⇩S I⇩S) ⟹ l ⊢d (Y ⊢⇩S (;;⇩S []))"|
Bigcomma_Nil_R: "l ⊢d (Y ⊢⇩S (;;⇩S [])) ⟹ l ⊢d (Y ⊢⇩S I⇩S)"|
Bigcomma_Nil_L2: "l ⊢d (I⇩S ⊢⇩S Y) ⟹ l ⊢d ((;;⇩S []) ⊢⇩S Y)"|
Bigcomma_Nil_L: "l ⊢d ((;;⇩S []) ⊢⇩S Y) ⟹ l ⊢d (I⇩S ⊢⇩S Y)"|
Bigcomma_Cons_R2: "l ⊢d (Y ⊢⇩S X ;⇩S (;;⇩S Xs)) ⟹ l ⊢d (Y ⊢⇩S ;;⇩S(X # Xs))"|
Bigcomma_Cons_R: "l ⊢d (Y ⊢⇩S ;;⇩S(X # Xs)) ⟹ l ⊢d (Y ⊢⇩S X ;⇩S (;;⇩S Xs))"|
Bigcomma_Cons_L2: "l ⊢d (X ;⇩S (;;⇩S Xs) ⊢⇩S Y) ⟹ l ⊢d (;;⇩S(X # Xs) ⊢⇩S Y)"|
Bigcomma_Cons_L: "l ⊢d (;;⇩S(X # Xs) ⊢⇩S Y) ⟹ l ⊢d (X ;⇩S (;;⇩S Xs) ⊢⇩S Y)"
| 
SingleCut: "(CutFormula f) ∈ set l ⟹ l ⊢d (X ⊢⇩S f ⇩S) ⟹ l ⊢d (f ⇩S ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S Y)"
| 
Comma_impL_disp: "l ⊢d ((X ;⇩S Y) ⊢⇩S Z) ⟹ l ⊢d (X ⊢⇩S (Z ←⇩S Y))"|
Comma_impR_disp2: "l ⊢d (Y ⊢⇩S (X →⇩S Z)) ⟹ l ⊢d ((X ;⇩S Y) ⊢⇩S Z)"|
ImpL_comma_disp2: "l ⊢d ((Z ←⇩S Y) ⊢⇩S X) ⟹ l ⊢d (Z ⊢⇩S (X ;⇩S Y))"|
ImpR_comma_disp2: "l ⊢d ((X →⇩S Z) ⊢⇩S Y) ⟹ l ⊢d (Z ⊢⇩S (X ;⇩S Y))"|
ImpR_comma_disp: "l ⊢d (Z ⊢⇩S (X ;⇩S Y)) ⟹ l ⊢d ((X →⇩S Z) ⊢⇩S Y)"|
ImpL_comma_disp: "l ⊢d (Z ⊢⇩S (X ;⇩S Y)) ⟹ l ⊢d ((Z ←⇩S Y) ⊢⇩S X)"|
Comma_impR_disp: "l ⊢d ((X ;⇩S Y) ⊢⇩S Z) ⟹ l ⊢d (Y ⊢⇩S (X →⇩S Z))"|
Comma_impL_disp2: "l ⊢d (X ⊢⇩S (Z ←⇩S Y)) ⟹ l ⊢d ((X ;⇩S Y) ⊢⇩S Z)"
| 
Back_forw_A: "l ⊢d (X ⊢⇩S (forwA⇩S a Y)) ⟹ l ⊢d ((backA⇩S a X) ⊢⇩S Y)"|
Forw_back_A2: "l ⊢d (X ⊢⇩S (backA⇩S a Y)) ⟹ l ⊢d ((forwA⇩S a X) ⊢⇩S Y)"|
Forw_back_A: "l ⊢d ((forwA⇩S a X) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (backA⇩S a Y))"|
Back_forw_A2: "l ⊢d ((backA⇩S a X) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (forwA⇩S a Y))"
| 
Back_forw_K2: "l ⊢d ((backK⇩S a X) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (forwK⇩S a Y))"|
Back_forw_K: "l ⊢d (X ⊢⇩S (forwK⇩S a Y)) ⟹ l ⊢d ((backK⇩S a X) ⊢⇩S Y)"|
Forw_back_K2: "l ⊢d (X ⊢⇩S (backK⇩S a Y)) ⟹ l ⊢d ((forwK⇩S a X) ⊢⇩S Y)"|
Forw_back_K: "l ⊢d ((forwK⇩S a X) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (backK⇩S a Y))"
| 
Grishin_R2: "l ⊢d (W ⊢⇩S ((X →⇩S Y) ;⇩S Z)) ⟹ l ⊢d (W ⊢⇩S (X →⇩S (Y ;⇩S Z)))"|
Grishin_R: "l ⊢d (W ⊢⇩S (X →⇩S (Y ;⇩S Z))) ⟹ l ⊢d (W ⊢⇩S ((X →⇩S Y) ;⇩S Z))"|
Grishin_L: "l ⊢d ((X →⇩S (Y ;⇩S Z)) ⊢⇩S W) ⟹ l ⊢d (((X →⇩S Y) ;⇩S Z) ⊢⇩S W)"|
Grishin_L2: "l ⊢d (((X →⇩S Y) ;⇩S Z) ⊢⇩S W) ⟹ l ⊢d ((X →⇩S (Y ;⇩S Z)) ⊢⇩S W)"
| 
Refl_ForwK: "(LAgent a) ∈ set l ⟹ l ⊢d (X ⊢⇩S (forwK⇩S a Y)) ⟹ l ⊢d (X ⊢⇩S Y)"
| 
Bot_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S (⊥⇩F ⇩S))"|
Top_L: "l ⊢d (I⇩S ⊢⇩S X) ⟹ l ⊢d ((⊤⇩F ⇩S) ⊢⇩S X)"|
DImpR_L: "l ⊢d (((A ⇩S) →⇩S (B ⇩S)) ⊢⇩S Z) ⟹ l ⊢d (((A >-⇩F B) ⇩S) ⊢⇩S Z)"|
ImpL_R: "l ⊢d (Z ⊢⇩S ((B ⇩S) ←⇩S (A ⇩S))) ⟹ l ⊢d (Z ⊢⇩S ((B ←⇩F A) ⇩S))"|
DImpL_R: "l ⊢d (Y ⊢⇩S (B ⇩S)) ⟹ l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d ((Y ←⇩S X) ⊢⇩S ((B -<⇩F A) ⇩S))"|
And_L: "l ⊢d (((A ⇩S) ;⇩S (B ⇩S)) ⊢⇩S Z) ⟹ l ⊢d (((A ∧⇩F B) ⇩S) ⊢⇩S Z)"|
ImpR_R: "l ⊢d (Z ⊢⇩S ((A ⇩S) →⇩S (B ⇩S))) ⟹ l ⊢d (Z ⊢⇩S ((A →⇩F B) ⇩S))"|
Or_L: "l ⊢d ((B ⇩S) ⊢⇩S Y) ⟹ l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d (((A ∨⇩F B) ⇩S) ⊢⇩S (X ;⇩S Y))"|
Or_R: "l ⊢d (Z ⊢⇩S ((A ⇩S) ;⇩S (B ⇩S))) ⟹ l ⊢d (Z ⊢⇩S ((A ∨⇩F B) ⇩S))"|
ImpR_L: "l ⊢d ((B ⇩S) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d (((A →⇩F B) ⇩S) ⊢⇩S (X →⇩S Y))"|
DImpL_L: "l ⊢d (((B ⇩S) ←⇩S (A ⇩S)) ⊢⇩S Z) ⟹ l ⊢d (((B -<⇩F A) ⇩S) ⊢⇩S Z)"|
And_R: "l ⊢d (Y ⊢⇩S (B ⇩S)) ⟹ l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d ((X ;⇩S Y) ⊢⇩S ((A ∧⇩F B) ⇩S))"|
DImpR_R: "l ⊢d (Y ⊢⇩S (B ⇩S)) ⟹ l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d ((X →⇩S Y) ⊢⇩S ((A >-⇩F B) ⇩S))"|
ImpL_L: "l ⊢d ((B ⇩S) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d (((B ←⇩F A) ⇩S) ⊢⇩S (Y ←⇩S X))"|
Top_R: "l ⊢d (I⇩S ⊢⇩S (⊤⇩F ⇩S))"|
Bot_L: "l ⊢d ((⊥⇩F ⇩S) ⊢⇩S I⇩S)"
| 
FdiamA_L: "l ⊢d ((forwA⇩S alpha (A ⇩S)) ⊢⇩S X) ⟹ l ⊢d (((fdiamA⇩F alpha A) ⇩S) ⊢⇩S X)"|
One_R: "l ⊢d ((Phi⇩S alpha) ⊢⇩S ((One⇩F alpha) ⇩S))"|
BdiamA_R: "l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d ((backA⇩S alpha X) ⊢⇩S ((bdiamA⇩F alpha A) ⇩S))"|
FboxA_R: "l ⊢d (X ⊢⇩S (forwA⇩S alpha (A ⇩S))) ⟹ l ⊢d (X ⊢⇩S ((fboxA⇩F alpha A) ⇩S))"|
Pre_L: "(PreFormula alpha f) ∈ set l ⟹ l ⊢d (f ⇩S ⊢⇩S X) ⟹ l ⊢d ((One⇩F alpha)⇩S ⊢⇩S X)"|
BboxA_R: "l ⊢d (X ⊢⇩S (backA⇩S alpha (A ⇩S))) ⟹ l ⊢d (X ⊢⇩S ((bboxA⇩F alpha A) ⇩S))"|
BboxA_L: "l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d (((bboxA⇩F alpha A) ⇩S) ⊢⇩S (backA⇩S alpha X))"|
FboxA_L: "l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d (((fboxA⇩F alpha A) ⇩S) ⊢⇩S (forwA⇩S alpha X))"|
Pre_R: "(PreFormula alpha f) ∈ set l ⟹ l ⊢d (X ⊢⇩S f ⇩S) ⟹ l ⊢d (X ⊢⇩S (One⇩F alpha)⇩S)"|
BdiamA_L: "l ⊢d ((backA⇩S alpha (A ⇩S)) ⊢⇩S X) ⟹ l ⊢d (((bdiamA⇩F alpha A) ⇩S) ⊢⇩S X)"|
One_L: "l ⊢d ((Phi⇩S alpha) ⊢⇩S X) ⟹ l ⊢d (((One⇩F alpha) ⇩S) ⊢⇩S X)"|
FdiamA_R: "l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d ((forwA⇩S alpha X) ⊢⇩S ((fdiamA⇩F alpha A) ⇩S))"
| 
BdiamK_L: "l ⊢d ((backK⇩S a (A ⇩S)) ⊢⇩S X) ⟹ l ⊢d (((bdiamK⇩F a A) ⇩S) ⊢⇩S X)"|
FdiamK_R: "l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d ((forwK⇩S a X) ⊢⇩S ((fdiamK⇩F a A) ⇩S))"|
FboxK_R: "l ⊢d (X ⊢⇩S (forwK⇩S a (A ⇩S))) ⟹ l ⊢d (X ⊢⇩S ((fboxK⇩F a A) ⇩S))"|
BboxK_L: "l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d (((bboxK⇩F a A) ⇩S) ⊢⇩S (backK⇩S a X))"|
BboxK_R: "l ⊢d (X ⊢⇩S (backK⇩S a (A ⇩S))) ⟹ l ⊢d (X ⊢⇩S ((bboxK⇩F a A) ⇩S))"|
FboxK_L: "l ⊢d ((A ⇩S) ⊢⇩S X) ⟹ l ⊢d (((fboxK⇩F a A) ⇩S) ⊢⇩S (forwK⇩S a X))"|
FdiamK_L: "l ⊢d ((forwK⇩S a (A ⇩S)) ⊢⇩S X) ⟹ l ⊢d (((fdiamK⇩F a A) ⇩S) ⊢⇩S X)"|
BdiamK_R: "l ⊢d (X ⊢⇩S (A ⇩S)) ⟹ l ⊢d ((backK⇩S a X) ⊢⇩S ((bdiamK⇩F a A) ⇩S))"
| 
W_impL_R: "l ⊢d (X ⊢⇩S Z) ⟹ l ⊢d ((X ←⇩S Z) ⊢⇩S Y)"|
ImpL_I: "l ⊢d (X ⊢⇩S Y) ⟹ l ⊢d ((X ←⇩S Y) ⊢⇩S I⇩S)"|
W_impL_L: "l ⊢d (X ⊢⇩S Z) ⟹ l ⊢d (Y ⊢⇩S (Z ←⇩S X))"|
ImpR_I2: "l ⊢d ((Y →⇩S X) ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S Y)"|
E_R: "l ⊢d (X ⊢⇩S (Y1 ;⇩S Y2)) ⟹ l ⊢d (X ⊢⇩S (Y2 ;⇩S Y1))"|
IW_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S Y)"|
IW_L: "l ⊢d (I⇩S ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S Y)"|
A_L2: "l ⊢d ((X ;⇩S (Y ;⇩S Z)) ⊢⇩S W) ⟹ l ⊢d (((X ;⇩S Y) ;⇩S Z) ⊢⇩S W)"|
E_L: "l ⊢d ((X1 ;⇩S X2) ⊢⇩S Y) ⟹ l ⊢d ((X2 ;⇩S X1) ⊢⇩S Y)"|
A_R: "l ⊢d (W ⊢⇩S ((X ;⇩S Y) ;⇩S Z)) ⟹ l ⊢d (W ⊢⇩S (X ;⇩S (Y ;⇩S Z)))"|
W_impR_R: "l ⊢d (X ⊢⇩S Z) ⟹ l ⊢d (Y ⊢⇩S (X →⇩S Z))"|
C_L: "l ⊢d ((X ;⇩S X) ⊢⇩S Y) ⟹ l ⊢d (X ⊢⇩S Y)"|
C_R: "l ⊢d (X ⊢⇩S (Y ;⇩S Y)) ⟹ l ⊢d (X ⊢⇩S Y)"|
ImpR_I: "l ⊢d (X ⊢⇩S Y) ⟹ l ⊢d ((Y →⇩S X) ⊢⇩S I⇩S)"|
W_impR_L: "l ⊢d (X ⊢⇩S Z) ⟹ l ⊢d ((Z →⇩S X) ⊢⇩S Y)"|
A_L: "l ⊢d (((X ;⇩S Y) ;⇩S Z) ⊢⇩S W) ⟹ l ⊢d ((X ;⇩S (Y ;⇩S Z)) ⊢⇩S W)"|
A_R2: "l ⊢d (W ⊢⇩S (X ;⇩S (Y ;⇩S Z))) ⟹ l ⊢d (W ⊢⇩S ((X ;⇩S Y) ;⇩S Z))"|
I_impR2: "l ⊢d (I⇩S ⊢⇩S (X →⇩S Y)) ⟹ l ⊢d (X ⊢⇩S Y)"|
I_impL: "l ⊢d (X ⊢⇩S Y) ⟹ l ⊢d (I⇩S ⊢⇩S (Y ←⇩S X))"|
I_impR: "l ⊢d (X ⊢⇩S Y) ⟹ l ⊢d (I⇩S ⊢⇩S (X →⇩S Y))"|
ImpL_I2: "l ⊢d ((X ←⇩S Y) ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S Y)"|
I_impL2: "l ⊢d (I⇩S ⊢⇩S (Y ←⇩S X)) ⟹ l ⊢d (X ⊢⇩S Y)"
| 
A_nec_L: "l ⊢d (I⇩S ⊢⇩S X) ⟹ l ⊢d ((backA⇩S a I⇩S) ⊢⇩S X)"|
A_mon_L: "l ⊢d (((backA⇩S a X) ;⇩S (backA⇩S a Y)) ⊢⇩S Z) ⟹ l ⊢d ((backA⇩S a (X ;⇩S Y)) ⊢⇩S Z)"|
Mon_A_R: "l ⊢d (Z ⊢⇩S ((forwA⇩S a X) ;⇩S (forwA⇩S a Y))) ⟹ l ⊢d (Z ⊢⇩S (forwA⇩S a (X ;⇩S Y)))"|
Nec_A_L: "l ⊢d (I⇩S ⊢⇩S X) ⟹ l ⊢d ((forwA⇩S a I⇩S) ⊢⇩S X)"|
FS_A_L: "l ⊢d (((forwA⇩S a Y) →⇩S (forwA⇩S a Z)) ⊢⇩S X) ⟹ l ⊢d ((forwA⇩S a (Y →⇩S Z)) ⊢⇩S X)"|
FS_A_R: "l ⊢d (X ⊢⇩S ((forwA⇩S a Y) →⇩S (forwA⇩S a Z))) ⟹ l ⊢d (X ⊢⇩S (forwA⇩S a (Y →⇩S Z)))"|
A_mon_R: "l ⊢d (Z ⊢⇩S ((backA⇩S a X) ;⇩S (backA⇩S a Y))) ⟹ l ⊢d (Z ⊢⇩S (backA⇩S a (X ;⇩S Y)))"|
A_FS_R: "l ⊢d (X ⊢⇩S ((backA⇩S a Y) →⇩S (backA⇩S a Z))) ⟹ l ⊢d (X ⊢⇩S (backA⇩S a (Y →⇩S Z)))"|
Nec_A_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S (forwA⇩S a I⇩S))"|
Mon_A_L: "l ⊢d (((forwA⇩S a X) ;⇩S (forwA⇩S a Y)) ⊢⇩S Z) ⟹ l ⊢d ((forwA⇩S a (X ;⇩S Y)) ⊢⇩S Z)"|
A_FS_L: "l ⊢d (((backA⇩S a Y) →⇩S (backA⇩S a Z)) ⊢⇩S X) ⟹ l ⊢d ((backA⇩S a (Y →⇩S Z)) ⊢⇩S X)"|
A_nec_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S (backA⇩S a I⇩S))"
| 
Reduce_R: "l ⊢d (Y ⊢⇩S ((Phi⇩S a) →⇩S (forwA⇩S a X))) ⟹ l ⊢d (Y ⊢⇩S (forwA⇩S a X))"|
CompA_R: "l ⊢d (Y ⊢⇩S (forwA⇩S a (backA⇩S a X))) ⟹ l ⊢d (Y ⊢⇩S ((Phi⇩S a) →⇩S X))"|
Balance: "l ⊢d (X ⊢⇩S Y) ⟹ l ⊢d ((forwA⇩S a X) ⊢⇩S (forwA⇩S a Y))"|
CompA_L: "l ⊢d ((forwA⇩S a (backA⇩S a X)) ⊢⇩S Y) ⟹ l ⊢d (((Phi⇩S a) ;⇩S X) ⊢⇩S Y)"|
Reduce_L: "l ⊢d (((Phi⇩S a) ;⇩S (forwA⇩S a X)) ⊢⇩S Y) ⟹ l ⊢d ((forwA⇩S a X) ⊢⇩S Y)"
| 
K_nec_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S (backK⇩S a I⇩S))"|
Nec_K_L: "l ⊢d (I⇩S ⊢⇩S X) ⟹ l ⊢d ((forwK⇩S a I⇩S) ⊢⇩S X)"|
K_mon_L: "l ⊢d (((backK⇩S a X) ;⇩S (backK⇩S a Y)) ⊢⇩S Z) ⟹ l ⊢d ((backK⇩S a (X ;⇩S Y)) ⊢⇩S Z)"|
Mon_K_L: "l ⊢d (((forwK⇩S a X) ;⇩S (forwK⇩S a Y)) ⊢⇩S Z) ⟹ l ⊢d ((forwK⇩S a (X ;⇩S Y)) ⊢⇩S Z)"|
FS_K_L: "l ⊢d (((forwK⇩S a Y) →⇩S (forwK⇩S a Z)) ⊢⇩S X) ⟹ l ⊢d ((forwK⇩S a (Y →⇩S Z)) ⊢⇩S X)"|
FS_K_R: "l ⊢d (X ⊢⇩S ((forwK⇩S a Y) →⇩S (forwK⇩S a Z))) ⟹ l ⊢d (X ⊢⇩S (forwK⇩S a (Y →⇩S Z)))"|
Mon_K_R: "l ⊢d (Z ⊢⇩S ((forwK⇩S a X) ;⇩S (forwK⇩S a Y))) ⟹ l ⊢d (Z ⊢⇩S (forwK⇩S a (X ;⇩S Y)))"|
K_mon_R: "l ⊢d (Z ⊢⇩S ((backK⇩S a X) ;⇩S (backK⇩S a Y))) ⟹ l ⊢d (Z ⊢⇩S (backK⇩S a (X ;⇩S Y)))"|
K_FS_L: "l ⊢d (((backK⇩S a Y) →⇩S (backK⇩S a Z)) ⊢⇩S X) ⟹ l ⊢d ((backK⇩S a (Y →⇩S Z)) ⊢⇩S X)"|
Nec_K_R: "l ⊢d (X ⊢⇩S I⇩S) ⟹ l ⊢d (X ⊢⇩S (forwK⇩S a I⇩S))"|
K_FS_R: "l ⊢d (X ⊢⇩S ((backK⇩S a Y) →⇩S (backK⇩S a Z))) ⟹ l ⊢d (X ⊢⇩S (backK⇩S a (Y →⇩S Z)))"|
K_nec_L: "l ⊢d (I⇩S ⊢⇩S X) ⟹ l ⊢d ((backK⇩S a I⇩S) ⊢⇩S X)"
| 
Swapin_L: "(RelAKA rel) ∈ set l ⟹ l ⊢d (forwA⇩S alpha (forwK⇩S a X) ⊢⇩S Y) ⟹ beta ∈ set (rel alpha a) ⟹ l ⊢d ((Phi⇩S alpha) ;⇩S (forwK⇩S a (forwA⇩S beta X)) ⊢⇩S Y)"|
Swapin_R: "(RelAKA rel) ∈ set l ⟹ l ⊢d (Y ⊢⇩S forwA⇩S alpha (forwK⇩S a X)) ⟹ beta ∈ set (rel alpha a) ⟹ l ⊢d (Y ⊢⇩S (Phi⇩S alpha) →⇩S (forwK⇩S a (forwA⇩S beta X)))"
| 
Swapout_L: "(RelAKA rel) ∈ set l ⟹ (∀ Y ∈ (set Ys). ∃beta ∈ set (rel alpha a). (l ⊢d forwK⇩S a (forwA⇩S beta X) ⊢⇩S Y) ) ⟹ l ⊢d forwA⇩S alpha (forwK⇩S a X) ⊢⇩S ;;⇩S Ys"|
Swapout_R: "(RelAKA rel) ∈ set l ⟹ (∀ Y ∈ (set Ys). ∃beta ∈ set (rel alpha a). (l ⊢d Y ⊢⇩S forwK⇩S a (forwA⇩S beta X)) ) ⟹ l ⊢d  ;;⇩S Ys ⊢⇩S forwA⇩S alpha (forwK⇩S a X)"
| 
Id: "l ⊢d (((p ⇩F) ⇩S) ⊢⇩S ((p ⇩F) ⇩S))"|
Atom: "atom seq ⟹ l ⊢d seq"
(*calc_structure_rules_se-END*)

end