% starts comments
% run with SPASS -Isabelle=1 [other options] [inputfile] for a set of options related to the paper.
begin_problem(identifier).
list_of_descriptions.
name({**}).
author({**}).
status(unknown).
description({**}).
end_of_list.
% up to here minimal required beginning. You could add text inbetween the two **.
% Every function, predicate and type symbol has to be declared including its arity
% For the monomorphic version (SPASS 3.8ds) types can only be type constants e.g. "nat"
% Predefined types include: Natural, Integer, Rational, Real and Top. They must not be used.
list_of_symbols.
functions [ (c, 0) , (f, 1), (g, 2)].
predicates [(p, 2)].
sorts [nat, t].
end_of_list.
% For every function and predicate symbol you have to declare its type.
% For the monomorphic version (SPASS 3.8ds) types can only be type constants e.g. "nat"
list_of_declarations.
function(c, t).
function(f, (t) nat).
function(g, (nat, t) nat).
predicate(p, nat, t).
end_of_list.
%list all axioms
% the general shape is: formula( ... , optional formula name, optional rank) if you want to give a rank you also have to provide a name
% default rank is 1000, less is more important
% SPASS has a flag that will tell you a list of all the names of the formulas it has used for the proof and the proof itself
% forall, exists, and, or, not, implies, false, true, equal, equiv are the keywords
% equality can be annotated to be oriented from left to right by writing it as equal:lr(leftterm , rightterm)
list_of_formulae(axioms).
formula(forall([X : nat, Y : t], and(or(p(f(c), c),not(p(f(f(c)),c)),true))), formula_name, 1000).
formula(implies(false,equal(f(c),f(f(c))))).
end_of_list.
%list conjecture
list_of_formulae(conjectures).
formula(forall([X : t],equal(f(f(f(f(X)))),c)), conj_0).
end_of_list.
end_problem.