Svejdar proof method for GL logic

Svejdar proof method for GL logic

Proof
1 : p, []-(p + q), []-q, []-p  |--  q, p   initial sequent
2 : q, []-(p + q), []-q, []-p  |--  q, p   initial sequent
3 : (p + q), []-(p + q), []-q, []-p  |--  q, p  by orL     applied to 1, 2
4 : []-(p + q), []-q, []-p  |--  -(p + q), q, p  by notL    applied to 3
5 : -p, []-(p + q), []-q, []-p  |--  q, -(p + q)  by notR    applied to 4
6 : -q, -p, []-(p + q), []-q, []-p  |--  -(p + q)  by notR    applied to 5
7 : []-q, []-p  |--  []-(p + q)  by necR    applied to 6
8 : []-p  |--  <>q, []-(p + q)  by posR    applied to 7
9 :   |--  <>p, <>q, []-(p + q)  by posR    applied to 8
10 :   |--  (<>p + <>q), []-(p + q)  by orR     applied to 9
11 : <>(p + q)  |--  (<>p + <>q)  by posL    applied to 10
12 :   |--  (<>(p + q) => (<>p + <>q))  by implyR  applied to 11
13 : p, []-p, []-(p + q)  |--  q, p   initial sequent
14 : []-p, []-(p + q)  |--  -p, q, p  by notL    applied to 13
15 : []-p, []-(p + q)  |--  (p + q), -p  by orR     applied to 14
16 : -(p + q), []-p, []-(p + q)  |--  -p  by notR    applied to 15
17 : []-(p + q)  |--  []-p  by necR    applied to 16
18 :   |--  <>(p + q), []-p  by posR    applied to 17
19 : <>p  |--  <>(p + q)  by posL    applied to 18
20 : q, []-q, []-(p + q)  |--  q, p   initial sequent
21 : []-q, []-(p + q)  |--  -q, q, p  by notL    applied to 20
22 : []-q, []-(p + q)  |--  (p + q), -q  by orR     applied to 21
23 : -(p + q), []-q, []-(p + q)  |--  -q  by notR    applied to 22
24 : []-(p + q)  |--  []-q  by necR    applied to 23
25 :   |--  <>(p + q), []-q  by posR    applied to 24
26 : <>q  |--  <>(p + q)  by posL    applied to 25
27 : (<>p + <>q)  |--  <>(p + q)  by orL     applied to 19, 26
28 :   |--  ((<>p + <>q) => <>(p + q))  by implyR  applied to 27
29 :   |--  (<>(p + q) <=> (<>p + <>q))  by equivR  applied to 12, 28