# Macros¶

Generated on: ${new Date()} by `gendoc.groovy`

.

Covering the macros of KeY.

## Full Auto Pilot (`autopilot`

)¶

Auto Pilot

- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions
- Try to close all proof obligations

## Auto pilot (preparation only) (`autopilot-prep`

)¶

Auto Pilot

- Finish symbolic execution
- Separate proof obligations
- Expand invariant definitions

## Full Information Flow Auto Pilot (`infflow-autopilot`

)¶

Information Flow

- Search exhaustively for applicable position, then
- Start auxiliary computation
- Finish symbolic execution
- Try to close as many goals as possible
- Apply macro recursively
- Finish auxiliary computation
- Use information flow contracts
- Try to close as many goals as possible

## Propositional expansion (w/o splits) (`nosplit-prop`

)¶

Propositional

Apply rules to decompose propositional toplevel formulas; does not split the goal.

## One Single Proof Step (`onestep`

)¶

Simplification

One single proof step is applied

## Heap Simplification (`simp-heap`

)¶

Simplification

This macro performs simplification of Heap and LocSet terms. It applies simplification rules (including the "unoptimized" select rules), One Step Simplification, alpha, and delta rules.

## Update Simplification Only (`simp-upd`

)¶

Simplification

Applies only update simplification rules

## Propositional expansion (w/ splits) (`split-prop`

)¶

Propositional

Apply rules to decompose propositional toplevel formulas; splits the goal if necessary

## Finish symbolic execution (`symbex`

)¶

Auto Pilot

Continue automatic strategy application until no more modality is on the sequent.

## Close provable goals below (`tryclose`

)¶

null

Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.