:: Extended Natural Numbers and Counters
:: by Sebastian Koch
::
:: Received October 25, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


definition
func ExtNAT -> Subset of ExtREAL equals :: COUNTERS:def 1
NAT \/ {+infty};
coherence
NAT \/ {+infty} is Subset of ExtREAL
proof end;
end;

:: deftheorem defines ExtNAT COUNTERS:def 1 :
ExtNAT = NAT \/ {+infty};

theorem Th1: :: COUNTERS:1
( NAT c< ExtNAT & ExtNAT c< ExtREAL )
proof end;

registration
cluster ExtNAT -> non empty infinite ;
coherence
( not ExtNAT is empty & not ExtNAT is finite )
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 :
for x being object holds
( x is ext-natural iff x in ExtNAT );

registration
cluster +infty -> ext-natural ;
coherence
+infty is ext-natural
by ZFMISC_1:136;
cluster ext-natural -> ext-real for object ;
coherence
for b1 being object st b1 is ext-natural holds
b1 is ext-real
;
cluster natural -> ext-natural for object ;
coherence
for b1 being object st b1 is natural holds
b1 is ext-natural
proof end;
cluster finite ext-natural -> natural for set ;
coherence
for b1 being set st b1 is finite & b1 is ext-natural holds
b1 is natural
proof end;
end;

registration
cluster zero ext-natural for object ;
existence
ex b1 being object st
( b1 is zero & b1 is ext-natural )
proof end;
cluster non zero ext-natural for object ;
existence
ex b1 being object st
( not b1 is zero & b1 is ext-natural )
proof end;
cluster ext-natural for set ;
existence
ex b1 being number st b1 is ext-natural
proof end;
cluster -> ext-natural for Element of ExtNAT ;
coherence
for b1 being Element of ExtNAT holds b1 is ext-natural
;
end;

definition
mode ExtNat is ext-natural ExtReal;
end;

registration
let x be ExtNat;
reduce In (x,ExtNAT) to x;
reducibility
In (x,ExtNAT) = x
by Def1, SUBSET_1:def 8;
end;

registration
ExtNat ex b1 being set st
for b2 being ExtNat holds b2 in b1
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
for b1 being object st b1 is zero holds
b1 is ext-natural
;
cluster ext-real ext-natural -> non negative for object ;
coherence
for b1 being ExtReal st b1 is ext-natural holds
not b1 is negative
by Th3;
end;

registration
cluster ext-real ext-natural -> non negative for object ;
coherence
for b1 being ExtNat holds not b1 is negative
;
cluster non zero ext-real ext-natural -> positive for object ;
coherence
for b1 being ExtNat st not b1 is zero holds
b1 is positive
;
end;

registration
let N, M be ExtNat;
cluster min (N,M) -> ext-natural ;
coherence
min (N,M) is ext-natural
by XXREAL_0:def 9;
cluster max (N,M) -> ext-natural ;
coherence
max (N,M) is ext-natural
by XXREAL_0:def 10;
cluster N + M -> ext-natural ;
coherence
N + M is ext-natural
proof end;
cluster N * M -> ext-natural ;
coherence
N * M is 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
not M + N is zero
;
cluster N + M -> non zero ;
coherence
not N + M is 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 :
for X being set holds
( X is ext-natural-membered iff for x being object st x in X holds
x is ext-natural );

registration
cluster empty -> ext-natural-membered for set ;
coherence
for b1 being set st b1 is empty holds
b1 is ext-natural-membered
;
cluster natural-membered -> ext-natural-membered for set ;
coherence
for b1 being set st b1 is natural-membered holds
b1 is ext-natural-membered
;
cluster ext-natural-membered -> ext-real-membered for set ;
coherence
for b1 being set st b1 is ext-natural-membered holds
b1 is ext-real-membered
proof end;
cluster ExtNAT -> ext-natural-membered ;
coherence
ExtNAT is ext-natural-membered
;
end;

registration
cluster non empty ext-natural-membered for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is ext-natural-membered )
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;
coherence
for b1 being Element of X holds b1 is ext-natural
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;
coherence
for b1 being Subset of X holds b1 is ext-natural-membered
;
end;

