# LP, the Larch Prover -- The fix command

The fix command provides a method of forward inference, which can be used to eliminate an existential quantifier from a fact in LP's logical system.

## Syntax

```<fix-command> ::= fix <variable> as <term> in <names>
```

## Examples

```fix x as s(0) in *Hyp
```

## Usage

The fix command eliminates the unique accessible prenex-existential quantifier over the variable from the named facts and substitutes the term for all occurrences of the variable bound by that quantifier. For example, given the formulas
```user.1: \E x \A y (f(y) = x)
user.2: \E z (x < z)
```
the commands fix x as c in user and fix z as bigger(x) in user produce the results
```user.1.1: f(y) = c
user.2.1: x < bigger(x)
```

LP will reject a fix command unless the following conditions are satisfied.

• The named facts must contain exactly one accessible prenex-existential quantifier over the variable (because it is not sound to instantiate two different existential quantifiers by the same term).

• The term must have the form sk(x1, ..., xn), where sk is a function identifier that does not appear in any fact or in the current conjecture, and where x1, ..., xn include all variables that are bound by outer (explicit or implicit) prenex-universal quantifiers in the formula containing the eliminated quantifier. See Skolem function.
LP automatically changes bound variables in the named facts, as needed, to avoid having them bind (or capture) variables that occur free in the term. This action, together with the above two conditions, guarantee that the results constitute a conservative extension to LP's logical system, i.e., that any consequence of the extended system is either a consequence of the original system or contains an occurrence of sk. The last condition prevents unsound derivations such as c ~= c from \E x (x ~= c) or \A y (c = y) from \A y \E x (x = y).