Thoof Axioms/Theorems for Peano Arithmetic

succ :: s/(?P<x>[SP]*0)/S\g<x>/;
pred :: s/(?P<x>[SP]*0/P\g<x>/;

RED_1 :: s/SP//;
RED_2 :: s/PS//;

appz :: s/(?P<x>[SP]*0)/\g<x>+0/;
incsnd :: s/(?P<x>[SP]*0)\+(?P<y>[SP]*0)/\g<x>+S\g<y>/;

ADD_ZER :: s/(?P<x>[SP]*0)\+0/\g<x>/;
ADD_1 :: s/(?P<x>[SP]*0)\+(?P<y>[SP]*0)/S\g<x>+P\g<y>/;

0 :: "0";

==;
--theo main;
-str 0;
succ;
succ;
succ;
appz;  # append +0
incsnd;  # Set the second argument to 1
incsnd;  # Set the second argument to 2
add;  # Set the output to 5
PS;  # Output the proof string("SSSSS0")

--lemm add;
@add';

--lemm add';
ADD_ZER;
ADD_1;
red_prim;

--lemm red_prim;
RED_1;
RED_2;