COUNTERS: Extended Natural Numbers and Counters

proof end;

end;

:: deftheorem defines ExtNAT COUNTERS:def 1 :

theorem Th1: :: COUNTERS:1

( NAT c< ExtNAT & ExtNAT c< ExtREAL )

proof end;

registration

cluster ExtNAT -> non empty infinite ;

coherence by Th1, FINSET_1:1, XBOOLE_0:def 8;

end;

definition

let x be object ;

attr x is ext-natural means :Def1: :: COUNTERS:def 2
x in ExtNAT ;

end;

:: deftheorem Def1 defines ext-natural COUNTERS:def 2 :

registration

cluster +infty -> ext-natural ;

coherence by ZFMISC_1:136;

cluster ext-natural -> ext-real for object ;

coherence ;

cluster natural -> ext-natural for object ;

proof end;

cluster finite ext-natural -> natural for set ;

proof end;

end;

registration

cluster zero ext-natural for object ;

proof end;

cluster non zero ext-natural for object ;

proof end;

cluster ext-natural for set ;

proof end;

cluster -> ext-natural for Element of ExtNAT ;

end;

definition

mode ExtNat is ext-natural ExtReal;

end;

registration

let x be ExtNat;

reduce In (x,ExtNAT) to x;

reducibility by Def1, SUBSET_1:def 8;

end;

registration

ExtNat ex b₁ being set st
for b₂ being ExtNat holds b₂ in b₁

proof end;

end;

theorem Th3: :: COUNTERS:2

for x being object holds
( x is ExtNat iff ( x is Nat or x = +infty ) )

proof end;

registration

cluster zero -> ext-natural for object ;

coherence ;

cluster ext-real ext-natural -> non negative for object ;

coherence by Th3;

end;

registration

cluster ext-real ext-natural -> non negative for object ;

coherence ;

cluster non zero ext-real ext-natural -> positive for object ;

end;

registration

let N, M be ExtNat;

cluster min (N,M) -> ext-natural ;

coherence by XXREAL_0:def 9;

cluster max (N,M) -> ext-natural ;

coherence by XXREAL_0:def 10;

cluster N + M -> ext-natural ;

proof end;

cluster N * M -> ext-natural ;

proof end;

end;

theorem :: COUNTERS:3

for N being ExtNat holds 0 <= N ;

theorem :: COUNTERS:4

for N being ExtNat st 0 <> N holds
0 < N ;

theorem :: COUNTERS:5

for N being ExtNat holds 0 < N + 1 ;

theorem Th5: :: COUNTERS:6

for N, M being ExtNat st M in NAT & N <= M holds
N in NAT

proof end;

theorem :: COUNTERS:7

for N, M being ExtNat st N < M holds
N in NAT

proof end;

theorem :: COUNTERS:8

for N, M, K being ExtNat st N <= M holds
N * K <= M * K by XXREAL_3:71;

theorem :: COUNTERS:9

for N being ExtNat holds
( N = 0 or ex K being ExtNat st N = K + 1 )

proof end;

theorem :: COUNTERS:10

for N, M being ExtNat st N + M = 0 holds
( N = 0 & M = 0 ) ;

registration

let M be ExtNat;
let N be non zero ExtNat;

cluster M + N -> non zero ;

coherence ;

cluster N + M -> non zero ;

end;

theorem Th10: :: COUNTERS:11

for N, M being ExtNat holds
( not N <= M + 1 or N <= M or N = M + 1 )

proof end;

theorem :: COUNTERS:12

for N, M being ExtNat st N <= M & M <= N + 1 & not N = M holds
M = N + 1

proof end;

theorem :: COUNTERS:13

for N, M being ExtNat st N <= M holds
ex K being ExtNat st M = N + K

proof end;

theorem :: COUNTERS:14

for N, M being ExtNat holds N <= N + M

proof end;

theorem :: COUNTERS:15

for N, M, K being ExtNat st N <= M holds
N <= M + K

