Color Codes in KIV Proof Trees

Node colors in proof trees encode the type of applied rule as follows:

• Red nodes either use an induction rule, apply an induction hypothesis or apply the invariant rule for loops.
• Green nodes instantiate quantifiers.
• Blue nodes are either case splits or unfold procedure calls.
• Brown nodes apply the weakening rule of sequent calculus.
• Purple nodes either unwind loops or execute the step rule of KIV's temporal logic.
• All other nodes are black and stand for simplification steps.

Filled nodes are automatic steps done by some heuristic. Unfilled nodes are interactive steps.

Named premises are applied lemmas either from the current specification (green) or from some subspecification (blue).

Edges of closed proof branches are green. Edges that lead to open premises are red.