branch

The built-in function branch returns a sentence of the form C if A | B is true, C can be proven from A, and C can be proven from B.

Syntax

branch([sentence argument expression], [variable identifier], [variable identifier], ...){
        ...
        return [return expression];
} or {
        ...
        return [return expression];
} or ...
}

Behavior

branch accepts one sentence expression value and two or more variable identifiers. The argument sentence must be verified, have a top-level | connective, and not have an unbound object or predicate, otherwise an error is raised.

After the ) character is one or more scopes. Between consecutive scopes is or. The number of scopes must be the same as the number of variable identifiers.

In the n-th scope, a variable with the n-th variable identifier is created.

Inside of the first scope, the argument sentence up to the first top-level | is stored as a verified sentence for the first variable identifier. At the end of the scope, a verified sentence must be returned. The return value of branch is the return value of the first scope.

For n > 1, inside of the n-th scope the argument sentence between the (n-1)-th top-level | and the n-th top-level | (or the end of the sentence if the scope is the last scope) is stored as a verified sentence for the n-th variable identifier. At the end of the scope, a verified sentence must be returned. If the return value of the scope is not trivially equivalent to the return value of the first scope, an error is raised.

Examples

Suppose = and in are relations, and that successor is a predicate such that successor(A, B) if and only if:

*X(X in A <-> X in B | X = B)

In other words, suppose the above sentence is the sentence definition of successor when A and B are considered unbound objects.

Suppose X, A, and B are objects, result is a predicate depending on one object, lem0 stores the verified sentence:

*Y(Y in B -> result(B))

And lem1 stores the verified sentence:

X = B -> result(B)

Finally, suppose arg0 stores the verified sentence:

successor(A, B)

And arg1 stores the verified sentence:

X in A

Then the following expression:

branch(expand(arg0)(X)(arg1), X_in_B, X_eq_B){
        return lem0(X)(X_in_B);
} or {
        return lem1(X_eq_B);
}

Evaluates to the verified sentence:

result(B)