%------------------------------------------------------------------------------
% File     : KLE001+6 : TPTP v7.2.0. Released v3.6.0.
% Domain   : Kleene Algebra
% Axioms   : Modal operators
% Version  : [Hoe08] axioms.
% English  :

% Refs     : [DMS06] Desharnais et al. (2006), Kleene Algebra with Domain
%          : [MS06]  Moeller & Struth (2006), Algebras of Modal Operators a
%          : [DS08]  Desharnais & Struth (2008), Modal Semirings Revisited
%          : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% Source   : [Hoe08]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    6 (   6 unit)
%            Number of atoms       :    6 (   6 equality)
%            Maximal formula depth :    3 (   3 average)
%            Number of connectives :    0 (   0 ~  ;   0  |;   0  &)
%                                         (   0 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
%            Number of functors    :   10 (   0 constant; 1-2 arity)
%            Number of variables   :   11 (   0 singleton;  11 !;   0 ?)
%            Maximal term depth    :    4 (   3 average)
% SPC      : 

% Comments : Requires KLE001+4.ax
%          : With KLE001+0 and KLE001+4.ax generates modal semirings
%            With KLE002+0 and KLE001+4.ax generates modal Kleene Algebra
%            With KLE003+0 and KLE001+4.ax generates modal Omega Algebra
%          : Defines forward/backward box and diamond (and domain).
%------------------------------------------------------------------------------
%----Standard axioms for forward/backward box and diamond
fof(complement,axiom,(
    ! [X0] : c(X0) = antidomain(domain(X0)) )).

fof(domain_difference,axiom,(
    ! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)) )).

fof(forward_diamond,axiom,(
    ! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))) )).

fof(backward_diamond,axiom,(
    ! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)) )).

fof(forward_box,axiom,(
    ! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))) )).

fof(backward_box,axiom,(
    ! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))) )).

%------------------------------------------------------------------------------