311_destruct.mlw 186 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
use list.List
use list.Length
use int.Int

constant x: int

predicate p int

axiom H: not (p 0)
axiom H1: p 0

goal g: false

axiom H2: false

goal g5: p 5

axiom H3: true

goal g6: p 5