registration
let N be ExtNat;
cluster {N} -> ext-natural-membered ;
coherence
{N} is ext-natural-membered
by TARSKI:def 1;
let M be ExtNat;
cluster {N,M} -> ext-natural-membered ;
coherence
{N,M} is ext-natural-membered
proof end;
let K be ExtNat;
cluster {N,M,K} -> ext-natural-membered ;
coherence
{N,M,K} is ext-natural-membered
proof end;
end;

registration
let X, Y be ext-natural-membered set ;
cluster X \/ Y -> ext-natural-membered ;
coherence
X \/ Y is ext-natural-membered
proof end;
end;

registration
let X be ext-natural-membered set ;
let Y be set ;
cluster X /\ Y -> ext-natural-membered ;
coherence
X /\ Y is ext-natural-membered
proof end;
cluster X \ Y -> ext-natural-membered ;
coherence
X \ Y is ext-natural-membered
;
end;

registration
let X, Y be ext-natural-membered set ;
cluster X \+\ Y -> ext-natural-membered ;
coherence
X \+\ Y is 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;
compatibility
( X c= Y iff for N being ExtNat st N in X holds
N in Y )
proof end;
end;

:: deftheorem defines c= COUNTERS:def 4 :
for X being ext-natural-membered set
for Y being set holds
( X c= Y iff for N being ExtNat st N in X holds
N in Y );

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 );
compatibility
( X = Y iff for N being ExtNat holds
( N in X iff N in Y ) )
proof end;
end;

:: deftheorem defines = COUNTERS:def 5 :
for X, Y being ext-natural-membered set holds
( X = Y iff for N being ExtNat holds
( N in X iff N in Y ) );

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 );
compatibility
( X misses Y iff for N being ExtNat holds
( not N in X or not N in Y ) )
proof end;
end;

