# Autoconverted from set.mm by xlat_mm.py and gen_set_mm.py param (PROP pax/prop () "") # set.mm - Version of 17-Oct-2006 # # PUBLIC DOMAIN # # This file (specifically, the version of this file with the above date) # has been released into the Public Domain per the Creative Commons Public # Domain Dedication. http://creativecommons.org/licenses/publicdomain/ # # Norman Megill - email: nm(at)alum(dot)mit(dot)edu # var (wff ph) var (wff ps) var (wff ch) var (wff th) var (wff ta) var (wff et) var (wff ze) kind (set) var (set x) var (set y) var (set z) var (set w) var (set v) var (set u) term (wff (A. set wff)) stmt (ax-4 () () (-> (A. x ph) ph)) stmt (ax-5 () () (-> (A. x (-> (A. x ph) ps)) (-> (A. x ph) (A. x ps)))) stmt (ax-6 () () (-> (-. (A. x (-. (A. x ph)))) ph)) stmt (ax-7 () () (-> (A. x (A. y ph)) (A. y (A. x ph)))) stmt (ax-gen () (ph) (A. x ph)) term (wff (E. set wff)) stmt (df-ex () () (<-> (E. x ph) (-. (A. x (-. ph))))) kind (class) term (class (cv set)) var (class A) var (class B) term (wff (= class class)) stmt (ax-8 () () (-> (= (cv x) (cv y)) (-> (= (cv x) (cv z)) (= (cv y) (cv z))))) stmt (ax-9 () () (-. (A. x (-. (= (cv x) (cv y)))))) stmt (ax-10 () () (-> (A. x (= (cv x) (cv y))) (-> (A. x ph) (A. y ph)))) stmt (ax-11 () () (-> (-. (A. x (= (cv x) (cv y)))) (-> (= (cv x) (cv y)) (-> ph (A. x (-> (= (cv x) (cv y)) ph)))))) stmt (ax-12 () () (-> (-. (A. z (= (cv z) (cv x)))) (-> (-. (A. z (= (cv z) (cv y)))) (-> (= (cv x) (cv y)) (A. z (= (cv x) (cv y))))))) term (wff (e. class class)) stmt (ax-13 () () (-> (= (cv x) (cv y)) (-> (e. (cv x) (cv z)) (e. (cv y) (cv z))))) stmt (ax-14 () () (-> (= (cv x) (cv y)) (-> (e. (cv z) (cv x)) (e. (cv z) (cv y))))) stmt (ax-15 () () (-> (-. (A. z (= (cv z) (cv x)))) (-> (-. (A. z (= (cv z) (cv y)))) (-> (e. (cv x) (cv y)) (A. z (e. (cv x) (cv y))))))) term (wff ([/] class set wff)) stmt (df-sb () () (<-> ([/] (cv y) x ph) (/\ (-> (= (cv x) (cv y)) ph) (E. x (/\ (= (cv x) (cv y)) ph))))) stmt (ax-16 ((x y)) () (-> (A. x (= (cv x) (cv y))) (-> ph (A. x ph)))) stmt (ax-17 ((ph x)) () (-> ph (A. x ph))) var (set f) var (set g) term (wff (E! set wff)) term (wff (E* set wff)) stmt (df-eu ((x y) (ph y)) () (<-> (E! x ph) (E. y (A. x (<-> ph (= (cv x) (cv y))))))) stmt (df-mo () () (<-> (E* x ph) (-> (E. x ph) (E! x ph)))) var (set t) stmt (ax-ext ((x y) (x z) (y z)) () (-> (A. z (<-> (e. (cv z) (cv x)) (e. (cv z) (cv y)))) (= (cv x) (cv y)))) term (class ({|} set wff)) var (class C) var (class D) var (class P) var (class Q) var (class R) var (class S) var (class T) var (class U) stmt (df-clab () () (<-> (e. (cv x) ({|} y ph)) ([/] (cv x) y ph))) stmt (df-cleq ((A x) (B x) (x y) (x z) (y z)) ((-> (A. x (<-> (e. (cv x) (cv y)) (e. (cv x) (cv z)))) (= (cv y) (cv z)))) (<-> (= A B) (A. x (<-> (e. (cv x) A) (e. (cv x) B))))) stmt (df-clel ((A x) (B x)) () (<-> (e. A B) (E. x (/\ (= (cv x) A) (e. (cv x) B))))) var (class F) var (class G) term (wff (=/= class class)) term (wff (e/ class class)) stmt (df-ne () () (<-> (=/= A B) (-. (= A B)))) stmt (df-nel () () (<-> (e/ A B) (-. (e. A B)))) term (wff (A.e. set class wff)) term (wff (E.e. set class wff)) term (wff (E!e. set class wff)) term (class ({e.|} set class wff)) stmt (df-ral () () (<-> (A.e. x A ph) (A. x (-> (e. (cv x) A) ph)))) stmt (df-rex () () (<-> (E.e. x A ph) (E. x (/\ (e. (cv x) A) ph)))) stmt (df-reu () () (<-> (E!e. x A ph) (E! x (/\ (e. (cv x) A) ph)))) stmt (df-rab () () (= ({e.|} x A ph) ({|} x (/\ (e. (cv x) A) ph)))) term (class (V)) stmt (df-v () () (= (V) ({|} x (= (cv x) (cv x))))) stmt (df-sbc () () (<-> ([/] A x ph) (e. A ({|} x ph)))) term (class ([_/]_ class set class)) stmt (df-csb ((A y) (B y) (x y)) () (= ([_/]_ A x B) ({|} y ([/] A x (e. (cv y) B))))) term (class (\ class class)) term (class (u. class class)) term (class (i^i class class)) term (wff (C_ class class)) term (wff (C: class class)) stmt (df-dif ((A x) (B x)) () (= (\ A B) ({|} x (/\ (e. (cv x) A) (-. (e. (cv x) B)))))) stmt (df-un ((A x) (B x)) () (= (u. A B) ({|} x (\/ (e. (cv x) A) (e. (cv x) B))))) stmt (df-in ((A x) (B x)) () (= (i^i A B) ({|} x (/\ (e. (cv x) A) (e. (cv x) B))))) stmt (df-ss () () (<-> (C_ A B) (= (i^i A B) A))) stmt (df-pss () () (<-> (C: A B) (/\ (C_ A B) (=/= A B)))) term (class ({/})) stmt (df-nul () () (= ({/}) (\ (V) (V)))) term (class (if wff class class)) stmt (df-if ((ph x) (A x) (B x)) () (= (if ph A B) ({|} x (\/ (/\ (e. (cv x) A) ph) (/\ (e. (cv x) B) (-. ph)))))) var (wff si) var (wff rh) term (class (P~ class)) stmt (df-pw ((A x)) () (= (P~ A) ({|} x (C_ (cv x) A)))) term (class ({} class)) term (class ({,} class class)) term (class (<,> class class)) stmt (df-sn ((A x)) () (= ({} A) ({|} x (= (cv x) A)))) stmt (df-pr () () (= ({,} A B) (u. ({} A) ({} B)))) term (class ({,,} class class class)) stmt (df-tp () () (= ({,,} A B C) (u. ({,} A B) ({} C)))) stmt (df-op () () (= (<,> A B) ({,} ({} A) ({,} A B)))) term (class (U. class)) stmt (df-uni ((x y) (A x) (A y)) () (= (U. A) ({|} x (E. y (/\ (e. (cv x) (cv y)) (e. (cv y) A)))))) term (class (|^| class)) stmt (df-int ((x y) (A x) (A y)) () (= (|^| A) ({|} x (A. y (-> (e. (cv y) A) (e. (cv x) (cv y))))))) term (class (U_ set class class)) term (class (|^|_ set class class)) stmt (df-iun ((x y) (A y) (B y)) () (= (U_ x A B) ({|} y (E.e. x A (e. (cv y) B))))) stmt (df-iin ((x y) (A y) (B y)) () (= (|^|_ x A B) ({|} y (A.e. x A (e. (cv y) B))))) term (wff (br class class class)) stmt (df-br () () (<-> (br A R B) (e. (<,> A B) R))) term (class ({<,>|} set set wff)) stmt (df-opab ((x z) (y z) (ph z)) () (= ({<,>|} x y ph) ({|} z (E. x (E. y (/\ (= (cv z) (<,> (cv x) (cv y))) ph)))))) term (wff (Tr class)) stmt (df-tr () () (<-> (Tr A) (C_ (U. A) A))) stmt (ax-rep ((x y) (x z) (w x) (y z) (w y) (w z)) () (-> (A. w (E. y (A. z (-> (A. y ph) (= (cv z) (cv y)))))) (E. y (A. z (<-> (e. (cv z) (cv y)) (E. w (/\ (e. (cv w) (cv x)) (A. y ph)))))))) stmt (ax-pow ((x y) (x z) (w x) (y z) (w y) (w z)) () (E. y (A. z (-> (A. w (-> (e. (cv w) (cv z)) (e. (cv w) (cv x)))) (e. (cv z) (cv y)))))) term (class (E)) term (class (I)) stmt (df-eprel ((x y)) () (= (E) ({<,>|} x y (e. (cv x) (cv y))))) stmt (df-id ((x y)) () (= (I) ({<,>|} x y (= (cv x) (cv y))))) term (wff (Po class class)) term (wff (Or class class)) stmt (df-po ((x y) (x z) (R x) (y z) (R y) (R z) (A x) (A y) (A z)) () (<-> (Po R A) (A.e. x A (A.e. y A (A.e. z A (/\ (-. (br (cv x) R (cv x))) (-> (/\ (br (cv x) R (cv y)) (br (cv y) R (cv z))) (br (cv x) R (cv z))))))))) stmt (df-so ((x y) (R x) (R y) (A x) (A y)) () (<-> (Or R A) (/\ (Po R A) (A.e. x A (A.e. y A (\/\/ (br (cv x) R (cv y)) (= (cv x) (cv y)) (br (cv y) R (cv x)))))))) stmt (ax-un ((w x) (w y) (w z) (x y) (x z) (y z)) () (E. y (A. z (-> (E. w (/\ (e. (cv z) (cv w)) (e. (cv w) (cv x)))) (e. (cv z) (cv y)))))) term (class (sup class class class)) stmt (df-sup ((x y) (x z) (R x) (y z) (R y) (R z) (A x) (A y) (A z) (B x) (B y) (B z)) () (= (sup B A R) (U. ({e.|} x A (/\ (A.e. y B (-. (br (cv x) R (cv y)))) (A.e. y A (-> (br (cv y) R (cv x)) (E.e. z B (br (cv y) R (cv z)))))))))) term (wff (Fr class class)) term (wff (We class class)) stmt (df-fr ((x y) (x z) (R x) (y z) (R y) (R z) (A x) (A y) (A z)) () (<-> (Fr R A) (A. x (-> (/\ (C_ (cv x) A) (-. (= (cv x) ({/})))) (E.e. y (cv x) (A.e. z (cv x) (-. (br (cv z) R (cv y))))))))) stmt (df-we () () (<-> (We R A) (/\ (Fr R A) (Or R A)))) term (wff (Ord class)) term (class (On)) term (wff (Lim class)) term (class (suc class)) stmt (df-ord () () (<-> (Ord A) (/\ (Tr A) (We (E) A)))) stmt (df-on () () (= (On) ({|} x (Ord (cv x))))) stmt (df-lim () () (<-> (Lim A) (/\/\ (Ord A) (-. (= A ({/}))) (= A (U. A))))) stmt (df-suc () () (= (suc A) (u. A ({} A)))) term (class (om)) stmt (df-om ((x y)) () (= (om) ({|} x (/\ (Ord (cv x)) (A. y (-> (Lim (cv y)) (e. (cv x) (cv y)))))))) var (set h) var (set j) var (set k) var (set m) var (set n) var (class H) var (class J) var (class K) var (class L) var (class M) var (class N) var (class W) var (class X) var (class Y) var (class Z) term (class (X. class class)) term (class (`' class)) term (class (dom class)) term (class (ran class)) term (class (|` class class)) term (class (" class class)) term (class (o. class class)) term (wff (Rel class)) term (wff (Fun class)) term (wff (Fn class class)) term (wff (:--> class class class)) term (wff (:-1-1-> class class class)) term (wff (:-onto-> class class class)) term (wff (:-1-1-onto-> class class class)) term (class (` class class)) term (wff (Isom class class class class class)) stmt (df-xp ((x y) (A x) (A y) (B x) (B y)) () (= (X. A B) ({<,>|} x y (/\ (e. (cv x) A) (e. (cv y) B))))) stmt (df-rel () () (<-> (Rel A) (C_ A (X. (V) (V))))) stmt (df-cnv ((x y) (A x) (A y)) () (= (`' A) ({<,>|} x y (br (cv y) A (cv x))))) stmt (df-co ((x y) (x z) (A x) (y z) (A y) (A z) (B x) (B y) (B z)) () (= (o. A B) ({<,>|} x y (E. z (/\ (br (cv x) B (cv z)) (br (cv z) A (cv y))))))) stmt (df-dm ((x y) (A x) (A y)) () (= (dom A) ({|} x (E. y (br (cv x) A (cv y)))))) stmt (df-rn () () (= (ran A) (dom (`' A)))) stmt (df-res () () (= (|` A B) (i^i A (X. B (V))))) stmt (df-ima () () (= (" A B) (ran (|` A B)))) stmt (df-fun () () (<-> (Fun A) (/\ (Rel A) (C_ (o. A (`' A)) (I))))) stmt (df-fn () () (<-> (Fn A B) (/\ (Fun A) (= (dom A) B)))) stmt (df-f () () (<-> (:--> F A B) (/\ (Fn F A) (C_ (ran F) B)))) stmt (df-f1 () () (<-> (:-1-1-> F A B) (/\ (:--> F A B) (Fun (`' F))))) stmt (df-fo () () (<-> (:-onto-> F A B) (/\ (Fn F A) (= (ran F) B)))) stmt (df-f1o () () (<-> (:-1-1-onto-> F A B) (/\ (:-1-1-> F A B) (:-onto-> F A B)))) stmt (df-fv ((A x) (F x)) () (= (` F A) (U. ({|} x (= (" F ({} A)) ({} (cv x))))))) stmt (df-iso ((x y) (A x) (A y) (B x) (B y) (R x) (R y) (S x) (S y) (H x) (H y)) () (<-> (Isom H R S A B) (/\ (:-1-1-onto-> H A B) (A.e. x A (A.e. y A (<-> (br (cv x) R (cv y)) (br (` H (cv x)) S (` H (cv y))))))))) term (class (rec class class)) stmt (df-rdg ((x y) (x z) (f x) (g x) (F x) (y z) (f y) (g y) (F y) (f z) (g z) (F z) (f g) (F f) (F g) (A x) (A y) (A z) (A f) (A g)) () (= (rec F A) (U. ({|} f (E.e. x (On) (/\ (Fn (cv f) (cv x)) (A.e. y (cv x) (= (` (cv f) (cv y)) (` ({<,>|} g z (= (cv z) (if (= (cv g) ({/})) A (if (Lim (dom (cv g))) (U. (ran (cv g))) (` F (` (cv g) (U. (dom (cv g))))))))) (|` (cv f) (cv y))))))))))) term (class (opr class class class)) term (class ({<<,>,>|} set set set wff)) stmt (df-opr () () (= (opr A F B) (` F (<,> A B)))) stmt (df-oprab ((w x) (w y) (w z) (ph w)) () (= ({<<,>,>|} x y z ph) ({|} w (E. x (E. y (E. z (/\ (= (cv w) (<,> (<,> (cv x) (cv y)) (cv z))) ph))))))) term (class (1st)) term (class (2nd)) stmt (df-1st ((x y)) () (= (1st) ({<,>|} x y (= (cv y) (U. (dom ({} (cv x)))))))) stmt (df-2nd ((x y)) () (= (2nd) ({<,>|} x y (= (cv y) (U. (ran ({} (cv x)))))))) term (class (1o)) term (class (2o)) term (class (+o)) term (class (.o)) term (class (^o)) stmt (df-1o () () (= (1o) (suc ({/})))) stmt (df-2o () () (= (2o) (suc (1o)))) stmt (df-oadd ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (= (+o) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (On)) (e. (cv y) (On))) (= (cv z) (` (rec ({<,>|} w v (= (cv v) (suc (cv w)))) (cv x)) (cv y))))))) stmt (df-omul ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (= (.o) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (On)) (e. (cv y) (On))) (= (cv z) (` (rec ({<,>|} w v (= (cv v) (opr (cv w) (+o) (cv x)))) ({/})) (cv y))))))) stmt (df-oexp ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (= (^o) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (On)) (e. (cv y) (On))) (= (cv z) (if (= (cv x) ({/})) (\ (1o) (cv y)) (` (rec ({<,>|} w v (= (cv v) (opr (cv w) (.o) (cv x)))) (1o)) (cv y)))))))) term (wff (Er class)) term (class ([] class class)) term (class (/. class class)) stmt (df-er () () (<-> (Er R) (C_ (u. (`' R) (o. R R)) R))) stmt (df-ec () () (= ([] A R) (" R ({} A)))) stmt (df-qs ((x y) (A x) (A y) (R x) (R y)) () (= (/. A R) ({|} y (E.e. x A (= (cv y) ([] (cv x) R)))))) var (set s) var (set r) var (set a) var (set b) var (set c) var (set d) term (class (^m)) stmt (df-map ((x y) (x z) (f x) (y z) (f y) (f z)) () (= (^m) ({<<,>,>|} x y z (= (cv z) ({|} f (:--> (cv f) (cv y) (cv x))))))) term (class (X_ set class class)) stmt (df-ixp ((f x) (A f) (B f)) () (= (X_ x A B) ({|} f (/\ (Fn (cv f) A) (A.e. x A (e. (` (cv f) (cv x)) B)))))) term (class (~~)) term (class (~<_)) term (class (~<)) stmt (df-en ((x y) (f x) (f y)) () (= (~~) ({<,>|} x y (E. f (:-1-1-onto-> (cv f) (cv x) (cv y)))))) stmt (df-dom ((x y) (f x) (f y)) () (= (~<_) ({<,>|} x y (E. f (:-1-1-> (cv f) (cv x) (cv y)))))) stmt (df-sdom () () (= (~<) (\ (~<_) (~~)))) stmt (ax-reg ((x y) (x z) (y z)) () (-> (E. y (e. (cv y) (cv x))) (E. y (/\ (e. (cv y) (cv x)) (A. z (-> (e. (cv z) (cv y)) (-. (e. (cv z) (cv x))))))))) stmt (ax-inf ((x y) (x z) (w x) (y z) (w y) (w z)) () (E. y (/\ (e. (cv x) (cv y)) (A. z (-> (e. (cv z) (cv y)) (E. w (/\ (e. (cv z) (cv w)) (e. (cv w) (cv y))))))))) term (class (R1)) term (class (rank)) stmt (df-r1 ((x y)) () (= (R1) (rec ({<,>|} x y (= (cv y) (P~ (cv x)))) ({/})))) stmt (df-rank ((x y) (x z) (y z)) () (= (rank) ({<,>|} x y (= (cv y) (|^| ({e.|} z (On) (e. (cv x) (` (R1) (suc (cv z)))))))))) stmt (ax-ac ((x y) (x z) (w x) (v x) (u x) (t x) (y z) (w y) (v y) (u y) (t y) (w z) (v z) (u z) (t z) (v w) (u w) (t w) (u v) (t v) (t u)) () (E. y (A. z (A. w (-> (/\ (e. (cv z) (cv w)) (e. (cv w) (cv x))) (E. v (A. u (<-> (E. t (/\ (/\ (e. (cv u) (cv w)) (e. (cv w) (cv t))) (/\ (e. (cv u) (cv t)) (e. (cv t) (cv y))))) (= (cv u) (cv v)))))))))) var (set q) term (class (card)) term (class (aleph)) term (class (cf)) stmt (df-card ((x y) (x z) (y z)) () (= (card) ({<,>|} x y (= (cv y) (|^| ({e.|} z (On) (br (cv z) (~~) (cv x)))))))) stmt (df-aleph ((x y) (x z) (y z)) () (= (aleph) (rec ({<,>|} x y (= (cv y) (|^| ({e.|} z (On) (br (cv x) (~<) (cv z)))))) (om)))) stmt (df-cf ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (cf) ({<,>|} x y (/\ (e. (cv x) (On)) (= (cv y) (|^| ({|} z (E. w (/\ (= (cv z) (` (card) (cv w))) (/\ (C_ (cv w) (cv x)) (A.e. v (cv x) (E.e. u (cv w) (C_ (cv v) (cv u)))))))))))))) term (class (+c)) stmt (df-cda ((x y) (x z) (y z)) () (= (+c) ({<<,>,>|} x y z (= (cv z) (u. (X. (cv x) ({} ({/}))) (X. (cv y) ({} (1o)))))))) stmt (ax-groth ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (E. y (/\/\ (e. (cv x) (cv y)) (A.e. z (cv y) (/\ (A. w (-> (C_ (cv w) (cv z)) (e. (cv w) (cv y)))) (E.e. w (cv y) (A. v (-> (C_ (cv v) (cv z)) (e. (cv v) (cv w))))))) (A. z (-> (C_ (cv z) (cv y)) (\/ (br (cv z) (~~) (cv y)) (e. (cv z) (cv y)))))))) term (class (N.)) term (class (+N)) term (class (.N)) term (class (,>|} x y z (/\ (/\ (e. (cv x) (X. (N.) (N.))) (e. (cv y) (X. (N.) (N.)))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (opr (cv w) (.N) (cv f)) (+N) (opr (cv v) (.N) (cv u))) (opr (cv v) (.N) (cv f))))))))))))) stmt (df-mpq ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (.pQ) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (X. (N.) (N.))) (e. (cv y) (X. (N.) (N.)))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (cv w) (.N) (cv u)) (opr (cv v) (.N) (cv f))))))))))))) stmt (df-enq ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (~Q) ({<,>|} x y (/\ (/\ (e. (cv x) (X. (N.) (N.))) (e. (cv y) (X. (N.) (N.)))) (E. z (E. w (E. v (E. u (/\ (/\ (= (cv x) (<,> (cv z) (cv w))) (= (cv y) (<,> (cv v) (cv u)))) (= (opr (cv z) (.N) (cv u)) (opr (cv w) (.N) (cv v)))))))))))) stmt (df-nq () () (= (Q.) (/. (X. (N.) (N.)) (~Q)))) stmt (df-plq ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (+Q) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (Q.)) (e. (cv y) (Q.))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) ([] (<,> (cv w) (cv v)) (~Q))) (= (cv y) ([] (<,> (cv u) (cv f)) (~Q)))) (= (cv z) ([] (opr (<,> (cv w) (cv v)) (+pQ) (<,> (cv u) (cv f))) (~Q)))))))))))) stmt (df-mq ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (.Q) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (Q.)) (e. (cv y) (Q.))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) ([] (<,> (cv w) (cv v)) (~Q))) (= (cv y) ([] (<,> (cv u) (cv f)) (~Q)))) (= (cv z) ([] (opr (<,> (cv w) (cv v)) (.pQ) (<,> (cv u) (cv f))) (~Q)))))))))))) stmt (df-rq ((x y)) () (= (*Q) ({<,>|} x y (/\ (e. (cv x) (Q.)) (= (opr (cv x) (.Q) (cv y)) (1Q)))))) stmt (df-ltq ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (|} x y (/\ (/\ (e. (cv x) (Q.)) (e. (cv y) (Q.))) (E. z (E. w (E. v (E. u (/\ (/\ (= (cv x) ([] (<,> (cv z) (cv w)) (~Q))) (= (cv y) ([] (<,> (cv v) (cv u)) (~Q)))) (br (opr (cv z) (.N) (cv u)) ( (1o) (1o)) (~Q)))) stmt (df-np ((x y) (x z) (y z)) () (= (P.) ({|} x (/\ (/\ (C: ({/}) (cv x)) (C: (cv x) (Q.))) (A.e. y (cv x) (/\ (A. z (-> (br (cv z) (,>|} x y z (/\ (/\ (e. (cv x) (P.)) (e. (cv y) (P.))) (= (cv z) ({|} w (E.e. v (cv x) (E.e. u (cv y) (= (cv w) (opr (cv v) (+Q) (cv u))))))))))) stmt (df-mp ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (.P.) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (P.)) (e. (cv y) (P.))) (= (cv z) ({|} w (E.e. v (cv x) (E.e. u (cv y) (= (cv w) (opr (cv v) (.Q) (cv u))))))))))) stmt (df-ltp ((x y)) () (= (|} x y (/\ (/\ (e. (cv x) (P.)) (e. (cv y) (P.))) (C: (cv x) (cv y)))))) stmt (df-plpr ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (+pR) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (X. (P.) (P.))) (e. (cv y) (X. (P.) (P.)))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (cv w) (+P.) (cv u)) (opr (cv v) (+P.) (cv f))))))))))))) stmt (df-mpr ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (.pR) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (X. (P.) (P.))) (e. (cv y) (X. (P.) (P.)))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (opr (cv w) (.P.) (cv u)) (+P.) (opr (cv v) (.P.) (cv f))) (opr (opr (cv w) (.P.) (cv f)) (+P.) (opr (cv v) (.P.) (cv u)))))))))))))) stmt (df-enr ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (~R) ({<,>|} x y (/\ (/\ (e. (cv x) (X. (P.) (P.))) (e. (cv y) (X. (P.) (P.)))) (E. z (E. w (E. v (E. u (/\ (/\ (= (cv x) (<,> (cv z) (cv w))) (= (cv y) (<,> (cv v) (cv u)))) (= (opr (cv z) (+P.) (cv u)) (opr (cv w) (+P.) (cv v)))))))))))) stmt (df-nr () () (= (R.) (/. (X. (P.) (P.)) (~R)))) stmt (df-plr ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (+R) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (R.)) (e. (cv y) (R.))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) ([] (<,> (cv w) (cv v)) (~R))) (= (cv y) ([] (<,> (cv u) (cv f)) (~R)))) (= (cv z) ([] (opr (<,> (cv w) (cv v)) (+pR) (<,> (cv u) (cv f))) (~R)))))))))))) stmt (df-mr ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (.R) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (R.)) (e. (cv y) (R.))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) ([] (<,> (cv w) (cv v)) (~R))) (= (cv y) ([] (<,> (cv u) (cv f)) (~R)))) (= (cv z) ([] (opr (<,> (cv w) (cv v)) (.pR) (<,> (cv u) (cv f))) (~R)))))))))))) stmt (df-ltr ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (|} x y (/\ (/\ (e. (cv x) (R.)) (e. (cv y) (R.))) (E. z (E. w (E. v (E. u (/\ (/\ (= (cv x) ([] (<,> (cv z) (cv w)) (~R))) (= (cv y) ([] (<,> (cv v) (cv u)) (~R)))) (br (opr (cv z) (+P.) (cv u)) ( (1P) (1P)) (~R)))) stmt (df-1r () () (= (1R) ([] (<,> (opr (1P) (+P.) (1P)) (1P)) (~R)))) stmt (df-m1r () () (= (-1R) ([] (<,> (1P) (opr (1P) (+P.) (1P))) (~R)))) term (class (CC)) term (class (RR)) term (class (0)) term (class (1)) term (class (i)) term (class (+)) term (class ( (0R) (0R)))) stmt (df-1 () () (= (1) (<,> (1R) (0R)))) stmt (df-i () () (= (i) (<,> (0R) (1R)))) stmt (df-r () () (= (RR) (X. (R.) ({} (0R))))) stmt (df-plus ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (+) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (CC)) (e. (cv y) (CC))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (cv w) (+R) (cv u)) (opr (cv v) (+R) (cv f))))))))))))) stmt (df-mul ((x y) (x z) (w x) (v x) (u x) (f x) (y z) (w y) (v y) (u y) (f y) (w z) (v z) (u z) (f z) (v w) (u w) (f w) (u v) (f v) (f u)) () (= (x.) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (CC)) (e. (cv y) (CC))) (E. w (E. v (E. u (E. f (/\ (/\ (= (cv x) (<,> (cv w) (cv v))) (= (cv y) (<,> (cv u) (cv f)))) (= (cv z) (<,> (opr (opr (cv w) (.R) (cv u)) (+R) (opr (-1R) (.R) (opr (cv v) (.R) (cv f)))) (opr (opr (cv v) (.R) (cv u)) (+R) (opr (cv w) (.R) (cv f)))))))))))))) stmt (df-lt ((x y) (x z) (w x) (y z) (w y) (w z)) () (= (|} x y (/\ (/\ (e. (cv x) (RR)) (e. (cv y) (RR))) (E. z (E. w (/\ (/\ (= (cv x) (<,> (cv z) (0R))) (= (cv y) (<,> (cv w) (0R)))) (br (cv z) (,>|} x y z (/\ (/\ (e. (cv x) (CC)) (e. (cv y) (CC))) (= (cv z) (U. ({e.|} w (CC) (= (opr (cv y) (+) (cv w)) (cv x))))))))) stmt (df-neg () () (= (-u A) (opr (0) (-) A))) stmt (df-div ((x y) (x z) (w x) (y z) (w y) (w z)) () (= (/) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (CC)) (e. (cv y) (\ (CC) ({} (0))))) (= (cv z) (U. ({e.|} w (CC) (= (opr (cv y) (x.) (cv w)) (cv x))))))))) term (class (+oo)) term (class (-oo)) term (class (RR*)) term (class (<)) stmt (df-pnf () () (= (+oo) (CC))) stmt (df-mnf () () (= (-oo) ({} (CC)))) stmt (df-xr () () (= (RR*) (u. (RR) ({,} (+oo) (-oo))))) stmt (df-ltxr () () (= (<) (u. (u. (i^i ( (-oo) (+oo)))) (u. (X. (RR) ({} (+oo))) (X. ({} (-oo)) (RR)))))) stmt (df-le () () (= (<_) (\ (X. (RR*) (RR*)) (`' (<))))) stmt (df-n ((x y)) () (= (NN) (|^| ({|} x (/\ (e. (1) (cv x)) (A.e. y (cv x) (e. (opr (cv y) (+) (1)) (cv x)))))))) term (class (2)) term (class (3)) term (class (4)) term (class (5)) term (class (6)) term (class (7)) term (class (8)) term (class (9)) stmt (df-2 () () (= (2) (opr (1) (+) (1)))) stmt (df-3 () () (= (3) (opr (2) (+) (1)))) stmt (df-4 () () (= (4) (opr (3) (+) (1)))) stmt (df-5 () () (= (5) (opr (4) (+) (1)))) stmt (df-6 () () (= (6) (opr (5) (+) (1)))) stmt (df-7 () () (= (7) (opr (6) (+) (1)))) stmt (df-8 () () (= (8) (opr (7) (+) (1)))) stmt (df-9 () () (= (9) (opr (8) (+) (1)))) stmt (df-n0 () () (= (NN0) (u. (NN) ({} (0))))) stmt (df-z () () (= (ZZ) ({e.|} n (RR) (\/\/ (= (cv n) (0)) (e. (cv n) (NN)) (e. (-u (cv n)) (NN)))))) term (class (floor)) stmt (df-fl ((x y) (x z) (y z)) () (= (floor) ({<,>|} x y (/\ (e. (cv x) (RR)) (= (cv y) (U. ({e.|} z (ZZ) (/\ (br (cv z) (<_) (cv x)) (br (cv x) (<) (opr (cv z) (+) (1))))))))))) stmt (df-q ((m n) (m x) (n x)) () (= (QQ) ({|} x (E.e. m (ZZ) (E.e. n (NN) (= (cv x) (opr (cv m) (/) (cv n)))))))) term (class (seq1)) stmt (df-seq1 ((x y) (x z) (w x) (f x) (g x) (h x) (y z) (w y) (f y) (g y) (h y) (w z) (f z) (g z) (h z) (f w) (g w) (h w) (f g) (f h) (g h)) () (= (seq1) ({<<,>,>|} f g h (= (cv h) ({<,>|} x y (/\ (e. (cv x) (NN)) (= (cv y) (` (2nd) (` (o. (rec ({<,>|} z w (= (cv w) (<,> (opr (` (1st) (cv z)) (+) (1)) (opr (` (2nd) (cv z)) (cv f) (` (cv g) (opr (` (1st) (cv z)) (+) (1))))))) (<,> (1) (` (cv g) (1)))) (`' (|` (rec ({<,>|} z w (= (cv w) (opr (cv z) (+) (1)))) (1)) (om)))) (cv x)))))))))) term (class (shift)) stmt (df-shft ((x y) (x z) (f x) (g x) (y z) (f y) (g y) (f z) (g z) (f g)) () (= (shift) ({<<,>,>|} f x g (= (cv g) ({<,>|} y z (/\ (e. (cv y) (CC)) (= (cv z) (` (cv f) (opr (cv y) (-) (cv x)))))))))) term (class (ZZ>)) stmt (df-uz ((j k) (j y) (k y)) () (= (ZZ>) ({<,>|} j y (/\ (e. (cv j) (ZZ)) (= (cv y) ({e.|} k (ZZ) (br (cv j) (<_) (cv k)))))))) term (class (...)) stmt (df-fz ((m n) (k m) (m z) (k n) (n z) (k z)) () (= (...) ({<<,>,>|} m n z (/\ (/\ (e. (cv m) (ZZ)) (e. (cv n) (ZZ))) (= (cv z) ({e.|} k (ZZ) (/\ (br (cv m) (<_) (cv k)) (br (cv k) (<_) (cv n))))))))) term (class (limsup)) stmt (df-limsup ((k x) (k y) (k z) (x y) (x z) (y z)) () (= (limsup) ({<,>|} x y (= (cv y) (sup ({|} z (E.e. k (ZZ) (= (cv z) (sup (i^i (" (cv x) (` (ZZ>) (cv k))) (RR*)) (RR*) (<))))) (RR*) (`' (<))))))) term (class (seq)) term (class (seq0)) stmt (df-seqz ((g h) (g k) (g x) (h k) (h x) (k x)) () (= (seq) ({<<,>,>|} x g h (= (cv h) (|` (opr (opr (` (2nd) (cv x)) (seq1) (opr (cv g) (shift) (opr (1) (-) (` (1st) (cv x))))) (shift) (opr (` (1st) (cv x)) (-) (1))) ({e.|} k (ZZ) (br (` (1st) (cv x)) (<_) (cv k)))))))) stmt (df-seq0 ((f g) (f h) (g h)) () (= (seq0) ({<<,>,>|} f g h (= (cv h) (|` (opr (opr (cv f) (seq1) (opr (cv g) (shift) (1))) (shift) (-u (1))) (NN0)))))) term (class (^)) stmt (df-exp ((x y) (x z) (y z)) () (= (^) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (CC)) (e. (cv y) (NN0))) (= (cv z) (if (= (cv y) (0)) (1) (` (opr (x.) (seq1) (X. (NN) ({} (cv x)))) (cv y)))))))) term (class (sqr)) stmt (df-sqr ((x y) (x z) (y z)) () (= (sqr) ({<,>|} x y (/\ (/\ (e. (cv x) (RR)) (br (0) (<_) (cv x))) (= (cv y) (sup ({e.|} z (RR) (/\ (br (0) (<_) (cv z)) (br (opr (cv z) (x.) (cv z)) (<_) (cv x)))) (RR) (<))))))) term (class (Re)) term (class (Im)) term (class (*)) term (class (abs)) stmt (df-re ((x y) (x z) (w x) (y z) (w y) (w z)) () (= (Re) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (U. ({e.|} z (RR) (E.e. w (RR) (= (cv x) (opr (cv z) (+) (opr (cv w) (x.) (i)))))))))))) stmt (df-im ((x y) (x z) (w x) (y z) (w y) (w z)) () (= (Im) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (U. ({e.|} w (RR) (E.e. z (RR) (= (cv x) (opr (cv z) (+) (opr (cv w) (x.) (i)))))))))))) stmt (df-cj ((x y)) () (= (*) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (opr (` (Re) (cv x)) (-) (opr (` (Im) (cv x)) (x.) (i)))))))) stmt (df-abs ((x y)) () (= (abs) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (` (sqr) (opr (cv x) (x.) (` (*) (cv x))))))))) term (class (!)) stmt (df-fac () () (= (!) (u. (opr (x.) (seq1) (|` (I) (NN))) ({} (<,> (0) (1)))))) term (class (C.)) stmt (df-bc ((k n) (m n) (k m)) () (= (C.) ({<<,>,>|} n k m (/\ (/\ (e. (cv n) (NN0)) (e. (cv k) (ZZ))) (= (cv m) (if (/\ (br (0) (<_) (cv k)) (br (cv k) (<_) (cv n))) (opr (` (!) (cv n)) (/) (opr (` (!) (opr (cv n) (-) (cv k))) (x.) (` (!) (cv k)))) (0))))))) term (class (~~>)) stmt (df-clim ((j k) (j x) (j y) (f j) (k x) (k y) (f k) (x y) (f x) (f y)) () (= (~~>) ({<,>|} f y (/\ (e. (cv y) (CC)) (A.e. x (RR) (-> (br (0) (<) (cv x)) (E.e. j (ZZ) (A.e. k (ZZ) (-> (br (cv j) (<_) (cv k)) (/\ (e. (` (cv f) (cv k)) (CC)) (br (` (abs) (opr (` (cv f) (cv k)) (-) (cv y))) (<) (cv x)))))))))))) term (class (sum_ set class class)) stmt (df-sum ((k m) (k n) (k x) (k y) (m n) (m x) (m y) (n x) (n y) (x y) (A m) (A n) (A x) (A y) (B m) (B n) (B x) (B y)) () (= (sum_ k A B) (u. ({|} x (E. m (E.e. n (` (ZZ>) (cv m)) (/\ (= A (opr (cv m) (...) (cv n))) (e. (cv x) (` (opr (<,> (cv m) (+)) (seq) (|` ({<,>|} k y (= (cv y) B)) (ZZ))) (cv n))))))) (U. ({|} x (E.e. m (ZZ) (/\ (= A (` (ZZ>) (cv m))) (br (opr (<,> (cv m) (+)) (seq) (|` ({<,>|} k y (= (cv y) B)) (ZZ))) (~~>) (cv x))))))))) term (class (exp)) term (class (e)) term (class (sin)) term (class (cos)) term (class (pi)) stmt (df-ef ((k x) (k y) (x y)) () (= (exp) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (sum_ k (NN0) (opr (opr (cv x) (^) (cv k)) (/) (` (!) (cv k))))))))) stmt (df-e () () (= (e) (` (exp) (1)))) stmt (df-sin ((x y)) () (= (sin) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (opr (opr (` (exp) (opr (i) (x.) (cv x))) (-) (` (exp) (opr (-u (i)) (x.) (cv x)))) (/) (opr (2) (x.) (i)))))))) stmt (df-cos ((x y)) () (= (cos) ({<,>|} x y (/\ (e. (cv x) (CC)) (= (cv y) (opr (opr (` (exp) (opr (i) (x.) (cv x))) (+) (` (exp) (opr (-u (i)) (x.) (cv x)))) (/) (2))))))) stmt (df-pi () () (= (pi) (sup ({e.|} x (RR) (/\ (br (0) (<) (cv x)) (= (` (sin) (cv x)) (0)))) (RR) (`' (<))))) term (class (Top)) term (class (TopSp)) term (class (Bases)) term (class (topGen)) stmt (df-top ((x y) (x z) (y z)) () (= (Top) ({|} x (/\ (A. y (-> (C_ (cv y) (cv x)) (e. (U. (cv y)) (cv x)))) (A.e. y (cv x) (A.e. z (cv x) (e. (i^i (cv y) (cv z)) (cv x)))))))) stmt (df-topsp ((x y)) () (= (TopSp) ({<,>|} x y (/\ (e. (cv y) (Top)) (= (cv x) (U. (cv y))))))) stmt (df-bases ((x y) (x z) (y z)) () (= (Bases) ({|} x (A.e. y (cv x) (A.e. z (cv x) (C_ (i^i (cv y) (cv z)) (U. (i^i (cv x) (P~ (i^i (cv y) (cv z))))))))))) stmt (df-topgen ((x y) (x z) (y z)) () (= (topGen) ({<,>|} x y (/\ (e. (cv x) (Bases)) (= (cv y) ({|} z (C_ (cv z) (U. (i^i (cv x) (P~ (cv z))))))))))) term (class (Cls)) term (class (int)) term (class (cls)) stmt (df-clsd ((w x) (w z) (x z)) () (= (Cls) ({<,>|} z w (/\ (e. (cv z) (Top)) (= (cv w) ({|} x (/\ (C_ (cv x) (U. (cv z))) (e. (\ (U. (cv z)) (cv x)) (cv z))))))))) stmt (df-ntr ((v w) (v x) (v y) (v z) (w x) (w y) (w z) (x y) (x z) (y z)) () (= (int) ({<,>|} z w (/\ (e. (cv z) (Top)) (= (cv w) ({<,>|} x y (/\ (C_ (cv x) (U. (cv z))) (= (cv y) (U. ({e.|} v (cv z) (C_ (cv v) (cv x)))))))))))) stmt (df-cls ((v w) (v x) (v y) (v z) (w x) (w y) (w z) (x y) (x z) (y z)) () (= (cls) ({<,>|} z w (/\ (e. (cv z) (Top)) (= (cv w) ({<,>|} x y (/\ (C_ (cv x) (U. (cv z))) (= (cv y) (|^| ({e.|} v (` (Cls) (cv z)) (C_ (cv x) (cv v)))))))))))) term (class (nei)) stmt (df-nei ((j y) (j w) (j z) (g j) (w y) (y z) (g y) (w z) (g w) (g z)) () (= (nei) ({<,>|} j y (/\ (e. (cv j) (Top)) (= (cv y) ({<,>|} w z (/\ (C_ (cv w) (U. (cv j))) (E.e. g (cv j) (/\ (C_ (cv z) (cv g)) (C_ (cv g) (cv w))))))))))) term (class (Cn)) term (class (CnP)) stmt (df-cn ((f j) (f k) (f y) (f z) (j k) (j y) (j z) (k y) (k z) (y z)) () (= (Cn) ({<<,>,>|} j k z (/\ (/\ (e. (cv j) (Top)) (e. (cv k) (Top))) (= (cv z) ({e.|} f (opr (U. (cv k)) (^m) (U. (cv j))) (A.e. y (cv k) (e. (" (`' (cv f)) (cv y)) (cv j))))))))) stmt (df-cnp ((f j) (f k) (f v) (f w) (f x) (f y) (f z) (j k) (j v) (j w) (j x) (j y) (j z) (k v) (k w) (k x) (k y) (k z) (v w) (v x) (v y) (v z) (w x) (w y) (w z) (x y) (x z) (y z)) () (= (CnP) ({<<,>,>|} j k z (/\ (/\ (e. (cv j) (Top)) (e. (cv k) (Top))) (= (cv z) ({<,>|} x y (/\ (e. (cv x) (U. (cv j))) (= (cv y) ({e.|} f (opr (U. (cv k)) (^m) (U. (cv j))) (A.e. w (cv k) (-> (e. (` (cv f) (cv x)) (cv w)) (E.e. v (cv j) (/\ (e. (cv x) (cv v)) (C_ (" (cv f) (cv v)) (cv w))))))))))))))) term (class (Met)) term (class (ball)) term (class (open)) stmt (df-ms ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (= (Met) ({<,>|} x y (/\ (:--> (cv y) (X. (cv x) (cv x)) (RR)) (A.e. z (cv x) (A.e. w (cv x) (/\ (<-> (= (opr (cv z) (cv y) (cv w)) (0)) (= (cv z) (cv w))) (A.e. v (cv x) (br (opr (cv z) (cv y) (cv w)) (<_) (opr (opr (cv v) (cv y) (cv z)) (+) (opr (cv v) (cv y) (cv w)))))))))))) stmt (df-bl ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (ball) ({<,>|} x y (/\ (e. (cv x) (Met)) (= (cv y) ({<<,>,>|} z w v (/\ (/\ (e. (cv z) (` (1st) (cv x))) (e. (cv w) (RR))) (/\ (br (0) (<) (cv w)) (= (cv v) ({e.|} u (` (1st) (cv x)) (br (opr (cv z) (` (2nd) (cv x)) (cv u)) (<) (cv w)))))))))))) stmt (df-opn ((x y) (x z) (w x) (v x) (y z) (w y) (v y) (w z) (v z) (v w)) () (= (open) ({<,>|} x y (/\ (e. (cv x) (Met)) (= (cv y) ({|} z (/\ (C_ (cv z) (` (1st) (cv x))) (A.e. w (cv z) (E.e. v (ran (` (ball) (cv x))) (/\ (e. (cv w) (cv v)) (C_ (cv v) (cv z)))))))))))) term (class (~~>m)) term (class (cau)) term (class (Cm)) stmt (df-lm ((j k) (j x) (j y) (f j) (j z) (j w) (k x) (k y) (f k) (k z) (k w) (x y) (f x) (x z) (w x) (f y) (y z) (w y) (f z) (f w) (w z)) () (= (~~>m) ({<,>|} z w (/\ (e. (cv z) (Met)) (= (cv w) ({<,>|} f y (/\/\ (C_ (cv f) (X. (CC) (` (1st) (cv z)))) (e. (cv y) (` (1st) (cv z))) (A.e. x (RR) (-> (br (0) (<) (cv x)) (E.e. j (ZZ) (A.e. k (ZZ) (-> (br (cv j) (<_) (cv k)) (/\ (e. (` (cv f) (cv k)) (` (1st) (cv z))) (br (opr (` (cv f) (cv k)) (` (2nd) (cv z)) (cv y)) (<) (cv x))))))))))))))) stmt (df-cau ((j k) (j m) (j x) (f j) (j z) (j w) (k m) (k x) (f k) (k z) (k w) (m x) (f m) (m z) (m w) (f x) (x z) (w x) (f z) (f w) (w z)) () (= (cau) ({<,>|} z w (/\ (e. (cv z) (Met)) (= (cv w) ({|} f (/\ (C_ (cv f) (X. (CC) (` (1st) (cv z)))) (A.e. x (RR) (-> (br (0) (<) (cv x)) (E.e. j (ZZ) (A.e. k (ZZ) (A.e. m (ZZ) (-> (/\ (br (cv j) (<_) (cv k)) (br (cv j) (<_) (cv m))) (/\/\ (e. (` (cv f) (cv k)) (` (1st) (cv z))) (e. (` (cv f) (cv m)) (` (1st) (cv z))) (br (opr (` (cv f) (cv k)) (` (2nd) (cv z)) (` (cv f) (cv m))) (<) (cv x)))))))))))))))) stmt (df-cms ((x y) (f x) (f y)) () (= (Cm) ({e.|} x (Met) (A.e. f (` (cau) (cv x)) (E.e. y (` (1st) (cv x)) (br (cv f) (` (~~>m) (cv x)) (cv y))))))) term (class (Grp)) term (class (Id)) stmt (df-grp ((g t) (g u) (g x) (g y) (g z) (t u) (t x) (t y) (t z) (u x) (u y) (u z) (x y) (x z) (y z)) () (= (Grp) ({|} g (E. t (/\ (= (cv t) (dom (dom (cv g)))) (/\/\ (:--> (cv g) (X. (cv t) (cv t)) (cv t)) (A.e. x (cv t) (A.e. y (cv t) (A.e. z (cv t) (= (opr (opr (cv x) (cv g) (cv y)) (cv g) (cv z)) (opr (cv x) (cv g) (opr (cv y) (cv g) (cv z))))))) (E.e. u (cv t) (A.e. x (cv t) (/\ (= (opr (cv u) (cv g) (cv x)) (cv x)) (E.e. y (cv t) (= (opr (cv y) (cv g) (cv x)) (cv u)))))))))))) stmt (df-gid ((g u) (g x) (g y) (u x) (u y) (x y)) () (= (Id) ({<,>|} g y (/\ (e. (cv g) (Grp)) (= (cv y) (U. ({e.|} u (dom (dom (cv g))) (A.e. x (dom (dom (cv g))) (= (opr (cv u) (cv g) (cv x)) (cv x)))))))))) term (class (H~)) term (class (+v)) term (class (.s)) term (class (0v)) term (class (-v)) term (class (.i)) term (class (norm)) term (class (Cauchy)) term (class (~~>v)) term (class (SH)) term (class (CH)) term (class (_|_)) term (class (+H)) term (class (span)) term (class (vH)) term (class (\/H)) term (class (0H)) term (class (C_H)) term (class (proj)) term (class (+op)) term (class (.op)) term (class (-op)) term (class (+fn)) term (class (.fn)) term (class (0op)) term (class (Iop)) term (class (normop)) term (class (ConOp)) term (class (LinOp)) term (class (BndLinOp)) term (class (UniOp)) term (class (HrmOp)) term (class (normfn)) term (class (null)) term (class (ConFn)) term (class (LinFn)) term (class (adj)) term (class (bra)) term (class (ketbra)) term (class (<_op)) term (class (eigvec)) term (class (eigval)) term (class (Lambda)) term (class (States)) term (class (CHStates)) term (class (Atoms)) term (class ( (/\ (e. A (H~)) (e. B (H~))) (e. (opr A (+v) B) (H~)))) stmt (ax-hvcom () () (-> (/\ (e. A (H~)) (e. B (H~))) (= (opr A (+v) B) (opr B (+v) A)))) stmt (ax-hvass () () (-> (/\/\ (e. A (H~)) (e. B (H~)) (e. C (H~))) (= (opr (opr A (+v) B) (+v) C) (opr A (+v) (opr B (+v) C))))) stmt (ax-hv0cl () () (e. (0v) (H~))) stmt (ax-hvaddid () () (-> (e. A (H~)) (= (opr A (+v) (0v)) A))) stmt (ax-hvmulcl () () (-> (/\ (e. A (CC)) (e. B (H~))) (e. (opr A (.s) B) (H~)))) stmt (ax-hvmulid () () (-> (e. A (H~)) (= (opr (1) (.s) A) A))) stmt (ax-hvmulass () () (-> (/\/\ (e. A (CC)) (e. B (CC)) (e. C (H~))) (= (opr (opr A (x.) B) (.s) C) (opr A (.s) (opr B (.s) C))))) stmt (ax-hvdistr1 () () (-> (/\/\ (e. A (CC)) (e. B (H~)) (e. C (H~))) (= (opr A (.s) (opr B (+v) C)) (opr (opr A (.s) B) (+v) (opr A (.s) C))))) stmt (ax-hvdistr2 () () (-> (/\/\ (e. A (CC)) (e. B (CC)) (e. C (H~))) (= (opr (opr A (+) B) (.s) C) (opr (opr A (.s) C) (+v) (opr B (.s) C))))) stmt (ax-hvmul0 () () (-> (e. A (H~)) (= (opr (0) (.s) A) (0v)))) stmt (df-hvsub ((x y) (x z) (y z)) () (= (-v) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (H~)) (e. (cv y) (H~))) (= (cv z) (opr (cv x) (+v) (opr (-u (1)) (.s) (cv y)))))))) stmt (ax-hicl () () (-> (/\ (e. A (H~)) (e. B (H~))) (e. (opr A (.i) B) (CC)))) stmt (ax-his1 () () (-> (/\ (e. A (H~)) (e. B (H~))) (= (opr A (.i) B) (` (*) (opr B (.i) A))))) stmt (ax-his2 () () (-> (/\/\ (e. A (H~)) (e. B (H~)) (e. C (H~))) (= (opr (opr A (+v) B) (.i) C) (opr (opr A (.i) C) (+) (opr B (.i) C))))) stmt (ax-his3 () () (-> (/\/\ (e. A (CC)) (e. B (H~)) (e. C (H~))) (= (opr (opr A (.s) B) (.i) C) (opr A (x.) (opr B (.i) C))))) stmt (ax-his4 () () (-> (/\ (e. A (H~)) (=/= A (0v))) (br (0) (<) (opr A (.i) A)))) stmt (df-hnorm ((x y)) () (= (norm) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (` (sqr) (opr (cv x) (.i) (cv x)))))))) stmt (df-hcau ((x y) (x z) (w x) (f x) (y z) (w y) (f y) (w z) (f z) (f w)) () (= (Cauchy) ({|} f (/\ (:--> (cv f) (NN) (H~)) (A.e. x (RR) (-> (br (0) (<) (cv x)) (E.e. y (NN) (A.e. z (NN) (A.e. w (NN) (-> (/\ (br (cv y) (<_) (cv z)) (br (cv y) (<_) (cv w))) (br (` (norm) (opr (` (cv f) (cv z)) (-v) (` (cv f) (cv w)))) (<) (cv x)))))))))))) stmt (df-hlim ((x y) (x z) (f x) (w x) (y z) (f y) (w y) (f z) (w z) (f w)) () (= (~~>v) ({<,>|} f w (/\ (/\ (:--> (cv f) (NN) (H~)) (e. (cv w) (H~))) (A.e. x (RR) (-> (br (0) (<) (cv x)) (E.e. y (NN) (A.e. z (NN) (-> (br (cv y) (<_) (cv z)) (br (` (norm) (opr (` (cv f) (cv z)) (-v) (cv w))) (<) (cv x))))))))))) stmt (ax-hcompl ((F x)) () (-> (e. F (Cauchy)) (E.e. x (H~) (br F (~~>v) (cv x))))) stmt (df-sh ((x y) (h x) (h y)) () (= (SH) ({|} h (/\ (/\ (C_ (cv h) (H~)) (e. (0v) (cv h))) (/\ (A.e. x (cv h) (A.e. y (cv h) (e. (opr (cv x) (+v) (cv y)) (cv h)))) (A.e. x (CC) (A.e. y (cv h) (e. (opr (cv x) (.s) (cv y)) (cv h))))))))) stmt (df-ch ((f x) (h x) (f h)) () (= (CH) ({|} h (/\ (e. (cv h) (SH)) (A. f (A. x (-> (/\ (:--> (cv f) (NN) (cv h)) (br (cv f) (~~>v) (cv x))) (e. (cv x) (cv h))))))))) stmt (df-oc ((x y) (x z) (w x) (y z) (w y) (w z)) () (= (_|_) ({<,>|} x y (/\ (C_ (cv x) (H~)) (= (cv y) ({e.|} z (H~) (A.e. w (cv x) (= (opr (cv z) (.i) (cv w)) (0))))))))) stmt (df-ch0 () () (= (0H) ({} (0v)))) stmt (df-pj ((f h) (h x) (h y) (h z) (h w) (f x) (f y) (f z) (f w) (x y) (x z) (w x) (y z) (w y) (w z)) () (= (proj) ({<,>|} h f (/\ (e. (cv h) (CH)) (= (cv f) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (U. ({e.|} z (cv h) (E.e. w (` (_|_) (cv h)) (= (cv x) (opr (cv z) (+v) (cv w)))))))))))))) stmt (df-shsum ((x y) (x z) (w x) (v x) (u x) (y z) (w y) (v y) (u y) (w z) (v z) (u z) (v w) (u w) (u v)) () (= (+H) ({<<,>,>|} x y z (/\ (/\ (e. (cv x) (SH)) (e. (cv y) (SH))) (= (cv z) ({e.|} w (H~) (E.e. v (cv x) (E.e. u (cv y) (= (cv w) (opr (cv v) (+v) (cv u))))))))))) stmt (df-span ((x y) (x z) (y z)) () (= (span) ({<,>|} x y (/\ (C_ (cv x) (H~)) (= (cv y) (|^| ({e.|} z (SH) (C_ (cv x) (cv z))))))))) stmt (df-chj ((x y) (x z) (y z)) () (= (vH) ({<<,>,>|} x y z (/\ (/\ (C_ (cv x) (H~)) (C_ (cv y) (H~))) (= (cv z) (` (_|_) (` (_|_) (u. (cv x) (cv y))))))))) stmt (df-chsup ((x y)) () (= (\/H) ({<,>|} x y (/\ (C_ (cv x) (P~ (H~))) (= (cv y) (` (_|_) (` (_|_) (U. (cv x))))))))) stmt (df-hosum ((f g) (f h) (f x) (f y) (g h) (g x) (g y) (h x) (h y) (x y)) () (= (+op) ({<<,>,>|} f g h (/\ (/\ (:--> (cv f) (H~) (H~)) (:--> (cv g) (H~) (H~))) (= (cv h) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (opr (` (cv f) (cv x)) (+v) (` (cv g) (cv x))))))))))) stmt (df-homul ((f g) (f h) (f x) (f y) (g h) (g x) (g y) (h x) (h y) (x y)) () (= (.op) ({<<,>,>|} f g h (/\ (/\ (e. (cv f) (CC)) (:--> (cv g) (H~) (H~))) (= (cv h) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (opr (cv f) (.s) (` (cv g) (cv x))))))))))) stmt (df-hodif ((f g) (f h) (f x) (f y) (g h) (g x) (g y) (h x) (h y) (x y)) () (= (-op) ({<<,>,>|} f g h (/\ (/\ (:--> (cv f) (H~) (H~)) (:--> (cv g) (H~) (H~))) (= (cv h) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (opr (` (cv f) (cv x)) (-v) (` (cv g) (cv x))))))))))) stmt (df-hfsum ((f g) (f h) (f x) (f y) (g h) (g x) (g y) (h x) (h y) (x y)) () (= (+fn) ({<<,>,>|} f g h (/\ (/\ (:--> (cv f) (H~) (CC)) (:--> (cv g) (H~) (CC))) (= (cv h) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (opr (` (cv f) (cv x)) (+) (` (cv g) (cv x))))))))))) stmt (df-hfmul ((f g) (f h) (f x) (f y) (g h) (g x) (g y) (h x) (h y) (x y)) () (= (.fn) ({<<,>,>|} f g h (/\ (/\ (e. (cv f) (CC)) (:--> (cv g) (H~) (CC))) (= (cv h) ({<,>|} x y (/\ (e. (cv x) (H~)) (= (cv y) (opr (cv f) (x.) (` (cv g) (cv x))))))))))) stmt (df-cm ((x y)) () (= (C_H) ({<,>|} x y (/\ (/\ (e. (cv x) (CH)) (e. (cv y) (CH))) (= (cv x) (opr (i^i (cv x) (cv y)) (vH) (i^i (cv x) (` (_|_) (cv y))))))))) stmt (df-0op () () (= (0op) (` (proj) (0H)))) stmt (df-iop () () (= (Iop) (` (proj) (H~)))) stmt (df-nmop ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (normop) ({<,>|} t y (/\ (:--> (cv t) (H~) (H~)) (= (cv y) (sup ({|} x (E.e. z (H~) (/\ (br (` (norm) (cv z)) (<_) (1)) (= (cv x) (` (norm) (` (cv t) (cv z))))))) (RR*) (<))))))) stmt (df-cnop ((t w) (t x) (t y) (t z) (w x) (w y) (w z) (x y) (x z) (y z)) () (= (ConOp) ({|} t (/\ (:--> (cv t) (H~) (H~)) (A.e. x (H~) (A.e. y (RR) (-> (br (0) (<) (cv y)) (E.e. z (RR) (/\ (br (0) (<) (cv z)) (A.e. w (H~) (-> (br (` (norm) (opr (cv w) (-v) (cv x))) (<) (cv z)) (br (` (norm) (opr (` (cv t) (cv w)) (-v) (` (cv t) (cv x)))) (<) (cv y))))))))))))) stmt (df-lnop ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (LinOp) ({|} t (/\ (:--> (cv t) (H~) (H~)) (A.e. x (CC) (A.e. y (H~) (A.e. z (H~) (= (` (cv t) (opr (opr (cv x) (.s) (cv y)) (+v) (cv z))) (opr (opr (cv x) (.s) (` (cv t) (cv y))) (+v) (` (cv t) (cv z))))))))))) stmt (df-bdop () () (= (BndLinOp) (i^i (LinOp) ({|} t (/\ (:--> (cv t) (H~) (H~)) (br (` (normop) (cv t)) (<) (+oo))))))) stmt (df-unop ((t x) (t y) (x y)) () (= (UniOp) ({|} t (/\ (:-onto-> (cv t) (H~) (H~)) (A.e. x (H~) (A.e. y (H~) (= (opr (` (cv t) (cv x)) (.i) (` (cv t) (cv y))) (opr (cv x) (.i) (cv y))))))))) stmt (df-hmop ((t x) (t y) (x y)) () (= (HrmOp) ({|} t (/\ (:--> (cv t) (H~) (H~)) (A.e. x (H~) (A.e. y (H~) (= (opr (cv x) (.i) (` (cv t) (cv y))) (opr (` (cv t) (cv x)) (.i) (cv y))))))))) stmt (df-nmfn ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (normfn) ({<,>|} t y (/\ (:--> (cv t) (H~) (CC)) (= (cv y) (sup ({|} x (E.e. z (H~) (/\ (br (` (norm) (cv z)) (<_) (1)) (= (cv x) (` (abs) (` (cv t) (cv z))))))) (RR*) (<))))))) stmt (df-nlfn ((t x) (t y) (x y)) () (= (null) ({<,>|} t y (/\ (:--> (cv t) (H~) (CC)) (= (cv y) ({e.|} x (H~) (= (` (cv t) (cv x)) (0)))))))) stmt (df-cnfn ((t w) (t x) (t y) (t z) (w x) (w y) (w z) (x y) (x z) (y z)) () (= (ConFn) ({|} t (/\ (:--> (cv t) (H~) (CC)) (A.e. x (H~) (A.e. y (RR) (-> (br (0) (<) (cv y)) (E.e. z (RR) (/\ (br (0) (<) (cv z)) (A.e. w (H~) (-> (br (` (norm) (opr (cv w) (-v) (cv x))) (<) (cv z)) (br (` (abs) (opr (` (cv t) (cv w)) (-) (` (cv t) (cv x)))) (<) (cv y))))))))))))) stmt (df-lnfn ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (LinFn) ({|} t (/\ (:--> (cv t) (H~) (CC)) (A.e. x (CC) (A.e. y (H~) (A.e. z (H~) (= (` (cv t) (opr (opr (cv x) (.s) (cv y)) (+v) (cv z))) (opr (opr (cv x) (x.) (` (cv t) (cv y))) (+) (` (cv t) (cv z))))))))))) stmt (df-adj ((t u) (t x) (t y) (u x) (u y) (x y)) () (= (adj) ({<,>|} t u (/\/\ (:--> (cv t) (H~) (H~)) (:--> (cv u) (H~) (H~)) (A.e. x (H~) (A.e. y (H~) (= (opr (` (cv t) (cv x)) (.i) (cv y)) (opr (cv x) (.i) (` (cv u) (cv y)))))))))) stmt (df-bra ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (bra) ({<,>|} x t (/\ (e. (cv x) (H~)) (= (cv t) ({<,>|} y z (/\ (e. (cv y) (H~)) (= (cv z) (opr (cv y) (.i) (cv x)))))))))) stmt (df-kb ((t v) (t w) (t x) (t y) (v w) (v x) (v y) (w x) (w y) (x y)) () (= (ketbra) ({<<,>,>|} x y t (/\ (/\ (e. (cv x) (H~)) (e. (cv y) (H~))) (= (cv t) ({<,>|} w v (/\ (e. (cv w) (H~)) (= (cv v) (opr (opr (cv w) (.i) (cv y)) (.s) (cv x)))))))))) stmt (df-leop ((t u) (t x) (u x)) () (= (<_op) ({<,>|} t u (/\ (e. (opr (cv u) (-op) (cv t)) (HrmOp)) (A.e. x (H~) (br (0) (<_) (opr (` (opr (cv u) (-op) (cv t)) (cv x)) (.i) (cv x)))))))) stmt (df-eigvec ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (eigvec) ({<,>|} t y (/\ (:--> (cv t) (H~) (H~)) (= (cv y) ({e.|} x (H~) (/\ (=/= (cv x) (0v)) (E.e. z (CC) (= (` (cv t) (cv x)) (opr (cv z) (.s) (cv x))))))))))) stmt (df-eigval ((t x) (t y) (t z) (x y) (x z) (y z)) () (= (eigval) ({<,>|} t y (/\ (:--> (cv t) (H~) (H~)) (= (cv y) ({<,>|} x z (/\ (e. (cv x) (` (eigvec) (cv t))) (= (cv z) (opr (opr (` (cv t) (cv x)) (.i) (cv x)) (/) (opr (` (norm) (cv x)) (^) (2))))))))))) stmt (df-spec ((t x) (t y) (x y)) () (= (Lambda) ({<,>|} t y (/\ (:--> (cv t) (H~) (H~)) (= (cv y) ({e.|} x (CC) (-. (:-1-1-> (opr (cv t) (-op) (opr (cv x) (.op) (|` (I) (H~)))) (H~) (H~))))))))) stmt (df-st ((f x) (f y) (x y)) () (= (States) ({|} f (/\ (/\ (:--> (cv f) (CH) (RR)) (A.e. x (CH) (/\ (br (0) (<_) (` (cv f) (cv x))) (br (` (cv f) (cv x)) (<_) (1))))) (/\ (= (` (cv f) (H~)) (1)) (A.e. x (CH) (A.e. y (CH) (-> (C_ (cv x) (` (_|_) (cv y))) (= (` (cv f) (opr (cv x) (vH) (cv y))) (opr (` (cv f) (cv x)) (+) (` (cv f) (cv y)))))))))))) stmt (df-hst ((f x) (f y) (x y)) () (= (CHStates) ({|} f (/\/\ (:--> (cv f) (CH) (H~)) (= (` (norm) (` (cv f) (H~))) (1)) (A.e. x (CH) (A.e. y (CH) (-> (C_ (cv x) (` (_|_) (cv y))) (/\ (= (opr (` (cv f) (cv x)) (.i) (` (cv f) (cv y))) (0)) (= (` (cv f) (opr (cv x) (vH) (cv y))) (opr (` (cv f) (cv x)) (+v) (` (cv f) (cv y)))))))))))) stmt (df-cv ((x y) (x z) (y z)) () (= (|} x y (/\ (/\ (e. (cv x) (CH)) (e. (cv y) (CH))) (/\ (C: (cv x) (cv y)) (-. (E.e. z (CH) (/\ (C: (cv x) (cv z)) (C: (cv z) (cv y)))))))))) stmt (df-md ((x y) (x z) (y z)) () (= (MH) ({<,>|} x y (/\ (/\ (e. (cv x) (CH)) (e. (cv y) (CH))) (A.e. z (CH) (-> (C_ (cv z) (cv y)) (= (i^i (opr (cv z) (vH) (cv x)) (cv y)) (opr (cv z) (vH) (i^i (cv x) (cv y)))))))))) stmt (df-dmd ((x y) (x z) (y z)) () (= (MH*) ({<,>|} x y (/\ (/\ (e. (cv x) (CH)) (e. (cv y) (CH))) (A.e. z (CH) (-> (C_ (cv y) (cv z)) (= (opr (i^i (cv z) (cv x)) (vH) (cv y)) (i^i (cv z) (opr (cv x) (vH) (cv y)))))))))) stmt (df-at () () (= (Atoms) ({e.|} x (CH) (br (0H) (