:: ORDINAL5 semantic presentation begin theorem :: ORDINAL5:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")))) "or" (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")))) ")" )) ; registration cluster (Set ($#k4_ordinal1 :::"NAT"::: ) ) -> ($#v4_ordinal1 :::"limit_ordinal"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"T-Sequence":::); let "g" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"T-Sequence":::); cluster (Set "f" ($#k1_ordinal4 :::"^"::: ) "g") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "g" ($#k1_ordinal4 :::"^"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ORDINAL5:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "b"))))) "holds" (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "S2")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ; theorem :: ORDINAL5:3 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "S1")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "S2")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S2"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "S1")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "S2")) ")" ))) ")" )) ; theorem :: ORDINAL5:4 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "S2"))) "is" ($#v1_ordinal2 :::"Ordinal-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Var "S1")) "is" ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ) & (Bool (Set (Var "S2")) "is" ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ) ")" )) ; definitionlet "f" be ($#m1_hidden :::"T-Sequence":::); attr "f" is :::"decreasing"::: means :: ORDINAL5:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); attr "f" is :::"non-decreasing"::: means :: ORDINAL5:def 2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))); attr "f" is :::"non-increasing"::: means :: ORDINAL5:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"decreasing"::: ORDINAL5:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_ordinal5 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )); :: deftheorem defines :::"non-decreasing"::: ORDINAL5:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_ordinal5 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) ")" )); :: deftheorem defines :::"non-increasing"::: ORDINAL5:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_ordinal5 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ($#v2_ordinal2 :::"increasing"::: ) -> ($#v2_ordinal5 :::"non-decreasing"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ($#v1_ordinal5 :::"decreasing"::: ) -> ($#v3_ordinal5 :::"non-increasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ORDINAL5:5 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_finset_1 :::"infinite"::: ) ) "iff" (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r1_ordinal1 :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal5 :::"decreasing"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_xboole_0 :::"empty"::: ) ($#v2_ordinal2 :::"increasing"::: ) ($#v1_ordinal5 :::"decreasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_afinsq_1 :::"<%"::: ) "a" ($#k3_afinsq_1 :::"%>"::: ) ) -> ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ; end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_afinsq_1 :::"<%"::: ) "a" ($#k3_afinsq_1 :::"%>"::: ) ) -> ($#v2_ordinal2 :::"increasing"::: ) ($#v1_ordinal5 :::"decreasing"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ($#v2_ordinal2 :::"increasing"::: ) ($#v1_ordinal5 :::"decreasing"::: ) ($#v2_ordinal5 :::"non-decreasing"::: ) ($#v3_ordinal5 :::"non-increasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ORDINAL5:6 (Bool "for" (Set (Var "f")) "being" ($#v2_ordinal5 :::"non-decreasing"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Bool "not" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "f"))) ($#r1_ordinal2 :::"is_limes_of"::: ) (Set (Var "f")))) ; theorem :: ORDINAL5:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "a")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "b")) ")" )))) ; theorem :: ORDINAL5:8 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_ordinal5 :::"non-decreasing"::: ) ))) ; theorem :: ORDINAL5:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) ; theorem :: ORDINAL5:10 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_ordinal2 :::"increasing"::: ) ))) ; theorem :: ORDINAL5:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" )) ")" ))) ; theorem :: ORDINAL5:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "c")))) ; begin definitionlet "a", "b" be ($#m1_hidden :::"Ordinal":::); func "a" :::"|^|^"::: "b" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL5:def 4 (Bool "ex" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "phi")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "b")) & (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "b"))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" "a" "," (Set "(" (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "b")) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set "(" (Set (Var "phi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "c")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"|^|^"::: ORDINAL5:def 4 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "phi")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set "(" (Set (Var "phi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "c")) ")" ))) ")" ) ")" )) ")" )); theorem :: ORDINAL5:13 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: ORDINAL5:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b")) ")" ) ")" ))) ; theorem :: ORDINAL5:15 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set (Var "phi")))))) ; theorem :: ORDINAL5:16 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: ORDINAL5:17 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 1) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: ORDINAL5:18 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ))) ; theorem :: ORDINAL5:19 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) ")" ))) ; theorem :: ORDINAL5:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ORDINAL5:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "c")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "a"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "c")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b"))))) ; theorem :: ORDINAL5:22 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_ordinal5 :::"non-decreasing"::: ) ))) ; theorem :: ORDINAL5:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b"))))) ; theorem :: ORDINAL5:24 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "n")))))) ; theorem :: ORDINAL5:25 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_ordinal2 :::"increasing"::: ) ))) ; theorem :: ORDINAL5:26 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b"))))) ; theorem :: ORDINAL5:27 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "n")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Set (Var "k"))))) ; registrationlet "n", "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k12_ordinal2 :::"exp"::: ) "(" "n" "," "k" ")" ) -> ($#v7_ordinal1 :::"natural"::: ) ; end; registrationlet "n", "k" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k1_ordinal5 :::"|^|^"::: ) "k") -> ($#v7_ordinal1 :::"natural"::: ) ; end; theorem :: ORDINAL5:28 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "n")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k")))) ; theorem :: ORDINAL5:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "n")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ; theorem :: ORDINAL5:30 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) ; theorem :: ORDINAL5:31 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )))) ; theorem :: ORDINAL5:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )))) ; begin scheme :: ORDINAL5:sch 1 CriticalNumber2{ F1() -> ($#m1_hidden :::"Ordinal":::), F2() -> ($#m1_hidden :::"Ordinal-Sequence":::), F3( ($#m1_hidden :::"Ordinal":::)) -> ($#m1_hidden :::"Ordinal":::) } : (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_ordinal1 :::"c="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set F2 "(" ")" ))) & (Bool (Set F3 "(" (Set "(" ($#k3_card_3 :::"Union"::: ) (Set F2 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set F2 "(" ")" ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set F1 "(" ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) & (Bool (Set F3 "(" (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set F2 "(" ")" )) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" ) ")" ) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set F3 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "b")) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set F3 "(" (Set (Var "a")) ")" ) ($#r1_ordinal2 :::"is_limes_of"::: ) (Set (Var "phi"))))) and (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F2 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) ")" ) and (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) "holds" (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ))) proof end; scheme :: ORDINAL5:sch 2 CriticalNumber3{ F1() -> ($#m1_hidden :::"Ordinal":::), F2( ($#m1_hidden :::"Ordinal":::)) -> ($#m1_hidden :::"Ordinal":::) } : (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set F2 "(" (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set F2 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" (Set (Var "b")) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set F2 "(" (Set (Var "a")) ")" ) ($#r1_ordinal2 :::"is_limes_of"::: ) (Set (Var "phi"))))) proof end; begin definitionlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; attr "a" is :::"epsilon"::: means :: ORDINAL5:def 5 (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," "a" ")" ) ($#r1_hidden :::"="::: ) "a"); end; :: deftheorem defines :::"epsilon"::: ORDINAL5:def 5 : (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v4_ordinal5 :::"epsilon"::: ) ) "iff" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )); theorem :: ORDINAL5:33 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "is" ($#v4_ordinal5 :::"epsilon"::: ) ) ")" ))) ; registration cluster ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v4_ordinal5 :::"epsilon"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "a" be ($#m1_hidden :::"Ordinal":::); func :::"first_epsilon_greater_than"::: "a" -> ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) means :: ORDINAL5:def 6 (Bool "(" (Bool "a" ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "b")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool "a" ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool it ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" ) ")" ); end; :: deftheorem defines :::"first_epsilon_greater_than"::: ORDINAL5:def 6 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b2")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" ) ")" ) ")" ))); theorem :: ORDINAL5:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "a"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "b"))))) ; theorem :: ORDINAL5:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "a"))))) ; theorem :: ORDINAL5:36 (Bool (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ; theorem :: ORDINAL5:37 (Bool "for" (Set (Var "e")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "e")))) ; registration cluster ($#v3_ordinal1 :::"ordinal"::: ) ($#v4_ordinal5 :::"epsilon"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_ordinal1 :::"limit_ordinal"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ORDINAL5:38 (Bool "for" (Set (Var "e")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "e")) "," (Set ($#k4_ordinal1 :::"omega"::: ) ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "e")) "," (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "e")) "," (Set ($#k4_ordinal1 :::"omega"::: ) ) ")" ")" ) ")" ))) ; theorem :: ORDINAL5:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "e")) ($#k1_ordinal5 :::"|^|^"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set "(" (Set (Var "e")) ($#k1_ordinal5 :::"|^|^"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: ORDINAL5:40 (Bool "for" (Set (Var "e")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "e")) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )))) ; definitionlet "a" be ($#m1_hidden :::"Ordinal":::); func :::"epsilon_"::: "a" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL5:def 7 (Bool "ex" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "phi")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "a")) & (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "a"))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "a")) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set "(" (Set (Var "phi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "c")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"epsilon_"::: ORDINAL5:def 7 : (Bool "for" (Set (Var "a")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "phi")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set "(" (Set (Var "phi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "c")) ")" ))) ")" ) ")" )) ")" )); theorem :: ORDINAL5:41 (Bool (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ; theorem :: ORDINAL5:42 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "a")) ")" ) ($#k1_ordinal5 :::"|^|^"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )))) ; theorem :: ORDINAL5:43 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k8_ordinal2 :::"lim"::: ) (Set (Var "phi")))))) ; theorem :: ORDINAL5:44 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "b"))))) ; theorem :: ORDINAL5:45 (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) )) ; theorem :: ORDINAL5:46 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "phi")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "phi")))))) ; theorem :: ORDINAL5:47 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "b")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "c")))) ")" )) ")" ))) ; theorem :: ORDINAL5:48 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "a"))))) ; theorem :: ORDINAL5:49 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::)) & (Bool "ex" (Set (Var "e")) "being" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "e"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) "is" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::))) ; theorem :: ORDINAL5:50 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::)) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_ordinal5 :::"first_epsilon_greater_than"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) "is" ($#v4_ordinal5 :::"epsilon"::: ) ($#m1_hidden :::"Ordinal":::))) ; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_ordinal5 :::"epsilon_"::: ) "a") -> ($#v4_ordinal5 :::"epsilon"::: ) ; end; theorem :: ORDINAL5:51 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) "is" ($#v4_ordinal5 :::"epsilon"::: ) )) "holds" (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal5 :::"epsilon_"::: ) (Set (Var "b")))))) ; begin definitionlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal-Sequence":::); func :::"Sum^"::: "A" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL5:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "f")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_afinsq_1 :::"dom"::: ) "A" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) "A"))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Sum^"::: ORDINAL5:def 8 : (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "f")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) ")" ))); theorem :: ORDINAL5:52 (Bool (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: ORDINAL5:53 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "a")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: ORDINAL5:54 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set "(" (Set (Var "A")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "a")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "a")))))) ; theorem :: ORDINAL5:55 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "a")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A")) ")" ))))) ; theorem :: ORDINAL5:56 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A"))))) ; definitionlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; attr "a" is :::"Cantor-component"::: means :: ORDINAL5:def 9 (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool "a" ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "b")) ")" ")" ))) ")" ))); end; :: deftheorem defines :::"Cantor-component"::: ORDINAL5:def 9 : (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v5_ordinal5 :::"Cantor-component"::: ) ) "iff" (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "b")) ")" ")" ))) ")" ))) ")" )); registration cluster ($#v3_ordinal1 :::"ordinal"::: ) ($#v5_ordinal5 :::"Cantor-component"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v5_ordinal5 :::"Cantor-component"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "a", "b" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; func "b" :::"-exponent"::: "a" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL5:def 10 (Bool "(" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" "b" "," it ")" ) ($#r1_ordinal1 :::"c="::: ) "a") & (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" "b" "," (Set (Var "c")) ")" ) ($#r1_ordinal1 :::"c="::: ) "a")) "holds" (Bool (Set (Var "c")) ($#r1_ordinal1 :::"c="::: ) it) ")" ) ")" ) if (Bool "(" (Bool (Num 1) ($#r2_hidden :::"in"::: ) "b") & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) "a") ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"-exponent"::: ORDINAL5:def 10 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "(" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "b3")) ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b3"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) "or" "not" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); theorem :: ORDINAL5:57 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a")) ")" ) ")" ) ")" ))) ; theorem :: ORDINAL5:58 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ORDINAL5:59 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "a")) ($#k6_ordinal3 :::"div^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) ; theorem :: ORDINAL5:60 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k6_ordinal3 :::"div^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )))) ; theorem :: ORDINAL5:61 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k7_ordinal3 :::"mod^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) ; theorem :: ORDINAL5:62 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a")) ")" ) ")" ")" ) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "c")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a")) ")" ) ")" )) ")" )))) ; theorem :: ORDINAL5:63 (Bool "for" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "c")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "c")) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "a")))) ; definitionlet "A" be ($#m1_hidden :::"Ordinal-Sequence":::); attr "A" is :::"Cantor-normal-form"::: means :: ORDINAL5:def 11 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "A"))) "holds" (Bool (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#v5_ordinal5 :::"Cantor-component"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "A"))) "holds" (Bool (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Cantor-normal-form"::: ORDINAL5:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#v5_ordinal5 :::"Cantor-component"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) -> ($#v6_ordinal5 :::"Cantor-normal-form"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ($#v6_ordinal5 :::"Cantor-normal-form"::: ) -> ($#v1_ordinal5 :::"decreasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ORDINAL5:64 (Bool "for" (Set (Var "A")) "being" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDINAL5:65 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "n")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" ($#k12_ordinal2 :::"exp"::: ) "(" (Set ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_ordinal2 :::"Ordinal-yielding"::: ) ($#v6_ordinal5 :::"Cantor-normal-form"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ORDINAL5:66 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set (Set (Var "A")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "B"))) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ) & (Bool (Set (Var "B")) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ) ")" )) ; theorem :: ORDINAL5:67 (Bool "for" (Set (Var "A")) "being" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#v5_ordinal5 :::"Cantor-component"::: ) ($#m1_hidden :::"Ordinal":::)(Bool "ex" (Set (Var "B")) "being" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "c")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "B"))))))) ; theorem :: ORDINAL5:68 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v5_ordinal5 :::"Cantor-component"::: ) ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#k5_ordinal5 :::"-exponent"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "c")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "A"))) "is" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ))) ; theorem :: ORDINAL5:69 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "A")) "being" ($#v6_ordinal5 :::"Cantor-normal-form"::: ) ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal5 :::"Sum^"::: ) (Set (Var "A")))))) ;