Template:L theorem

From Event-B
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Usage

Template use to typeset a theorem in an event-b listing. (use Template:l_invariant)

Example

MACHINE

AntiCollide

REFINES

Safety

SEES

Network

Acyclic

VARIABLES

v1

v2

THEOREMS

inv1 :
v2 \in BOOL

END

Template

{{{1}}} :

{{{2}}}