// Theorem 1 (mutual exclusion)

num_crit <= 1

// Lemma C
// If the crical section is occupied then eventually it becomes clear

num_crit > 0 => P>=1 [ F num_crit = 0 ]

// Lemma D
// If a process is between 4 and 13 (in our version) then eventually some process gets to 14

"some_4_13" => P>=1 [ F "some_14" ]

// Theorem 2 (liveness)
// If process 1 tries then eventually it enters the critical section

p1=1 => P>=1 [ F p1=10 ]