// theorem 1 (mutual exclusion)

(!((p1>9) & (p2>9))) &
(!((p1>9) & (p3>9))) &
(!((p1>9) & (p4>9))) &
(!((p1>9) & (p5>9))) &
(!((p1>9) & (p6>9))) &
(!((p1>9) & (p7>9))) &
(!((p1>9) & (p8>9))) &
(!((p1>9) & (p9>9))) &
(!((p1>9) & (p10>9))) &
(!((p2>9) & (p3>9))) &
(!((p2>9) & (p4>9))) &
(!((p2>9) & (p5>9))) &
(!((p2>9) & (p6>9))) &
(!((p2>9) & (p7>9))) &
(!((p2>9) & (p8>9))) &
(!((p2>9) & (p9>9))) &
(!((p2>9) & (p10>9))) &
(!((p3>9) & (p4>9))) &
(!((p3>9) & (p5>9))) &
(!((p3>9) & (p6>9))) &
(!((p3>9) & (p7>9))) &
(!((p3>9) & (p8>9))) &
(!((p3>9) & (p9>9))) &
(!((p3>9) & (p10>9))) &
(!((p4>9) & (p5>9))) &
(!((p4>9) & (p6>9))) &
(!((p4>9) & (p7>9))) &
(!((p4>9) & (p8>9))) &
(!((p4>9) & (p9>9))) &
(!((p4>9) & (p10>9))) &
(!((p5>9) & (p6>9))) &
(!((p5>9) & (p7>9))) &
(!((p5>9) & (p8>9))) &
(!((p5>9) & (p9>9))) &
(!((p5>9) & (p10>9))) &
(!((p6>9) & (p7>9))) &
(!((p6>9) & (p8>9))) &
(!((p6>9) & (p9>9))) &
(!((p6>9) & (p10>9))) &
(!((p7>9) & (p8>9))) &
(!((p7>9) & (p9>9))) &
(!((p7>9) & (p10>9))) &
(!((p8>9) & (p9>9))) &
(!((p8>9) & (p10>9))) &
(!((p9>9) & (p10>9)))

// lemma c
// if the crical section is occupied then eventually it becomes clear

(p1>9) | (p2>9) | (p3>9) | (p4>9) | (p5>9) | (p6>9) | (p7>9) | (p8>9) | (p9>9) | (p10>9) =>
P>=1 [ true U (p1<10) & (p2<10) & (p3<10) & (p4<10) & (p5<10) & (p6<10) & (p7<10) & (p8<10) & (p9<10) & (p10<10) ]

// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14

((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) | ((p4>3) & (p4<14)) | ((p5>3) & (p5<14)) | ((p6>3) & (p6<14)) | ((p7>3) & (p7<14)) | ((p8>3) & (p8<14)) | ((p9>3) & (p9<14)) | ((p10>3) & (p10<14)) =>
P>=1 [ true U (p1=14) | (p2=14) | (p3=14) | (p4=14) | (p5=14) | (p6=14) | (p7=14) | (p8=14) | (p9=14) | (p10=14) ]

// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section

(p1=1) => P>=1 [ true U (p1=10) ]

// not probability 1

P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]