Abstract

ABSTRACT We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and [086], The method is given by a system of rules of formation of proofs. The proofs of f is defined' and the proofs of correctness ‘φ)' formed by application of the rules of the system are such that they contain a computation of the value f, where f is a partial function valued in natural numbers and is a vector of natural numbers. We show that the system is complete, i.e. if an equation holds in every model then it has a proof formed by application of the rules of the system. The system is equipped with a method of visual presentation of proofs by nested commutative triangles, i.e. commutative triangles which contain in their interiors other commutative triangles which may be also nested. To provide formal foundations for the method of visual presentation of proofs we give a mathematical description of nested commutative triangles in terms of directed graphs and graph homomorphisms. AMS Subject Classification 1995: Primary: 68. Secondary: 18.