Module Common.OracleSource

is_true meta p check if the predicate p is true in the original theory.

is_true_axiom meta s s' check if the predicate Axiom s s' is true in the original theory.

is_true_cumul meta s s' check if the predicate Cumul s s' is true in the original theory.

is_true_rule meta s s' s'' check if the predicate Rule s s' s'' is true in the original theory.

mk_theory meta i computes a theory for the universes up to i. A theory is an array for each predicate that tells if the predicate holds. The array is index by universes and its dimension is the arity of the predicate.