proof end;

theorem Th4c: :: COUNTERS:16

for N being ExtNat st N < 1 holds
N = 0

proof end;

theorem :: COUNTERS:17

for N, M being ExtNat st N * M = 1 holds
N = 1

proof end;

theorem :: COUNTERS:18

for N, K being ExtNat holds
( K < K + N iff ( 1 <= N & K <> +infty ) )

proof end;

theorem :: COUNTERS:19

for N, M, K being ExtNat st K <> 0 & N = M * K holds
M <= N

proof end;

theorem :: COUNTERS:20

for N, M, K being ExtNat st M <= N holds
M * K <= N * K by XXREAL_3:71;

theorem :: COUNTERS:21

for N, M, K being ExtNat holds (K + M) + N = K + (M + N) by XXREAL_3:29;

theorem :: COUNTERS:22

for N, M, K being ExtNat holds K * (N + M) = (K * N) + (K * M)

proof end;

definition

let X be set ;

attr X is ext-natural-membered means :Def2: :: COUNTERS:def 3
for x being object st x in X holds
x is ext-natural ;

end;

:: deftheorem Def2 defines ext-natural-membered COUNTERS:def 3 :

registration

cluster empty -> ext-natural-membered for set ;

coherence ;

cluster natural-membered -> ext-natural-membered for set ;

coherence ;

cluster ext-natural-membered -> ext-real-membered for set ;

proof end;

cluster ExtNAT -> ext-natural-membered ;

end;

registration

cluster non empty ext-natural-membered for set ;

proof end;

end;

theorem ThSubset: :: COUNTERS:23

for X being set holds
( X is ext-natural-membered iff X c= ExtNAT )

proof end;

registration

let X be ext-natural-membered set ;

cluster -> ext-natural for Element of X;

proof end;

end;

theorem ThEx: :: COUNTERS:24

for X being non empty ext-natural-membered set ex N being ExtNat st N in X

proof end;

theorem :: COUNTERS:25

for X being ext-natural-membered set st ( for N being ExtNat holds N in X ) holds
X = ExtNAT

proof end;

theorem :: COUNTERS:26

for X being ext-natural-membered set
for Y being set st Y c= X holds
Y is ext-natural-membered ;

registration

let X be ext-natural-membered set ;

cluster -> ext-natural-membered for Element of bool X;

end;

registration

let N be ExtNat;

cluster {N} -> ext-natural-membered ;

coherence by TARSKI:def 1;
let M be ExtNat;

cluster {N,M} -> ext-natural-membered ;

proof end;

let K be ExtNat;

cluster {N,M,K} -> ext-natural-membered ;

proof end;

end;

registration

let X, Y be ext-natural-membered set ;

cluster X \/ Y -> ext-natural-membered ;

proof end;

end;

registration

let X be ext-natural-membered set ;
let Y be set ;

cluster X /\ Y -> ext-natural-membered ;

proof end;

cluster X \ Y -> ext-natural-membered ;

end;

registration

let X, Y be ext-natural-membered set ;

cluster X \+\ Y -> ext-natural-membered ;

proof end;

end;

definition

let X be ext-natural-membered set ;
let Y be set ;

redefine pred X c= Y means :: COUNTERS:def 4
for N being ExtNat st N in X holds
N in Y;

proof end;

end;

:: deftheorem defines c= COUNTERS:def 4 :

definition

let X, Y be ext-natural-membered set ;

redefine pred X = Y means :: COUNTERS:def 5
for N being ExtNat holds
( N in X iff N in Y );

proof end;

end;

:: deftheorem defines = COUNTERS:def 5 :

definition

let X, Y be ext-natural-membered set ;

redefine pred X misses Y means :: COUNTERS:def 6
for N being ExtNat holds
( not N in X or not N in Y );

proof end;

end;

:: deftheorem defines misses COUNTERS:def 6 :

theorem :: COUNTERS:27

