Conceptadvanced
Inductive invariant
Also called Inductive invariant of a transition system.
An invariant that holds initially and is preserved by every transition, so it holds in all reachable states.
An invariant that holds initially and is preserved by every transition, so it holds in all reachable states.
About this page
The build computes these levels from the evidence in the repository. Each row says what the next level needs. Read what the levels mean.
| Ladder | Level | What the next level needs |
|---|---|---|
| Human proof | H0 no proof |
|
| Lean | L0 no Lean part |
|
| Visual | V0 none |
|
| Writing | W0 stub |
|
Tag TFE5WF Edit this page History Report an error