&<>~!%^*()-+=|\/{}.:;"' , ? -- /- -/ " " axiom definition inductive structure theorem