(fmod PNAT is sorts PNat PNzNat PZero . subsorts PZero PNzNat < PNat . op 0 : -> PZero [ctor] . op s_ : PNat -> PNzNat [ctor]. op _+_ : PNat PNat -> PNat [prec 30]. vars M N : PNat . --- eq 0 + N = N . eq s M + N = s(M + N) . --- op _*_ : PNat PNat -> PNat [prec 29]. eq 0 * N = 0 . eq s M * N = N + (M * N) . endfm) --- ------------------------------------------------------------ --- ------------------------------------------------------------ ---> lemma1+ (goal PNAT |- eq M:PNat + 0 = M:PNat ;) (set ind on M:PNat .) (apply SI TC RD .) ---> lemma2+ (goal PNAT |- eq M:PNat + s N:PNat = s(M:PNat + N:PNat) ;) (set ind on M:PNat .) (apply SI TC RD .) --- ------------------------------------------------------------ --- ------------------------------------------------------------ (fth PNAT+ is inc PNAT . ---> pr PNAT vars M N : PNat . --- eq N + 0 = N . eq N + s M = s(N + M) . endfth) --- ------------------------------------------------------------ --- ------------------------------------------------------------ ---> comm+ (goal PNAT+ |- eq M:PNat + N:PNat = N:PNat + M:PNat ;) (set ind on M:PNat .) (apply SI TC RD .) ---> assoc+ (goal PNAT+ |- eq (M:PNat + N:PNat) + P:PNat = M:PNat + (N:PNat + P:PNat) ;) (set ind on M:PNat .) (apply SI TC RD .) --- ------------------------------------------------------------ --- ------------------------------------------------------------ (fmod PNAT+ is sorts PNat PNzNat PZero . subsorts PZero PNzNat < PNat . op 0 : -> PZero [ctor] . op s_ : PNat -> PNzNat [ctor]. op _+_ : PNat PNat -> PNat [assoc comm prec 30]. vars M N : PNat . --- eq 0 + N = N . eq s M + N = s(M + N) . --- op _*_ : PNat PNat -> PNat [prec 29]. eq 0 * N = 0 . eq s M * N = N + (M * N) . endfm) --- ------------------------------------------------------------ --- ------------------------------------------------------------ ---> lemma1* (goal PNAT+ |- eq M:PNat * 0 = 0 ;) --- --- 1. Prove lemma1*. --- ---> lemma2* (goal PNAT+ |- eq M:PNat * s N:PNat = M:PNat + (M:PNat * N:PNat) ;) --- --- 2. Prove lemma2*. --- --- ------------------------------------------------------------ --- ------------------------------------------------------------ (fth PNAT+* is inc PNAT+ . ---> pr PNAT vars M N : PNat . --- eq N * 0 = 0 . eq N * s M = N + N * M . endfth) --- ------------------------------------------------------------ --- ------------------------------------------------------------ ---> comm* --- --- 3. Prove comm*. --- ---> distributivity (goal PNAT+* |- eq M:PNat * (N:PNat + P:PNat) = M:PNat * N:PNat + M:PNat * P:PNat ;) --- --- 4. Prove distributivity (left). --- (goal PNAT+* |- eq (M:PNat + N:PNat) * P:PNat = M:PNat * P:PNat + N:PNat * P:PNat ;) --- --- 5. Prove distributivity (right). --- --- ------------------------------------------------------------ --- ------------------------------------------------------------ (fth PNAT+* is inc PNAT+ . vars M N P : PNat . eq N * 0 = 0 . eq N * s M = N + N * M . eq (M + N) * P = M * P + N * P . endfth) --- ------------------------------------------------------------ --- ------------------------------------------------------------ ---> assoc* --- --- 6. Prove assoc*. ---