terminals s
syntax
n ::= 0
| s n
judgment gt: n > n
------- gt-one
s n > n
n1 > n2
--------- gt-more
s n1 > n2
lemma all-gt-zero:
forall n
exists s n > 0 .
_: s n > 0 by induction on n:
case 0 is
_: s 0 > 0 by rule gt-one
end case
case s n1 is
g: s n1 > 0 by induction hypothesis on n1
_: s s n1 > 0 by rule gt-more on g
end case
end induction
end lemma
theorem gt-implies-gt-succ:
forall g: n1 > n2
exists s n1 > s n2 .
_: s n1 > s n2 by induction on g:
case rule
------------ gt-one
_: s n2 > n2
is
_: s s n2 > s n2 by rule gt-one
end case
case rule
g1: n11 > n2
------------- gt-more
_: s n11 > n2
is
g2: s n11 > s n2 by induction hypothesis on g1
_: s s n11 > s n2 by rule gt-more on g2
end case
end induction
end theorem