Landau, Grundlagen der Analysis, Simple Type Theory Version, A Few Details

_AMONE (Automatic Translation)

Types Shown: LAMBDA z^3(OZZ) LAMBDA z^4(OZ) FORALL x(Z) . z^3 x x IMPLIES FORALL x^28(Z) . z^3 x^28 x^28 IMPLIES . z^4 x IMPLIES .z^4 x^28 IMPLIES z^3 x x^28

Types Omitted: LAMBDA z^3 LAMBDA z^4 FORALL x . z^3 x x IMPLIES FORALL x^28 . z^3 x^28 x^28 IMPLIES .z^4 x IMPLIES .z^4 x^28 IMPLIES z^3 x x^28

_E_ONE (Automatic Translation)

Types Shown: LAMBDA z^3(OZZ) LAMBDA z^4(OZ) . _AMONE(O(OZ)(OZZ)) z^3 z^4 AND EXISTS x(Z) .z^3 x x AND z^4 x

Types Omitted: LAMBDA z^3 LAMBDA z^4 ._AMONE z^3 z^4 AND EXISTS x .z^3 x x AND z^4 x

_ONEAX (Automatic Translation)

Types Shown: LAMBDA DUMMY(Z) FORALL x(OZZ) . PER(O(OZZ)) x IMPLIES FORALL x(OZ) . _E_ONE(O(OZ)(OZZ)) x(OZZ) x(OZ) IMPLIES x .IOTA .LAMBDA x(Z) . x(OZZ) x(Z) x AND x(OZ) x(Z)

Types Omitted: LAMBDA DUMMY FORALL x . PER x IMPLIES FORALL x . _E_ONE x x IMPLIES x .IOTA .LAMBDA x . x x x AND x x

_FISI (Automatic Translation)

Types Shown: LAMBDA DUMMY(YZ) FORALL x(OZZ) . PER(O(OZZ)) x IMPLIES FORALL x(OYY) . PER(O(OYY)) x IMPLIES FORALL x(YZ) . FORALL x(Z) FORALL y(Z) [ x(OZZ) x(Z) y IMPLIES x(OYY) [x(YZ) x(Z)] .x(YZ) y] IMPLIES FORALL x^1(YZ) . FORALL x(Z) FORALL y [ x(OZZ) x(Z) y IMPLIES x(OYY) [x^1 x(Z)] .x^1 y] IMPLIES . FORALL x [ x(OZZ) x(Z) x IMPLIES x(OYY) [x(YZ) x(Z)] . x^1 x] IMPLIES FORALL x FORALL y . x(OZZ) x(Z) y IMPLIES x(OYY) [ x(YZ) x(Z)] . x^1 y

Types Omitted: LAMBDA DUMMY FORALL x . PER x IMPLIES FORALL x . PER x IMPLIES FORALL x . FORALL x FORALL y [x x y IMPLIES x [x x] .x y] IMPLIES FORALL x^1 . FORALL x FORALL y [ x x y IMPLIES x [x^1 x] .x^1 y] IMPLIES . FORALL x [ x x x IMPLIES x [x x] . x^1 x] IMPLIES FORALL x FORALL y . x x y IMPLIES x [x x] . x^1 y

_FISI_THM (Theorem)

Types Shown: _FISI(O(YZ)) DUMMY(YZ)

Types Omitted: _FISI DUMMY

_NAT (Hand-Coded Translation)

=(OII)

_N_IN (Automatic Translation)

Types Shown: [_ESTI(O(OI)I(OII)) =]

Types Omitted: [_ESTI =]

_N_SOME (Automatic Translation)

Types Shown: LAMBDA q(OI) EXISTS x(I) q x

Types Omitted: LAMBDA q EXISTS x q x

_N_ALL (Automatic Translation)

Types Shown: LAMBDA q(OI) FORALL x(I) q x

Types Omitted: LAMBDA q FORALL x q x

_N_ONE (Automatic Translation)

Types Shown: [_E_ONE(O(OI)(OII)) =]

Types Omitted: [_E_ONE =]

_AX2 (Automatic Translation)

Types Shown: FORALL x(I) FORALL x^0(I) .x = x^0 IMPLIES _SUC x = _SUC x^0

Types Omitted: FORALL x FORALL x^0 .x = x^0 IMPLIES _SUC x = _SUC x^0

_AX2_THM (Theorem)

Types Shown: _AX2(O)

Types Omitted: _AX2

_AX3 (Automatic Translation)

Types Shown: FORALL x(I) .~._SUC x = _1

Types Omitted: FORALL x .~._SUC x = _1

_AX4 (Automatic Translation)

Types Shown: FORALL x(I) FORALL x^1(I) ._SUC x = _SUC x^1 IMPLIES x = x^1

Types Omitted: FORALL x FORALL x^1 ._SUC x = _SUC x^1 IMPLIES x = x^1