for F being set st ( for X being set st X in F holds
X is ext-natural-membered ) holds
union F is ext-natural-membered

proof end;

theorem :: COUNTERS:28

for F, X being set st X in F & X is ext-natural-membered holds
meet F is ext-natural-membered

proof end;

scheme :: COUNTERS:sch 1
ENMSeparation{ P₁[ object ] } :

ex X being ext-natural-membered set st
for N being ExtNat holds
( N in X iff P₁[N] )

proof end;

definition

let X be ext-natural-membered set ;

redefine mode UpperBound of X means :DefU: :: COUNTERS:def 7
for N being ExtNat st N in X holds
N <= it;

proof end;

redefine mode LowerBound of X means :DefL: :: COUNTERS:def 8
for N being ExtNat st N in X holds
it <= N;

proof end;

end;

:: deftheorem DefU defines UpperBound COUNTERS:def 7 :

:: deftheorem DefL defines LowerBound COUNTERS:def 8 :

registration

cluster ext-natural-membered -> bounded_below ext-natural-membered for set ;

proof end;

cluster non empty ext-natural-membered -> left_end ext-natural-membered for set ;

proof end;

end;

registration

let X be ext-natural-membered set ;

cluster ext-real ext-natural for UpperBound of X;

proof end;

cluster ext-real ext-natural for LowerBound of X;

proof end;

cluster inf X -> ext-natural ;

proof end;

end;

registration

let X be non empty ext-natural-membered set ;

cluster sup X -> ext-natural ;

proof end;

end;

registration

cluster non empty bounded_above ext-natural-membered -> right_end ext-natural-membered for set ;

proof end;

end;

definition

let X be left_end ext-natural-membered set ;

:: original: inf
redefine func min X -> ExtNat means :: COUNTERS:def 9
( it in X & ( for N being ExtNat st N in X holds
it <= N ) );

coherence ;
compatibility

proof end;

end;

:: deftheorem defines min COUNTERS:def 9 :

definition

let X be right_end ext-natural-membered set ;

:: original: sup
redefine func max X -> ExtNat means :: COUNTERS:def 10
( it in X & ( for N being ExtNat st N in X holds
N <= it ) );

coherence ;
compatibility

proof end;

end;

:: deftheorem defines max COUNTERS:def 10 :

definition

let R be Relation;

attr R is ext-natural-valued means :: COUNTERS:def 11
rng R c= ExtNAT ;

end;

:: deftheorem defines ext-natural-valued COUNTERS:def 11 :

registration

cluster Relation-like empty -> ext-natural-valued for set ;

proof end;

cluster Relation-like natural-valued -> ext-natural-valued for set ;

proof end;

cluster Relation-like ext-natural-valued -> ExtNAT -valued ext-real-valued for set ;

coherence by RELAT_1:def 19, XBOOLE_1:1, VALUED_0:def 2;

cluster Relation-like ExtNAT -valued -> ext-natural-valued for set ;

coherence by RELAT_1:def 19;

end;

registration

cluster Relation-like Function-like ext-natural-valued for set ;

proof end;

end;

registration

let R be ext-natural-valued Relation;

cluster rng R -> ext-natural-membered ;

end;

theorem :: COUNTERS:29

for R being Relation
for S being ext-natural-valued Relation st R c= S holds
R is ext-natural-valued ;

registration

let R be ext-natural-valued Relation;

cluster -> ext-natural-valued for Element of bool R;

end;

registration

let R, S be ext-natural-valued Relation;

cluster R \/ S -> ext-natural-valued ;

end;

registration

let R be ext-natural-valued Relation;
let S be Relation;

cluster R /\ S -> ext-natural-valued ;

coherence ;

cluster R \ S -> ext-natural-valued ;

coherence ;

cluster S * R -> ext-natural-valued ;

end;

registration

let R, S be ext-natural-valued Relation;

cluster R \+\ S -> ext-natural-valued ;

