зеркало из https://github.com/microsoft/ivy.git
22 строки
347 B
XML
22 строки
347 B
XML
#lang ivy1.6
|
|
|
|
type t
|
|
relation succ(X:t,Y:t)
|
|
|
|
schema existsE = {
|
|
type t
|
|
relation p(X:t)
|
|
property exists X. p(X)
|
|
fresh function n:t
|
|
#----------------------
|
|
property p(n)
|
|
}
|
|
|
|
axiom exists Y. succ(X,Y)
|
|
|
|
function next(X:t):t
|
|
|
|
property succ(X,next(X))
|
|
proof existsE with n = next(X), p(Y) = succ(X,Y)
|
|
|