Example

From Automated Assistance for Formal Reasoning

Jump to: navigation, search

The main page cannot be edited by anonymous users, so the example on the main page is reproduced on this page for experimentation.

Introduce f.
Assume f is a total function from \mathbb{N} to \mathbb{N} and f is injective.
Assert for any x,y \in \mathbb{N}, if x \neq y then f(x) \neq f(y).


To see which relations and predicates apply to an expression within an argument, use the ?...? notation instead of the $...$ notation around an expression. For example, clicking verify given the following assertion produces a list of predicates and relations that govern the variable x (assuming the statement is within a validation context of the form vbeg...vend).

Assert for any x \in \mathbb{N}, ?x?.

To list the predicates and relations that apply to more than one expression, list the expressions in a comma-separated list between ?...?.

Assert for any x,y \in \mathbb{N}, if x > y then ?x,y?.
Retrieved from "http://www.aartifact.org/wiki/index.php/Example"
Personal tools
course projects
ongoing projects