in nat-add.maude
fmod NAT-ADD-IND-PROOF is extending NAT-ADD .
op t' : -> Nat . --- generic constant for induction
eq t' + 0 = t' . --- induction hypothesis
endfm
--- Induction proof of NAT-ADD |- T + 0 = T.
--- Base case: T is 0. Prove |- 0 + 0 = 0 .
--- Holds if 0 + 0 and 0 have the same normal form,
--- which can be tested by 0 + 0 == 0 in Maude:
red 0 + 0 == 0 .
--- Induction step. T is s(t'):
red s(t') + 0 == s(t') .
fmod NAT-ASS-IND-PROOF is extending NAT-ADD .
ops t1 t2 t3 : -> Nat .
eq (t1 + t2) + t3 = t1 + (t2 + t3) .
endfm
red (0 + t2) + t3 == 0 + (t2 + t3) .
red (s(t1) + t2) + t3 == s(t1) + (t2 + t3) .