anthem-rs/examples/example-1.spec

input: p/1.

assert:
	forall N
	(
		forall X (p(X) -> exists I exists M (I = M and I = X and I <= N))
		-> forall X (q(X) -> exists I exists M (I = M and I = X and I <= 2 * N))
	).
Support hiding auxiliary predicates 2020-05-13 07:41:01 +02:00			`input: p/1.`

Add specification for example 1 2020-05-12 04:33:52 +02:00			`assert:`
			`forall N`
			`(`
			`forall X (p(X) -> exists I exists M (I = M and I = X and I <= N))`
			`-> forall X (q(X) -> exists I exists M (I = M and I = X and I <= 2 * N))`
			`).`