Checking Landau's "Grundlagen" in the Automath System

2-expressions abstraction expressions ALGOL 60 andi Appendix applied AUT-QE text AUT-SYNT AUTOMATH languages AUTOMATH project axioms chapter chapter chapter Church-Rosser theorem complex numbers concepts constant context correct expressions defined definitional equality definitionally equal denotes double negation law E-formulas EB-lines example extensional equality folgt formal formulas free variables function-like identifier IMP(A,B indexed induction interpretation introduced irrelevance of proofs ISBN 90 Kapitel Landau Landau's book language theory LASTELT lemmas mathematics n-reduction natural deduction natural numbers natürliche natürlichen Zahlen NOT(A NOT(B paragraph lines partial functions Peano's axioms PL Y,Z PN E type PN PN PN-lines predicate primitive notions proof of Satz PROP PROP PROP1 properties proposition proved real number reduces rule Satz 27 SIGMA SIGMA,P simultaneous substitution strong normalization substitution successor SYMIS synt syntactic variables theorems tion transitive closure translation verification verifying program x,S]PROP Zahl Zandleven