Thoof proof

PAREN :: s/(?P<x>.*)/(\g<x>)/;  # A substitution axiom, which tells the computer a way to transform a string (in this case, put it in parentheses)
CARET :: s/^(?P<x>[^P].*)/^\g<x>/;  # Another substitution axiom, this one conditional
ST1 :: "walrus";  # A constant axiom- a string that exists by definition
ST2 :: "PLATYPUS";  # Another constant axiom
==;
--theo main;  # The main section, which has the body of the proof (not lemmas (subroutines))
-strs ST1 ST2;  # Set the working string to the ST1 and ST2 axioms (the only strings known to exist by definition). Because there's more than one string, all axioms will be applied to every string available.
aux;
CARET;  # Apply the CARET axiom again
PS; # Output the proof state- currently, the strings "^(^walrus)" and "^(PLATYPUS)".
--lemm aux;  # An extra theorem used to simplify (well, not in this case, but generally simplify) proving
CARET;  # Apply the CARET axiom to the current string (or, more accurately, to both strings)
PAREN;  # Apply the PAREN axiom