_COND1 (Automatic Translation)

Types Shown: _N_IN(O(OI)I) _1

Types Omitted: _N_IN _1

_COND2 (Automatic Translation)

Types Shown: LAMBDA z^2(OI) _N_ALL(O(OI)) .LAMBDA z^5(I) . _N_IN(O(OI)I) z^5 z^2 IMPLIES _N_IN [_SUC z^5] z^2

Types Omitted: LAMBDA z^2 _N_ALL .LAMBDA z^5 ._N_IN z^5 z^2 IMPLIES _N_IN [_SUC z^5] z^2

_AX5 (Automatic Translation)

Types Shown: FORALL x(OI) . _COND1(O(OI)) x IMPLIES . _COND2(O(OI)) x IMPLIES FORALL x(I) _N_IN(O(OI)I) x x(OI)

Types Omitted: FORALL x ._COND1 x IMPLIES ._COND2 x IMPLIES FORALL x _N_IN x x

_I1_T1 (Automatic Translation)

Types Shown: FORALL x(OI) . x _1 IMPLIES . FORALL x(I) [x(OI) x(I) IMPLIES x(OI) ._SUC x(I)] IMPLIES FORALL x _COND1(O(OI)) .[_SETOF(OI(OI)(OII)) =] x(OI)

Types Omitted: FORALL x . x _1 IMPLIES . FORALL x [x x IMPLIES x ._SUC x] IMPLIES FORALL x _COND1 .[_SETOF =] x

_I1_T1_THM (Theorem)

Types Shown: _I1_T1(O)

Types Omitted: _I1_T1

_I1_T2 (Automatic Translation)

Types Shown: FORALL x(OI) . x _1 IMPLIES . FORALL x(I) [x(OI) x(I) IMPLIES x(OI) ._SUC x(I)] IMPLIES FORALL x FORALL x . _N_IN(O(OI)I) x [[_SETOF(OI(OI)(OII)) =] x(OI)] IMPLIES x x(I)

Types Omitted: FORALL x . x _1 IMPLIES . FORALL x [x x IMPLIES x ._SUC x] IMPLIES FORALL x FORALL x . _N_IN x [[_SETOF =] x] IMPLIES x x

_I1_T2_THM (Theorem)

Types Shown: _I1_T2(O)

Types Omitted: _I1_T2

_I1_T3 (Automatic Translation)

Types Shown: FORALL x(OI) . x _1 IMPLIES . FORALL x(I) [x(OI) x(I) IMPLIES x(OI) ._SUC x(I)] IMPLIES FORALL x FORALL x . _N_IN(O(OI)I) x [[_SETOF(OI(OI)(OII)) =] x(OI)] IMPLIES _N_IN [_SUC x(I)] .[_SETOF =] x(OI)

Types Omitted: FORALL x . x _1 IMPLIES . FORALL x [x x IMPLIES x ._SUC x] IMPLIES FORALL x FORALL x . _N_IN x [[_SETOF =] x] IMPLIES _N_IN [_SUC x] .[ _SETOF =] x

_I1_T3_THM (Theorem)

Types Shown: _I1_T3(O)

Types Omitted: _I1_T3

_I1_T4 (Automatic Translation)

Types Shown: FORALL x(OI) . x _1 IMPLIES . FORALL x(I) [x(OI) x(I) IMPLIES x(OI) ._SUC x(I)] IMPLIES FORALL x _N_IN(O(OI)I) x .[_SETOF(OI(OI)(OII)) =] x(OI)

Types Omitted: FORALL x . x _1 IMPLIES . FORALL x [x x IMPLIES x ._SUC x] IMPLIES FORALL x _N_IN x .[_SETOF =] x

_I1_T4_THM (Theorem)

Types Shown: _I1_T4(O)

Types Omitted: _I1_T4

_I1_T4_HTHM (Theorem with Relevant Previous Results in Antecedent)

Types Shown: _I1_T3(O) AND _I1_T1(O) IMPLIES _I1_T4(O)

Types Omitted: _I1_T3 AND _I1_T1 IMPLIES _I1_T4

_INDUCTION (Automatic Translation)

Types Shown: FORALL x(OI) . x _1 IMPLIES . FORALL x(I) [ x(OI) x(I) IMPLIES x(OI) ._SUC x(I)] IMPLIES FORALL x .x = x IMPLIES x(OI) x(I)

Types Omitted: FORALL x . x _1 IMPLIES . FORALL x [x x IMPLIES x ._SUC x] IMPLIES FORALL x .x = x IMPLIES x x

_INDUCTION_THM (Theorem)

Types Shown: _INDUCTION(O)

Types Omitted: _INDUCTION

_INDUCTION_ATHM (Theorem with Axioms)

Types Shown: _AX5(O) IMPLIES _INDUCTION(O)

Types Omitted: _AX5 IMPLIES _INDUCTION