Download Ontic: Language Specification and User`s Manual Robert Givan

(show (is (f x) (an-operator-from τ2 to σ))
. . .)))
(show (is f (a-function-from τ to σ))
(show (is (a-domain-member-of f ) τ )
. . .)
(show (is τ (a-domain-member-of f ))
. . .)
(suppose-there-is ((x τ ))
(show (is (f x) σ))
. . .)
(show (singleton (f x))
. . .))
(show (is f (a-function-from τ1 τ2 to σ))
(show (is (a-domain-member-of f ) τ1 )
. . .)
(show (is τ1 (a-domain-member-of f ))
. . .)
(suppose-there-is ((x τ1 ))
(show (is (f x) (a-function-from τ2 to σ))
. . .)))
5.8
Induction Proofs
Proving facts about recursively defined thunks and operators requires mathematical induction. For example, consider the following definition of a a-node-connected-to.
The operator a-node-connected-to takes two arguments, a graph and a
node in the graph, and nondeterministically returns any node that can be
reached from the given node by traversing arcs of the graph.
(define (a-node-connected-to (g (a-graph)) (n (a-node-of g)))
60