- s "?x"; {?x} ?x - ri "BIND@?x"; ex(); {[?1] @ ?x} (* [?1] is the identity function *) [?1] @ ?x - ri "EVAL"; ex(); (* evaluate the function *) {?x} ?x - s "[?1]"; {[?1]} [?1] - ri "BIND@?y"; ex(); {[[?2]] @ ?y} (* [[?2]] is the constant function [[?2]] @ ?y whose value is [?1]; this is an example of relabelling of bound variables *) - ri "EVAL"; ex(); {[?1]} [?1] (* abstraction does not need to be with respect to atomic terms *) - s "(?x+?y)=?x+?y"; {(?x + ?y) = ?x + ?y} (?x + ?y) = ?x + ?y - ri "BIND@?x+?y"; ex(); {[?1 = ?1] @ ?x + ?y} [?1 = ?1] @ ?x + ?y s "3+3"; {3 + 3} 3 + 3 - ri "UNEVAL@[?1+?1]"; ex(); {[?1 + ?1] @ 3} [?1 + ?1] @ 3 (* definition of the universal quantifier *) (* a full account of definition commands is given in a later section *) - defineconstant "forall@?x" "?x=[true]"; forall: forall @ ?x = ?x = [true] forall , 0 (* definition of the existential quantifier *) - defineconstant "forsome@?x" "~forall@[~?x@?1]"; forsome: forsome @ ?x = ~ forall @ [~ ?x @ ?1] forsome , 0