:: deftheorem defines misses COUNTERS:def 6 :
for X, Y being ext-natural-membered set holds
( X misses Y iff for N being ExtNat holds
( not N in X or not N in Y ) );

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{ P1[ object ] } :
ex X being ext-natural-membered set st
for N being ExtNat holds
( N in X iff P1[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;
compatibility
for b1 being object holds
( b1 is UpperBound of X iff for N being ExtNat st N in X holds
N <= b1 )
proof end;
redefine mode LowerBound of X means :DefL: :: COUNTERS:def 8
for N being ExtNat st N in X holds
it <= N;
compatibility
for b1 being object holds
( b1 is LowerBound of X iff for N being ExtNat st N in X holds
b1 <= N )
proof end;
end;

:: deftheorem DefU defines UpperBound COUNTERS:def 7 :
for X being ext-natural-membered set
for b2 being object holds
( b2 is UpperBound of X iff for N being ExtNat st N in X holds
N <= b2 );

:: deftheorem DefL defines LowerBound COUNTERS:def 8 :
for X being ext-natural-membered set
for b2 being object holds
( b2 is LowerBound of X iff for N being ExtNat st N in X holds
b2 <= N );

registration
cluster ext-natural-membered -> bounded_below ext-natural-membered for set ;
coherence
for b1 being ext-natural-membered set holds b1 is bounded_below
proof end;
cluster non empty ext-natural-membered -> left_end ext-natural-membered for set ;
coherence
for b1 being ext-natural-membered set st not b1 is empty holds
b1 is left_end
proof end;
end;

registration
let X be ext-natural-membered set ;
cluster ext-real ext-natural for UpperBound of X;
existence
ex b1 being UpperBound of X st b1 is ext-natural
proof end;
cluster ext-real ext-natural for LowerBound of X;
existence
ex b1 being LowerBound of X st b1 is ext-natural
proof end;
cluster inf X -> ext-natural ;
coherence
inf X is ext-natural
proof end;
end;

registration
let X be non empty ext-natural-membered set ;
cluster sup X -> ext-natural ;
coherence
sup X is ext-natural
proof end;
end;

registration
cluster non empty bounded_above ext-natural-membered -> right_end ext-natural-membered for set ;
coherence
for b1 being ext-natural-membered set st not b1 is empty & b1 is bounded_above holds
b1 is right_end
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
inf X is ExtNat
;
compatibility
for b1 being ExtNat holds
( b1 = inf X iff ( b1 in X & ( for N being ExtNat st N in X holds
b1 <= N ) ) )
proof end;
end;

:: deftheorem defines min COUNTERS:def 9 :
for X being left_end ext-natural-membered set
for b2 being ExtNat holds
( b2 = min X iff ( b2 in X & ( for N being ExtNat st N in X holds
b2 <= N ) ) );

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
sup X is ExtNat
;
compatibility
for b1 being ExtNat holds
( b1 = sup X iff ( b1 in X & ( for N being ExtNat st N in X holds
N <= b1 ) ) )
proof end;
end;

:: deftheorem defines max COUNTERS:def 10 :
for X being right_end ext-natural-membered set
for b2 being ExtNat holds
( b2 = max X iff ( b2 in X & ( for N being ExtNat st N in X holds
N <= b2 ) ) );

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 :
for R being Relation holds
( R is ext-natural-valued iff rng R c= ExtNAT );

registration
cluster Relation-like empty -> ext-natural-valued for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is ext-natural-valued
proof end;
cluster Relation-like natural-valued -> ext-natural-valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is ext-natural-valued
proof end;
cluster Relation-like ext-natural-valued -> ExtNAT -valued ext-real-valued for set ;
coherence
for b1 being Relation st b1 is ext-natural-valued holds
( b1 is ExtNAT -valued & b1 is ext-real-valued )
by RELAT_1:def 19, XBOOLE_1:1, VALUED_0:def 2;
cluster Relation-like ExtNAT -valued -> ext-natural-valued for set ;
coherence
for b1 being Relation st b1 is ExtNAT -valued holds
b1 is ext-natural-valued
by RELAT_1:def 19;
end;

registration
cluster Relation-like Function-like ext-natural-valued for set ;
existence
ex b1 being Function st b1 is ext-natural-valued
proof end;
end;

registration
let R be ext-natural-valued Relation;
cluster rng R -> ext-natural-membered ;
coherence
rng R is 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;
coherence
for b1 being Subset of R holds b1 is ext-natural-valued
;
end;

registration
let R, S be ext-natural-valued Relation;
cluster R \/ S -> ext-natural-valued ;
coherence
R \/ S is ext-natural-valued
;
end;

registration
let R be ext-natural-valued Relation;
let S be Relation;
cluster R /\ S -> ext-natural-valued ;
coherence
R /\ S is ext-natural-valued
;
cluster R \ S -> ext-natural-valued ;
coherence
R \ S is ext-natural-valued
;
cluster S * R -> ext-natural-valued ;
coherence
S * R is ext-natural-valued
;
end;

registration
let R, S be ext-natural-valued Relation;
cluster R \+\ S -> ext-natural-valued ;
coherence
R \+\ S is ext-natural-valued
proof end;
end;

registration
let R be ext-natural-valued Relation;
let X be set ;
cluster R .: X -> ext-natural-membered ;
coherence
R .: X is ext-natural-membered
proof end;
cluster R | X -> ext-natural-valued ;
coherence
R | X is ext-natural-valued
;
cluster X |` R -> ext-natural-valued ;
coherence
X |` R is ext-natural-valued
;
end;

registration
let R be ext-natural-valued Relation;
let x be object ;
cluster Im (R,x) -> ext-natural-membered ;
coherence
Im (R,x) is ext-natural-membered
proof end;
end;

registration
let X be ext-natural-membered set ;
cluster id X -> ext-natural-valued ;
coherence
id X is ext-natural-valued
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 ;
compatibility
( f is ext-natural-valued iff 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 :
for f being Function holds
( f is ext-natural-valued iff for x being object st x in dom f holds
f . x is ext-natural );

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
f . x is ext-natural
by ThFunc1;
end;

registration
let X be set ;
let N be ExtNat;
cluster X --> N -> ext-natural-valued ;
coherence
X --> N is ext-natural-valued
proof end;
end;

registration
let f, g be ext-natural-valued Function;
cluster f +* g -> ext-natural-valued ;
coherence
f +* g is ext-natural-valued
proof end;
end;

registration
let x be object ;
let N be ExtNat;
cluster x .--> N -> ext-natural-valued ;
coherence
x .--> N is 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:];
coherence
for b1 being Relation of Z,X holds b1 is ext-natural-valued
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;
coherence
for b1 being Relation of Z,X st b1 = [:Z,X:] holds
b1 is ext-natural-valued
;
end;

registration
cluster Relation-like Function-like constant non empty ext-natural-valued for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is ext-natural-valued )
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 ;
coherence
for b1 being set st b1 is ordinal holds
b1 is c=-linear
proof end;
end;

:: into ORDINAL1 ? ::: generalize in ORDINAL2
registration
let f be Ordinal-yielding Function;
let x be object ;
cluster f . x -> ordinal ;
coherence
f . x is ordinal
proof end;
end;

:: into ORDINAL4 ?
registration
let A, B be non-empty Sequence;
cluster A ^ B -> non-empty ;
coherence
A ^ B is 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 ;
coherence
card X is trivial
proof end;
end;

:: into CARD_2 ?
registration
let c1 be Cardinal;
let c2 be non empty Cardinal;
cluster c1 +` c2 -> non empty ;
coherence
not c1 +` c2 is 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 ;
coherence
f * g is Cardinal-yielding
proof end;
end;

:: into CARD_3 ?
registration
cluster Relation-like Function-like natural-valued -> Cardinal-yielding for set ;
coherence
for b1 being Function st b1 is natural-valued holds
b1 is Cardinal-yielding
proof end;
end;

:: into CARD_3 ?
registration
let f be empty Function;
cluster disjoin f -> empty ;
coherence
disjoin f is empty
by CARD_3:3;
end;

:: into CARD_3 ?
registration
let f be empty-yielding Function;
cluster disjoin f -> empty-yielding ;
coherence
disjoin f is empty-yielding
proof end;
end;

:: into CARD_3 ?
registration
let f be non empty-yielding Function;
cluster disjoin f -> non empty-yielding ;
coherence
not disjoin f is empty-yielding
proof end;
end;

:: into CARD_3 ?
registration
let f be empty-yielding Function;
cluster Union f -> empty ;
coherence
Union f is empty
proof end;
end;

:: into CARD_3 ?
registration
cluster Relation-like Function-like Cardinal-yielding -> Ordinal-yielding for set ;
coherence
for b1 being Function st b1 is Cardinal-yielding holds
b1 is Ordinal-yielding
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 ;
coherence
Card A is 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 ;
coherence
Card f is trivial
proof end;
end;

:: into CARD_3 ?
registration
let f be non trivial Function;
cluster Card f -> non trivial ;
coherence
not Card f is trivial
proof end;
end;

:: into CARD_3 ?
registration
let A, B be Cardinal-yielding Sequence;
cluster A ^ B -> Cardinal-yielding ;
coherence
A ^ B is Cardinal-yielding
proof end;
end;

:: into CARD_3 or AFINSQ_1 ?
registration
let c1 be Cardinal;
cluster <%c1%> -> Cardinal-yielding ;
coherence
<%c1%> is Cardinal-yielding
proof end;
let c2 be Cardinal;
cluster <%c1,c2%> -> Cardinal-yielding ;
coherence
<%c1,c2%> is Cardinal-yielding
proof end;
let c3 be Cardinal;
cluster <%c1,c2,c3%> -> Cardinal-yielding ;
coherence
<%c1,c2,c3%> is 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 ;
coherence
<%X1,X2,X3%> is non-empty
proof end;
end;

:: into AFINSQ_1 ?
registration
let A be infinite Ordinal;
cluster <%A%> -> non natural-valued ;
coherence
not <%A%> is natural-valued
proof end;
let x be object ;
cluster <%A,x%> -> non natural-valued ;
coherence
not <%A,x%> is natural-valued
proof end;
cluster <%x,A%> -> non natural-valued ;
coherence
not <%x,A%> is natural-valued
proof end;
let y be object ;
cluster <%A,x,y%> -> non natural-valued ;
coherence
not <%A,x,y%> is natural-valued
proof end;
cluster <%x,A,y%> -> non natural-valued ;
coherence
not <%x,A,y%> is natural-valued
proof end;
cluster <%x,y,A%> -> non natural-valued ;
coherence
not <%x,y,A%> is 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 ;
existence
ex b1 being XFinSequence st
( not b1 is empty & b1 is non-empty & b1 is natural-valued )
proof end;
let x be object ;
cluster <%x%> -> one-to-one ;
coherence
<%x%> is 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
<%x%> is trivial
;
let y be object ;
cluster <%x,y%> -> non trivial ;
coherence
not <%x,y%> is trivial
proof end;
let z be object ;
cluster <%x,y,z%> -> non trivial ;
coherence
not <%x,y,z%> is 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 ;
existence
ex b1 being XFinSequence st
( not b1 is empty & b1 is trivial )
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 ;
existence
ex b1 being XFinSequence of D st
( not b1 is empty & b1 is trivial )
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 :
for R being Relation holds
( R is with_cardinal_domain iff ex c being Cardinal st dom R = c );

registration
cluster Relation-like empty -> with_cardinal_domain for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is with_cardinal_domain
;
cluster Relation-like Sequence-like finite -> with_cardinal_domain for set ;
coherence
for b1 being Relation st b1 is finite & b1 is Sequence-like holds
b1 is with_cardinal_domain
proof end;
cluster Relation-like with_cardinal_domain -> Sequence-like for set ;
coherence
for b1 being Relation st b1 is with_cardinal_domain holds
b1 is Sequence-like
by ORDINAL1:def 7;
let c be Cardinal;
cluster Relation-like c -defined Function-like total -> with_cardinal_domain for set ;
coherence
for b1 being ManySortedSet of c holds b1 is with_cardinal_domain
by PARTFUN1:def 2;
let x be object ;
cluster c --> x -> with_cardinal_domain ;
coherence
c --> x is 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:];
coherence
for b1 being Denumeration of X holds b1 is with_cardinal_domain
proof end;
end;