proof end;

end;

registration

let R be ext-natural-valued Relation;
let X be set ;

cluster R .: X -> ext-natural-membered ;

proof end;

cluster R | X -> ext-natural-valued ;

coherence ;

cluster X |` R -> ext-natural-valued ;

end;

registration

let R be ext-natural-valued Relation;
let x be object ;

cluster Im (R,x) -> ext-natural-membered ;

proof end;

end;

registration

let X be ext-natural-membered set ;

cluster id X -> ext-natural-valued ;

coherence by ThSubset;

end;

definition

let f be Function;

redefine attr f is ext-natural-valued means :: COUNTERS:def 12
for x being object st x in dom f holds
f . x is ext-natural ;

proof end;

end;

:: deftheorem defines ext-natural-valued COUNTERS:def 12 :

theorem ThFunc1: :: COUNTERS:30

for f being Function holds
( f is ext-natural-valued iff for x being object holds f . x is ext-natural )

proof end;

registration

let f be ext-natural-valued Function;
let x be object ;

cluster f . x -> ext-natural ;

coherence by ThFunc1;

end;

registration

let X be set ;
let N be ExtNat;

cluster X --> N -> ext-natural-valued ;

proof end;

end;

registration

let f, g be ext-natural-valued Function;

cluster f +* g -> ext-natural-valued ;

proof end;

end;

registration

let x be object ;
let N be ExtNat;

cluster x .--> N -> ext-natural-valued ;

proof end;

end;

registration

let Z be set ;
let X be ext-natural-membered set ;

cluster -> ext-natural-valued for Element of bool [:Z,X:];

proof end;

end;

registration

let Z be set ;
let X be ext-natural-membered set ;

cluster [:Z,X:] -> ext-natural-valued for Relation of Z,X;

end;

registration

cluster Relation-like Function-like constant non empty ext-natural-valued for set ;

proof end;

end;

theorem :: COUNTERS:31

for f being constant non empty ext-natural-valued Function ex N being ExtNat st
for x being object st x in dom f holds
f . x = N

proof end;

:: into ORDINAL1 ?

theorem Th2: :: COUNTERS:32

for f being Function holds
( f is Ordinal-yielding iff for x being object st x in dom f holds
f . x is Ordinal )

proof end;

:: into ORDINAL1 ?

registration

cluster ordinal -> c=-linear for set ;

proof end;

end;

:: into ORDINAL1 ? ::: generalize in ORDINAL2

registration

let f be Ordinal-yielding Function;
let x be object ;

cluster f . x -> ordinal ;

proof end;

end;

:: into ORDINAL4 ?

registration

let A, B be non-empty Sequence;

cluster A ^ B -> non-empty ;

proof end;

end;

:: into CARD_1 ? ::: version of CARD_1:64

theorem Th3: :: COUNTERS:33

for X being set
for x being object holds card (X --> x) = card X

proof end;

:: generalization of CARD_1:64
:: into CARD_1 ?

theorem :: COUNTERS:34

for c being Cardinal
for x being object holds card (c --> x) = c

proof end;

:: into CARD_1 ?

registration

let X be trivial set ;

cluster card X -> trivial ;

proof end;

end;

:: into CARD_2 ?

registration

let c1 be Cardinal;
let c2 be non empty Cardinal;

cluster c1 +` c2 -> non empty ;

proof end;

end;

:: into CARD_2 ?

theorem :: COUNTERS:35

for A being Ordinal holds
( ( A <> 0 & A <> 1 ) iff not A is trivial )

proof end;

:: into CARD_2 ?

theorem ThAdd: :: COUNTERS:36

for A being Ordinal
for B being infinite Cardinal st A in B holds
A +^ B = B

proof end;

:: into CARD_3 ?

registration

let f be Cardinal-yielding Function;
let g be Function;

cluster g * f -> Cardinal-yielding ;

proof end;

end;

:: into CARD_3 ?

registration

