# EXAMPLE 5.16
y > 1 { begin x := 3; if x + y < 19 then x := x + 19 else x := y + y end } x > y  WHERE y > 1 && x = 3 IS B, x + y < 19 IS Q

# EXAMPLE 5.17
(x = 3 && y = 1) { while x > 0 do begin y := y + 3; x := x - 1 end } y = 10  WHERE (x = 3 && y = 1) IS P, (y = 10) IS Q

# EXAMPLE 5.18
divisor > 0 {begin begin rem := dividend; quot := 0 end; while rem >= divisor do begin rem := rem - divisor; quot := quot + 1 end end} dividend = rem + quot * divisor && rem < divisor           WHERE divisor > 0 IS P, dividend = rem + quot * divisor && rem < divisor IS Q, I1 IS I, rem >= divisor IS B

# another example:
x > 0 && x + y = z { begin x := x - 1; y := y + 1 end } x + y = z

# www.logic.at: bsp-07.pdf, 7.3.a
y > 0 { if x > y then z := x else begin z := y; y := y - 1 end } z > y

# www.logic.at: bsp-07.pdf, 7.3.b
x = 2 && y = 3 { while x != y do begin x := x + 1; y := y + 2 end } x = 1

# T1 can not be used in this example:
y = 5 && v = 3 { begin v := 5 + y; a := 7 end } a = 7