:- module(cti,[ {}/0, {}/1 ]).
:- use_module(library(term),[acylic_term/1]).

{}.

{Expr} :-
	( \+ b_valid(Expr) -> throw(condition_failed(Expr)) ; true ).

b_valid(Expr) :-
	nonvar(Expr),
	nb_valid(Expr).

nb_valid(b(V)) :-
	ground(V),
	acyclic_term(V).
nb_valid((A,B)) :-
	b_valid(A),
	b_valid(B).
nb_valid((A;_B)) :-
	b_valid(A).
nb_valid((_A;B)) :-
	b_valid(B).