cluster Relation-like Function-like natural-valued -> Cardinal-yielding for set ;

proof end;

end;

:: into CARD_3 ?

registration

let f be empty Function;

cluster disjoin f -> empty ;

coherence by CARD_3:3;

end;

:: into CARD_3 ?

registration

let f be empty-yielding Function;

cluster disjoin f -> empty-yielding ;

proof end;

end;

:: into CARD_3 ?

registration

let f be non empty-yielding Function;

cluster disjoin f -> non empty-yielding ;

proof end;

end;

:: into CARD_3 ?

registration

let f be empty-yielding Function;

cluster Union f -> empty ;

proof end;

end;

:: into CARD_3 ?

registration

cluster Relation-like Function-like Cardinal-yielding -> Ordinal-yielding for set ;

proof end;

end;

:: into CARD_3 ?

theorem :: COUNTERS:37

for f being Function
for p being Permutation of (dom f) holds Card (f * p) = (Card f) * p

proof end;

:: into CARD_3 ?

registration

let A be Sequence;

cluster Card A -> Sequence-like ;

proof end;

end;

:: into CARD_3 ?

theorem :: COUNTERS:38

for A, B being Sequence holds Card (A ^ B) = (Card A) ^ (Card B)

proof end;

:: into CARD_3 ?

registration

let f be trivial Function;

cluster Card f -> trivial ;

proof end;

end;

:: into CARD_3 ?

registration

let f be non trivial Function;

cluster Card f -> non trivial ;

proof end;

end;

:: into CARD_3 ?

registration

let A, B be Cardinal-yielding Sequence;

cluster A ^ B -> Cardinal-yielding ;

proof end;

end;

:: into CARD_3 or AFINSQ_1 ?

registration

let c1 be Cardinal;

cluster <%c1%> -> Cardinal-yielding ;

proof end;

let c2 be Cardinal;

cluster <%c1,c2%> -> Cardinal-yielding ;

proof end;

let c3 be Cardinal;

cluster <%c1,c2,c3%> -> Cardinal-yielding ;

proof end;

end;

:: into CARD_3 or AFINSQ_1 ?

registration

let X1, X2, X3 be non empty set ;

cluster <%X1,X2,X3%> -> non-empty ;

proof end;

end;

:: into AFINSQ_1 ?

registration

let A be infinite Ordinal;

cluster <%A%> -> non natural-valued ;

proof end;

let x be object ;

cluster <%A,x%> -> non natural-valued ;

proof end;

cluster <%x,A%> -> non natural-valued ;

proof end;

let y be object ;

cluster <%A,x,y%> -> non natural-valued ;

proof end;

cluster <%x,A,y%> -> non natural-valued ;

proof end;

cluster <%x,y,A%> -> non natural-valued ;

proof end;

end;

:: into AFINSQ_1 ?

registration

cluster Relation-like non-empty omega -defined Sequence-like Function-like non empty finite natural-valued countable V182() for set ;

proof end;

let x be object ;

cluster <%x%> -> one-to-one ;

proof end;

end;

:: into AFINSQ_1 ?

theorem Th7: :: COUNTERS:39

for x, y being object holds
( dom <%x,y%> = {0,1} & rng <%x,y%> = {x,y} )

proof end;

:: into AFINSQ_1 ?

theorem Th8: :: COUNTERS:40

for x, y, z being object holds
( dom <%x,y,z%> = {0,1,2} & rng <%x,y,z%> = {x,y,z} )

proof end;

:: into AFINSQ_1 ?

registration

let x be object ;

cluster <%x%> -> trivial ;

coherence ;
let y be object ;

cluster <%x,y%> -> non trivial ;

proof end;

let z be object ;

cluster <%x,y,z%> -> non trivial ;

proof end;

end;

:: into AFINSQ_1 ?

registration

cluster Relation-like omega -defined Sequence-like Function-like non empty trivial finite countable V182() for set ;

proof end;

