Matita Home

`applyS t auto_params`

- Synopsis:
**applyS***sterm**auto_params*- Pre-conditions:
**t**must have type**T**._{1}→ ... → T_{n}→ G- Action:
**applyS**is useful when**apply**fails because the current goal and the conclusion of the applied theorems are extensionally equivalent up to instantiation of metavariables, but cannot be unified. E.g. the goal is**P(n*O+m)**and the theorem to be applied proves**∀m.P(m+O)**.It tries to automatically rewrite the current goal using auto paramodulation to make it unifiable with

**G**. Then it closes the current sequent by applying**t**to**n**implicit arguments (that become new sequents). The**auto_params**parameters are passed directly to**auto paramodulation**.- New sequents to prove:
It opens a new sequent for each premise

**T**that is not instantiated by unification._{i}**T**is the conclusion of the_{i}**i**-th new sequent to prove.