%%% Example proofs: modal axioms
% Insert some redundant !G or ?G to make them normal
% in the sense defined by "norm"

ax1 : (! A => A) @ W0
    = (=>I ([x] !E x)).
ax2 : (! A => ! ! A) @ W0
    = (=>I ([x] !I ([o] !I [o'] !E (!G x)))).
ax3 : (A => ? A) @ W0
    = (=>I ([x] ?I x)).
ax4 : (? ? A => ? A) @ W0
    = (=>I ([x] ?E x ([o][y] ?E (?G y) ([o'][y'] (?G (?I y')))))).
ax4' : (? ? A => ? A) @ W0
     = (=>I ([x] ?E x ([o][y] ?G y))).
ax5 : (? A => ! ? A) @ W0
    = (=>I ([x] ?E x ([o][y] !I ([o'] ?G (?I y))))).
ax5' : (? A => ! ? A) @ W0
     = (=>I ([x] !I ([o] ?G x))).
ax6 : (? ! A => ! A) @ W0
    = (=>I ([x] ?E x ([o][y] !I ([o'] (!E (!G y)))))).
ax6' : (? ! A => ! A) @ W0
     = (=>I ([x] ?E x ([o][y] !G y))).
ax7 : (! (A => B) => ! A => ! B) @ W0
    = (=>I ([x] =>I ([y] !I ([o] =>E (!E (!G x)) (!E (!G y)))))).
ax8 : (! (A => B) => ? A => ? B) @ W0
    = (=>I ([x] =>I ([y] ?E y ([o][y'] (?G (?I (=>E (!E (!G x)) y'))))))).
ax9 : ((? A => ! B) => ! (A => B)) @ W0
    = (=>I ([x] !I ([o] =>I ([y] !E (!G (=>E x (?G (?I y)))))))).

% Sample normalizations
% N is always unique, but there are multiple normalizations
% due to the non-determinism in cut elimination
% limit to find first solution

%query 1 1 normalize ax1 N.
%query 6 1 normalize ax2 N.
%query 1 1 normalize ax3 N.
%query 9 1 normalize ax4 N.
%query 1 1 normalize ax4' N.
%query 3 1 normalize ax5 N.
%query 1 1 normalize ax5' N.
%query 6 1 normalize ax6 N.
%query 2 1 normalize ax6' N.
%query 36 1 normalize ax7 N.
%query 60 1 normalize ax8 N.
%query 30 1 normalize ax9 N.