lemmas_Gen.tptp

%---------------------------------------------------------------------------
% Problem : hets_exported
% Name    : <lemmas?Gen>
% Author  : hets
% Status  : unknown
% Desc    :
% Date    : 2015-06-23 08:36:33.239316 UTC
% Option  :
%---------------------------------------------------------------------------
fof(declaration0,axiom,
    ! [X1, X2] : ((g(X1) & g(X2)) => g(auxfunc(X1, X2)))).
fof(declaration1,axiom,
    ! [X1, X2] : ((h(X1) & g(X2)) => g(constructor(X1, X2)))).
fof(declaration2,axiom,
    g(null)).
fof(declaration3,axiom,
    ! [X1, X2] : ((g(X1) & g(X2)) => g(qrecfunc(X1, X2)))).
fof(declaration4,axiom,
    ! [X1] : (g(X1) => g(recfunc(X1)))).
fof(disjoint_sorts_g_h,axiom,
    ! [Y1, Y2] : ((g(Y1) & h(Y2)) => ~ Y1 = Y2)).
fof(ga_non_empty_sort_g,axiom,
    ? [Y] : g(Y)).
fof(ga_non_empty_sort_h,axiom,
    ? [Y] : h(Y)).