# [PVS-Help] Circular dependencies in judgements of PVS 4.0

```
Before digging into my particular problem, I have a general question.
pvs-system-guide.pdf, section "2.2 Parsing and Typechecking" states that
TCCs must be proved before theorems in a theory. If so, why am I allowed
to use lemmas of a theory in proofs of a TCC? In contrast to that, if I
prove a lemma and try to use a lemma which is defined later in the same
PVS file, the interactive PVS prover considers the later lemma as
non-existent. As a side note: I would also like to use lemmas of a theory
in proofs of TCCs of the same theory. If the order is like those of "Proof
Status", that is
lemmaA_TCC1
lemmaA
lemmaB_TCC1
lemmaB_TCC2
lemmaB
would there be any chance of a circular reasoning?

Now the particular problem: I'm working on a theory of multi-sets, which I
have designed analogously to Prelude's "sets" and "finite_sets" theories.
(I'm afraid, I'm duplicating work, however it is a nice exercise to get
started with PVS.) I have the functions 'remove', which removes one
element from a multiset, and 'remove_all', which removes all instances of
an element from a multiset. Now I have the judgements

x: VAR T

A: VAR finite_multiset

finite_remove: JUDGEMENT remove(x, A) HAS_TYPE finite_multiset

finite_remove_all: JUDGEMENT remove_all(x, A) HAS_TYPE finite_multiset

The proofs of the statements are practically identical, because both
'remove' and 'remove_all' generate subsets of A. However the proof of
'finite_remove' is considered complete, whereas the one of
'finite_remove_all' is considered incomplete, due to an circularity with
the definition of 'finite_multiset'. I compared the proof and definition
chains of 'finite_remove' and 'finite_remove_all' and I found no
differences with respect to the objects of the same module. I reduced the
proof of 'finite_remove_all' in order to see, which lemma invokation
causes the circularity. I ended up with a simple (POSTPONE) and the proof
is still considered circular (although now UNPROVED). How can I find out