registration
let c be Cardinal;
cluster Function-like quasi_total bijective -> with_cardinal_domain for Element of bool [:c,c:];
coherence
for b1 being Permutation of c holds b1 is with_cardinal_domain
;
end;

registration
cluster Relation-like non-empty Function-like non empty trivial Cardinal-yielding with_cardinal_domain for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is trivial & b1 is non-empty & b1 is with_cardinal_domain & b1 is Cardinal-yielding )
proof end;
cluster Relation-like non-empty Function-like non empty non trivial finite Cardinal-yielding with_cardinal_domain for set ;
existence
ex b1 being Function st
( not b1 is empty & not b1 is trivial & b1 is non-empty & b1 is finite & b1 is with_cardinal_domain & b1 is Cardinal-yielding )
proof end;
cluster Relation-like non-empty Function-like non empty infinite natural-valued with_cardinal_domain for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is non-empty & b1 is infinite & b1 is with_cardinal_domain & b1 is natural-valued )
proof end;
cluster Relation-like non-empty Function-like non trivial non natural-valued Cardinal-yielding with_cardinal_domain for set ;
existence
ex b1 being Function st
( not b1 is trivial & b1 is non-empty & b1 is with_cardinal_domain & b1 is Cardinal-yielding & not b1 is natural-valued )
proof end;
end;

registration
let R be with_cardinal_domain Relation;
cluster dom R -> cardinal ;
coherence
dom R is cardinal
proof end;
end;

registration
let f be with_cardinal_domain Function;
identify dom f with card f;
correctness
compatibility
dom f = card f
;
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 ;
coherence
R * P is with_cardinal_domain
proof end;
end;

registration
let g be Function;
let f be Denumeration of (dom g);
cluster f * g -> with_cardinal_domain ;
coherence
g * f is 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 ;
coherence
f * p is 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 ;
coherence
p ^ B is with_cardinal_domain
proof end;
end;

definition
mode Counters is non empty Cardinal-yielding with_cardinal_domain Function;
end;

definition
mode Counters+ is non-empty non empty Cardinal-yielding with_cardinal_domain Function;
end;