Twelf proof that addition commutes.

commutes.elf

% http://twelf.org/wiki/Proving_metatheorems:Summary:_the_natural_numbers

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.

plus-z : plus z N N.
plus-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.

%worlds () (plus _ _ _).
%total N (plus N _ _).

plus-id : {N:nat} plus N z N -> type.
%mode plus-id +N -D.

plus-id-z : plus-id z plus-z.
plus-id-s : plus-id (s N) (plus-s D) <- plus-id N D.

%worlds () (plus-id _ _).
%total N (plus-id N _).

plus-flip : plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode plus-flip +D1 -D2.

plus-flip-z : plus-flip _ plus-z.
plus-flip-s : plus-flip (plus-s D1) (plus-s D2)
                <- plus-flip D1 D2.

%worlds () (plus-flip _ _).
%total D (plus-flip D _).

plus-commutes : plus N1 N2 N3 -> plus N2 N1 N3 -> type.
%mode plus-commutes +D1 -D2.

plus-commutes-z : plus-commutes plus-z D <- plus-id _ D.
plus-commutes-s : plus-commutes (plus-s D1) D3
                    <- plus-commutes D1 D2
                    <- plus-flip D2 D3.

%worlds () (plus-commutes _ _).
%total D (plus-commutes D _).