let D be non empty set ;

cluster Relation-like omega -defined D -valued Sequence-like Function-like non empty trivial finite countable V182() for set ;

proof end;

end;

:: into AFINSQ_1 ?

theorem Th9: :: COUNTERS:41

for p being non empty trivial Sequence ex x being object st p = <%x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:42

for D being non empty set
for p being non empty trivial Sequence of D ex x being Element of D st p = <%x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:43

<%0%> = id 1

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:44

<%0,1%> = id 2

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:45

<%0,1,2%> = id 3

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:46

for x, y being object holds <%x,y%> * <%1,0%> = <%y,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:47

for x, y, z being object holds <%x,y,z%> * <%0,2,1%> = <%x,z,y%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:48

for x, y, z being object holds <%x,y,z%> * <%1,0,2%> = <%y,x,z%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:49

for x, y, z being object holds <%x,y,z%> * <%1,2,0%> = <%y,z,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:50

for x, y, z being object holds <%x,y,z%> * <%2,0,1%> = <%z,x,y%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:51

for x, y, z being object holds <%x,y,z%> * <%2,1,0%> = <%z,y,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:52

for x, y being object st x <> y holds
<%x,y%> is one-to-one

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:53

for x, y, z being object st x <> y & x <> z & y <> z holds
<%x,y,z%> is one-to-one

proof end;

definition

let R be Relation;

attr R is with_cardinal_domain means :Def1: :: COUNTERS:def 13
ex c being Cardinal st dom R = c;

end;

:: deftheorem Def1 defines with_cardinal_domain COUNTERS:def 13 :

registration

cluster Relation-like empty -> with_cardinal_domain for set ;

coherence ;

cluster Relation-like Sequence-like finite -> with_cardinal_domain for set ;

proof end;

cluster Relation-like with_cardinal_domain -> Sequence-like for set ;

coherence by ORDINAL1:def 7;
let c be Cardinal;

cluster Relation-like c -defined Function-like total -> with_cardinal_domain for set ;

coherence by PARTFUN1:def 2;
let x be object ;

cluster c --> x -> with_cardinal_domain ;

end;

registration

let X be set ;

cluster Function-like one-to-one quasi_total onto -> with_cardinal_domain for Element of bool [:(card X),X:];

proof end;

end;

registration

let c be Cardinal;

cluster Function-like quasi_total bijective -> with_cardinal_domain for Element of bool [:c,c:];

end;

registration

cluster Relation-like non-empty Function-like non empty trivial Cardinal-yielding with_cardinal_domain for set ;

proof end;

cluster Relation-like non-empty Function-like non empty non trivial finite Cardinal-yielding with_cardinal_domain for set ;

proof end;

cluster Relation-like non-empty Function-like non empty infinite natural-valued with_cardinal_domain for set ;

proof end;

cluster Relation-like non-empty Function-like non trivial non natural-valued Cardinal-yielding with_cardinal_domain for set ;

proof end;

end;

registration

let R be with_cardinal_domain Relation;

cluster dom R -> cardinal ;

proof end;

end;

registration

let f be with_cardinal_domain Function;

identify dom f with card f;

correctness

proof end;

end;

registration

let R be with_cardinal_domain Relation;
let P be rng R -defined total Relation;

cluster R * P -> with_cardinal_domain ;

proof end;

end;

registration

let g be Function;
let f be Denumeration of (dom g);

cluster f * g -> with_cardinal_domain ;

proof end;

end;

registration

let f be with_cardinal_domain Function;
let p be Permutation of (dom f);

cluster p * f -> with_cardinal_domain ;

proof end;

end;

theorem Th56: :: COUNTERS:54

for A, B being with_cardinal_domain Sequence st dom A in dom B holds
A ^ B is with_cardinal_domain

proof end;

registration

let p be XFinSequence;
let B be with_cardinal_domain Sequence;

cluster p ^ B -> with_cardinal_domain ;