:: by Ievgen Ivanov , Mykola Nikitchenko , Andrii Kryvolap and Artur Korni{\l}owicz

::

:: Received August 30, 2017

:: Copyright (c) 2017 Association of Mizar Users

theorem Th1: :: NOMIN_1:1

for x being object

for n being Nat

for f being FinSequence st n in dom f holds

(<*x*> ^ f) . (n + 1) = f . n

for n being Nat

for f being FinSequence st n in dom f holds

(<*x*> ^ f) . (n + 1) = f . n

proof end;

registration
end;

:: deftheorem defines =~ NOMIN_1:def 1 :

for f, g being Function

for x, y being object holds

( f,x =~ g,y iff ( ( x in dom f implies y in dom g ) & ( y in dom g implies x in dom f ) & ( x in dom f implies f . x = g . y ) ) );

for f, g being Function

for x, y being object holds

( f,x =~ g,y iff ( ( x in dom f implies y in dom g ) & ( y in dom g implies x in dom f ) & ( x in dom f implies f . x = g . y ) ) );

registration
end;

definition

let V, A be set ;

{ d where d is TypeSSNominativeData of V,A : verum } is set ;

end;
func NDSS (V,A) -> set equals :: NOMIN_1:def 2

{ d where d is TypeSSNominativeData of V,A : verum } ;

coherence { d where d is TypeSSNominativeData of V,A : verum } ;

{ d where d is TypeSSNominativeData of V,A : verum } is set ;

:: deftheorem defines NDSS NOMIN_1:def 2 :

for V, A being set holds NDSS (V,A) = { d where d is TypeSSNominativeData of V,A : verum } ;

for V, A being set holds NDSS (V,A) = { d where d is TypeSSNominativeData of V,A : verum } ;

registration
end;

theorem Th8: :: NOMIN_1:8

for V, A being set

for f, g being finite Function st f tolerates g & f in NDSS (V,A) & g in NDSS (V,A) holds

f \/ g in NDSS (V,A)

for f, g being finite Function st f tolerates g & f in NDSS (V,A) & g in NDSS (V,A) holds

f \/ g in NDSS (V,A)

proof end;

definition

let V, A be set ;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = A & ( for n being Nat holds b_{1} . (n + 1) = NDSS (V,(A \/ (b_{1} . n))) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = A & ( for n being Nat holds b_{1} . (n + 1) = NDSS (V,(A \/ (b_{1} . n))) ) & dom b_{2} = NAT & b_{2} . 0 = A & ( for n being Nat holds b_{2} . (n + 1) = NDSS (V,(A \/ (b_{2} . n))) ) holds

b_{1} = b_{2}

end;
func FNDSC (V,A) -> Function means :Def3: :: NOMIN_1:def 3

( dom it = NAT & it . 0 = A & ( for n being Nat holds it . (n + 1) = NDSS (V,(A \/ (it . n))) ) );

existence ( dom it = NAT & it . 0 = A & ( for n being Nat holds it . (n + 1) = NDSS (V,(A \/ (it . n))) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines FNDSC NOMIN_1:def 3 :

for V, A being set

for b_{3} being Function holds

( b_{3} = FNDSC (V,A) iff ( dom b_{3} = NAT & b_{3} . 0 = A & ( for n being Nat holds b_{3} . (n + 1) = NDSS (V,(A \/ (b_{3} . n))) ) ) );

for V, A being set

for b

( b

registration
end;

theorem Th13: :: NOMIN_1:13

for V, A being set

for m, n being Nat st m <> 0 & m <= n holds

(FNDSC (V,A)) . m c= (FNDSC (V,A)) . n

for m, n being Nat st m <> 0 & m <= n holds

(FNDSC (V,A)) . m c= (FNDSC (V,A)) . n

proof end;

:: deftheorem defines IsNDRankSeq NOMIN_1:def 4 :

for V, A being set

for S being FinSequence holds

( S IsNDRankSeq V,A iff ( S . 1 = NDSS (V,A) & ( for n being Nat st n in dom S & n + 1 in dom S holds

S . (n + 1) = NDSS (V,(A \/ (S . n))) ) ) );

for V, A being set

for S being FinSequence holds

( S IsNDRankSeq V,A iff ( S . 1 = NDSS (V,A) & ( for n being Nat st n in dom S & n + 1 in dom S holds

S . (n + 1) = NDSS (V,(A \/ (S . n))) ) ) );

theorem :: NOMIN_1:14

theorem Th15: :: NOMIN_1:15

for V, A being set

for S, S1 being FinSequence st S IsNDRankSeq V,A & S1 c= S & S1 <> {} holds

S1 IsNDRankSeq V,A

for S, S1 being FinSequence st S IsNDRankSeq V,A & S1 c= S & S1 <> {} holds

S1 IsNDRankSeq V,A

proof end;

theorem Th16: :: NOMIN_1:16

for V, A being set

for n being Nat

for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S | n IsNDRankSeq V,A

for n being Nat

for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S | n IsNDRankSeq V,A

proof end;

theorem Th17: :: NOMIN_1:17

for V, A being set

for S being FinSequence st S IsNDRankSeq V,A holds

S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A

for S being FinSequence st S IsNDRankSeq V,A holds

S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A

proof end;

theorem Th19: :: NOMIN_1:19

for V, A being set

for n being Nat

for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S . n = (FNDSC (V,A)) . n

for n being Nat

for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S . n = (FNDSC (V,A)) . n

proof end;

theorem Th21: :: NOMIN_1:21

for V, A being set

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds

S1 tolerates S2

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds

S1 tolerates S2

proof end;

theorem Th22: :: NOMIN_1:22

for V, A being set

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 c= S2 holds

S2 c= S1

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 c= S2 holds

S2 c= S1

proof end;

theorem Th23: :: NOMIN_1:23

for V, A being set

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 holds

S1 +* S2 = S2

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 holds

S1 +* S2 = S2

proof end;

theorem :: NOMIN_1:24

for V, A being set

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds

S1 +* S2 IsNDRankSeq V,A by Th23;

for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds

S1 +* S2 IsNDRankSeq V,A by Th23;

theorem Th25: :: NOMIN_1:25

for V, A being set

for m, n being Nat

for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds

S . m c= S . n

for m, n being Nat

for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds

S . m c= S . n

proof end;

theorem Th26: :: NOMIN_1:26

for V, A being set

for F being FinSequence st F IsNDRankSeq V,A holds

ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

for F being FinSequence st F IsNDRankSeq V,A holds

ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

proof end;

Lm1: for V, A being set

for f being Function st ex S being FinSequence st

( S IsNDRankSeq V,A & f in Union S ) holds

f in Union (FNDSC (V,A))

proof end;

theorem :: NOMIN_1:29

for V, A being set holds <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A))))),(NDSS (V,(A \/ (NDSS (V,(A \/ (NDSS (V,A))))))))*> IsNDRankSeq V,A

proof end;

definition

let V, A be set ;

ex b_{1} being Function ex S being FinSequence st

( S IsNDRankSeq V,A & b_{1} in Union S )

ex b_{1} being set st

for b_{2} being Function st ex S being FinSequence st

( S IsNDRankSeq V,A & b_{2} in Union S ) holds

b_{2} in b_{1}

end;
mode NonatomicND of V,A -> Function means :Def5: :: NOMIN_1:def 5

ex S being FinSequence st

( S IsNDRankSeq V,A & it in Union S );

existence ex S being FinSequence st

( S IsNDRankSeq V,A & it in Union S );

ex b

( S IsNDRankSeq V,A & b

proof end;

sethood ex b

for b

( S IsNDRankSeq V,A & b

b

proof end;

:: deftheorem Def5 defines NonatomicND NOMIN_1:def 5 :

for V, A being set

for b_{3} being Function holds

( b_{3} is NonatomicND of V,A iff ex S being FinSequence st

( S IsNDRankSeq V,A & b_{3} in Union S ) );

for V, A being set

for b

( b

( S IsNDRankSeq V,A & b

theorem Th32: :: NOMIN_1:32

for V, A being set

for D being NonatomicND of V,A

for d being set st d c= D holds

d is NonatomicND of V,A

for D being NonatomicND of V,A

for d being set st d c= D holds

d is NonatomicND of V,A

proof end;

theorem Th33: :: NOMIN_1:33

for V, A being set

for D being NonatomicND of V,A ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

for D being NonatomicND of V,A ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

proof end;

registration
end;

theorem Th34: :: NOMIN_1:34

for V, A being set

for m being Nat

for S being FinSequence

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds

D1 \/ D2 in S . m

for m being Nat

for S being FinSequence

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds

D1 \/ D2 in S . m

proof end;

theorem Th35: :: NOMIN_1:35

for V, A being set

for S1, S2 being FinSequence

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 holds

D1 \/ D2 in Union S2

for S1, S2 being FinSequence

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 holds

D1 \/ D2 in Union S2

proof end;

theorem Th36: :: NOMIN_1:36

for V, A being set

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds

D1 \/ D2 is NonatomicND of V,A

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds

D1 \/ D2 is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:37

for V, A being set

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds

D1 +* D2 is NonatomicND of V,A

for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds

D1 +* D2 is NonatomicND of V,A

proof end;

definition

let V, A be set ;

ex b_{1} being set st

( b_{1} in A or b_{1} is NonatomicND of V,A )

ex b_{1} being set st

for b_{2} being set st ( b_{2} in A or b_{2} is NonatomicND of V,A ) holds

b_{2} in b_{1}

end;
mode TypeSCNominativeData of V,A -> set means :Def6: :: NOMIN_1:def 6

( it in A or it is NonatomicND of V,A );

existence ( it in A or it is NonatomicND of V,A );

ex b

( b

proof end;

sethood ex b

for b

b

proof end;

:: deftheorem Def6 defines TypeSCNominativeData NOMIN_1:def 6 :

for V, A, b_{3} being set holds

( b_{3} is TypeSCNominativeData of V,A iff ( b_{3} in A or b_{3} is NonatomicND of V,A ) );

for V, A, b

( b

definition
end;

:: deftheorem defines ND NOMIN_1:def 7 :

for V, A being set holds ND (V,A) = { D where D is TypeSCNominativeData of V,A : verum } ;

for V, A being set holds ND (V,A) = { D where D is TypeSCNominativeData of V,A : verum } ;

registration
end;

:: [v->a]

registration

let v, a be object ;

coherence

( ND_ex_1 (v,a) is Function-like & ND_ex_1 (v,a) is Relation-like ) ;

end;
coherence

( ND_ex_1 (v,a) is Function-like & ND_ex_1 (v,a) is Relation-like ) ;

theorem Th46: :: NOMIN_1:46

for a, v being object

for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) is NonatomicND of V,A

for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;

let v be Element of V;

let a be Element of A;

:: original: ND_ex_1

redefine func ND_ex_1 (v,a) -> NonatomicND of V,A;

coherence

ND_ex_1 (v,a) is NonatomicND of V,A by Th46;

end;
let v be Element of V;

let a be Element of A;

:: original: ND_ex_1

redefine func ND_ex_1 (v,a) -> NonatomicND of V,A;

coherence

ND_ex_1 (v,a) is NonatomicND of V,A by Th46;

theorem Th47: :: NOMIN_1:47

for a, v being object

for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) is TypeSCNominativeData of V,A

for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) is TypeSCNominativeData of V,A

proof end;

:: [v->[v1->a]]

:: deftheorem defines ND_ex_2 NOMIN_1:def 9 :

for v, v1, a1 being object holds ND_ex_2 (v,v1,a1) = v .--> (v1 .--> a1);

for v, v1, a1 being object holds ND_ex_2 (v,v1,a1) = v .--> (v1 .--> a1);

registration

let v, v1, a1 be object ;

coherence

( ND_ex_2 (v,v1,a1) is Function-like & ND_ex_2 (v,v1,a1) is Relation-like ) ;

end;
coherence

( ND_ex_2 (v,v1,a1) is Function-like & ND_ex_2 (v,v1,a1) is Relation-like ) ;

theorem Th48: :: NOMIN_1:48

for a1, v, v1 being object

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

proof end;

theorem Th49: :: NOMIN_1:49

for a1, v, v1 being object

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) is NonatomicND of V,A

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;

let v, v1 be Element of V;

let a be Element of A;

:: original: ND_ex_2

redefine func ND_ex_2 (v,v1,a) -> NonatomicND of V,A;

coherence

ND_ex_2 (v,v1,a) is NonatomicND of V,A

end;
let v, v1 be Element of V;

let a be Element of A;

:: original: ND_ex_2

redefine func ND_ex_2 (v,v1,a) -> NonatomicND of V,A;

coherence

ND_ex_2 (v,v1,a) is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:50

for a1, v, v1 being object

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A

for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A

proof end;

:: deftheorem defines ND_ex_3 NOMIN_1:def 10 :

for v, v1, a, a1 being object holds ND_ex_3 (v,v1,a,a1) = (v,v1) --> (a,a1);

for v, v1, a, a1 being object holds ND_ex_3 (v,v1,a,a1) = (v,v1) --> (a,a1);

registration

let v, v1, a, a1 be object ;

coherence

( ND_ex_3 (v,v1,a,a1) is Function-like & ND_ex_3 (v,v1,a,a1) is Relation-like ) ;

end;
coherence

( ND_ex_3 (v,v1,a,a1) is Function-like & ND_ex_3 (v,v1,a,a1) is Relation-like ) ;

theorem Th51: :: NOMIN_1:51

for a, a1, v, v1 being object

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

proof end;

theorem Th52: :: NOMIN_1:52

for a, a1, v, v1 being object

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;

let v, v1 be Element of V;

let a, a1 be Element of A;

:: original: ND_ex_3

redefine func ND_ex_3 (v,v1,a,a1) -> NonatomicND of V,A;

coherence

ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

end;
let v, v1 be Element of V;

let a, a1 be Element of A;

:: original: ND_ex_3

redefine func ND_ex_3 (v,v1,a,a1) -> NonatomicND of V,A;

coherence

ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:53

for a, a1, v, v1 being object

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) is TypeSCNominativeData of V,A

for V, A being set st {v,v1} c= V & {a,a1} c= A holds

ND_ex_3 (v,v1,a,a1) is TypeSCNominativeData of V,A

proof end;

:: deftheorem defines ND_ex_4 NOMIN_1:def 11 :

for v, v1, v2, a, a1 being object holds ND_ex_4 (v,v1,v2,a,a1) = (v,v1) --> (a,(v2 .--> a1));

for v, v1, v2, a, a1 being object holds ND_ex_4 (v,v1,v2,a,a1) = (v,v1) --> (a,(v2 .--> a1));

registration

let v, v1, v2, a, a1 be object ;

coherence

( ND_ex_4 (v,v1,v2,a,a1) is Function-like & ND_ex_4 (v,v1,v2,a,a1) is Relation-like ) ;

end;
coherence

( ND_ex_4 (v,v1,v2,a,a1) is Function-like & ND_ex_4 (v,v1,v2,a,a1) is Relation-like ) ;

theorem Th54: :: NOMIN_1:54

for a, a1, v, v1, v2 being object

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

proof end;

theorem Th55: :: NOMIN_1:55

for a, a1, v, v1, v2 being object

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;

let v, v1, v2 be Element of V;

let a, a1 be Element of A;

:: original: ND_ex_4

redefine func ND_ex_4 (v,v1,v2,a,a1) -> NonatomicND of V,A;

coherence

ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

end;
let v, v1, v2 be Element of V;

let a, a1 be Element of A;

:: original: ND_ex_4

redefine func ND_ex_4 (v,v1,v2,a,a1) -> NonatomicND of V,A;

coherence

ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:56

for a, a1, v, v1, v2 being object

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) is TypeSCNominativeData of V,A

for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) is TypeSCNominativeData of V,A

proof end;

definition

let V, A be set ;

let v be object ;

let D be NonatomicND of V,A;

assume A1: v in dom D ;

coherence

D . v is TypeSCNominativeData of V,A

end;
let v be object ;

let D be NonatomicND of V,A;

assume A1: v in dom D ;

coherence

D . v is TypeSCNominativeData of V,A

proof end;

:: deftheorem Def12 defines denaming NOMIN_1:def 12 :

for V, A being set

for v being object

for D being NonatomicND of V,A st v in dom D holds

denaming (v,D) = D . v;

for V, A being set

for v being object

for D being NonatomicND of V,A st v in dom D holds

denaming (v,D) = D . v;

definition

let V, A be set ;

let v, D be object ;

assume A1: D is TypeSCNominativeData of V,A ;

assume A2: v in V ;

coherence

v .--> D is NonatomicND of V,A

end;
let v, D be object ;

assume A1: D is TypeSCNominativeData of V,A ;

assume A2: v in V ;

coherence

v .--> D is NonatomicND of V,A

proof end;

:: deftheorem Def13 defines naming NOMIN_1:def 13 :

for V, A being set

for v, D being object st D is TypeSCNominativeData of V,A & v in V holds

naming (V,A,v,D) = v .--> D;

for V, A being set

for v, D being object st D is TypeSCNominativeData of V,A & v in V holds

naming (V,A,v,D) = v .--> D;

definition

let V, A be set ;

let a be object ;

let f be V -valued FinSequence;

assume A1: len f > 0 ;

ex b_{1} being FinSequence st

( len b_{1} = len f & b_{1} . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = naming (V,A,(f . ((len f) - n)),(b_{1} . n)) ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = len f & b_{1} . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = naming (V,A,(f . ((len f) - n)),(b_{1} . n)) ) & len b_{2} = len f & b_{2} . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b_{2} holds

b_{2} . (n + 1) = naming (V,A,(f . ((len f) - n)),(b_{2} . n)) ) holds

b_{1} = b_{2}

end;
let a be object ;

let f be V -valued FinSequence;

assume A1: len f > 0 ;

func namingSeq (V,A,f,a) -> FinSequence means :Def14: :: NOMIN_1:def 14

( len it = len f & it . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len it holds

it . (n + 1) = naming (V,A,(f . ((len f) - n)),(it . n)) ) );

existence ( len it = len f & it . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len it holds

it . (n + 1) = naming (V,A,(f . ((len f) - n)),(it . n)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines namingSeq NOMIN_1:def 14 :

for V, A being set

for a being object

for f being b_{1} -valued FinSequence st len f > 0 holds

for b_{5} being FinSequence holds

( b_{5} = namingSeq (V,A,f,a) iff ( len b_{5} = len f & b_{5} . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b_{5} holds

b_{5} . (n + 1) = naming (V,A,(f . ((len f) - n)),(b_{5} . n)) ) ) );

for V, A being set

for a being object

for f being b

for b

( b

b

theorem Th58: :: NOMIN_1:58

for a being object

for V, A being set

for n being Nat

for f being b_{2} -valued FinSequence st 1 <= n & n <= len f holds

(namingSeq (V,A,f,a)) . n is NonatomicND of V,A

for V, A being set

for n being Nat

for f being b

(namingSeq (V,A,f,a)) . n is NonatomicND of V,A

proof end;

definition

let V, A be set ;

let f be V -valued FinSequence;

let a be object ;

(namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a))) is set ;

end;
let f be V -valued FinSequence;

let a be object ;

func naming (V,A,f,a) -> set equals :: NOMIN_1:def 15

(namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

coherence (namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

(namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a))) is set ;

:: deftheorem defines naming NOMIN_1:def 15 :

for V, A being set

for f being b_{1} -valued FinSequence

for a being object holds naming (V,A,f,a) = (namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

for V, A being set

for f being b

for a being object holds naming (V,A,f,a) = (namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

theorem :: NOMIN_1:59

for a being object

for V, A being set

for f being b_{2} -valued FinSequence st len f > 0 holds

naming (V,A,f,a) is NonatomicND of V,A

for V, A being set

for f being b

naming (V,A,f,a) is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:60

for a being object

for A being set

for V being non empty set

for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)

for A being set

for V being non empty set

for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)

proof end;

theorem :: NOMIN_1:61

for a being object

for A being set

for V being non empty set

for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds

naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)

for A being set

for V being non empty set

for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds

naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)

proof end;

theorem :: NOMIN_1:62

for v being object

for V, A being set

for D being TypeSCNominativeData of V,A st v in V holds

denaming (v,(naming (V,A,v,D))) = D

for V, A being set

for D being TypeSCNominativeData of V,A st v in V holds

denaming (v,(naming (V,A,v,D))) = D

proof end;

theorem :: NOMIN_1:63

for v being object

for V, A being set

for D being NonatomicND of V,A st v in dom D holds

naming (V,A,v,(denaming (v,D))) = v .--> (D . v)

for V, A being set

for D being NonatomicND of V,A st v in dom D holds

naming (V,A,v,(denaming (v,D))) = v .--> (D . v)

proof end;

definition

let V, A be set ;

let d1, d2 be object ;

assume that

A1: d1 is TypeSCNominativeData of V,A and

A2: d2 is TypeSCNominativeData of V,A ;

( ( not d1 in A & not d2 in A implies ex b_{1} being TypeSCNominativeData of V,A ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & b_{1} = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b_{1} being TypeSCNominativeData of V,A st b_{1} = d2 ) )

for b_{1}, b_{2} being TypeSCNominativeData of V,A holds

( ( not d1 in A & not d2 in A & ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & b_{1} = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) & ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & b_{2} = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) implies b_{1} = b_{2} ) & ( ( d1 in A or d2 in A ) & b_{1} = d2 & b_{2} = d2 implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being TypeSCNominativeData of V,A holds verum
;

end;
let d1, d2 be object ;

assume that

A1: d1 is TypeSCNominativeData of V,A and

A2: d2 is TypeSCNominativeData of V,A ;

func global_overlapping (V,A,d1,d2) -> TypeSCNominativeData of V,A means :Def16: :: NOMIN_1:def 16

ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & it = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) if ( not d1 in A & not d2 in A )

otherwise it = d2;

existence ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & it = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) if ( not d1 in A & not d2 in A )

otherwise it = d2;

( ( not d1 in A & not d2 in A implies ex b

( f1 = d1 & f2 = d2 & b

proof end;

uniqueness for b

( ( not d1 in A & not d2 in A & ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & b

( f1 = d1 & f2 = d2 & b

consistency

for b

:: deftheorem Def16 defines global_overlapping NOMIN_1:def 16 :

for V, A being set

for d1, d2 being object st d1 is TypeSCNominativeData of V,A & d2 is TypeSCNominativeData of V,A holds

for b_{5} being TypeSCNominativeData of V,A holds

( ( not d1 in A & not d2 in A implies ( b_{5} = global_overlapping (V,A,d1,d2) iff ex f1, f2 being Function st

( f1 = d1 & f2 = d2 & b_{5} = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) ) & ( ( d1 in A or d2 in A ) implies ( b_{5} = global_overlapping (V,A,d1,d2) iff b_{5} = d2 ) ) );

for V, A being set

for d1, d2 being object st d1 is TypeSCNominativeData of V,A & d2 is TypeSCNominativeData of V,A holds

for b

( ( not d1 in A & not d2 in A implies ( b

( f1 = d1 & f2 = d2 & b

definition

let V, A be set ;

let d1, d2, v be object ;

global_overlapping (V,A,d1,(naming (V,A,v,d2))) is TypeSCNominativeData of V,A ;

end;
let d1, d2, v be object ;

func local_overlapping (V,A,d1,d2,v) -> TypeSCNominativeData of V,A equals :: NOMIN_1:def 17

global_overlapping (V,A,d1,(naming (V,A,v,d2)));

coherence global_overlapping (V,A,d1,(naming (V,A,v,d2)));

global_overlapping (V,A,d1,(naming (V,A,v,d2))) is TypeSCNominativeData of V,A ;

:: deftheorem defines local_overlapping NOMIN_1:def 17 :

for V, A being set

for d1, d2, v being object holds local_overlapping (V,A,d1,d2,v) = global_overlapping (V,A,d1,(naming (V,A,v,d2)));

for V, A being set

for d1, d2, v being object holds local_overlapping (V,A,d1,d2,v) = global_overlapping (V,A,d1,(naming (V,A,v,d2)));

theorem Th64: :: NOMIN_1:64

for V, A being set

for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A holds

global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))

for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A holds

global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))

proof end;

theorem Th65: :: NOMIN_1:65

for V, A being set

for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A & dom D1 c= dom D2 holds

global_overlapping (V,A,D1,D2) = D2

for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A & dom D1 c= dom D2 holds

global_overlapping (V,A,D1,D2) = D2

proof end;

theorem :: NOMIN_1:66

for V, A being set

for D being NonatomicND of V,A st not D in A holds

global_overlapping (V,A,D,D) = D

for D being NonatomicND of V,A st not D in A holds

global_overlapping (V,A,D,D) = D

proof end;

theorem :: NOMIN_1:67

for a1, a2, v being object

for V, A being set st v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds

global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

for V, A being set st v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds

global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

proof end;

theorem Th68: :: NOMIN_1:68

for a1, a2, v1, v2 being object

for V, A being set st {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds

global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)

for V, A being set st {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds

global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)

proof end;

theorem :: NOMIN_1:69

for a1, a2, v, v1, v2 being object

for V, A being set st {v,v1,v2} c= V & v <> v1 & a2 in A & not v1 .--> a1 in A & not v .--> (v2 .--> a2) in A & a1 is TypeSCNominativeData of V,A holds

local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1)

for V, A being set st {v,v1,v2} c= V & v <> v1 & a2 in A & not v1 .--> a1 in A & not v .--> (v2 .--> a2) in A & a1 is TypeSCNominativeData of V,A holds

local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1)

proof end;

definition

let V, A be set ;

let v be object ;

set Dom = { d where d is NonatomicND of V,A : v in dom d } ;

ex b_{1} being PartFunc of (ND (V,A)),(ND (V,A)) st

( dom b_{1} = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b_{1} holds

b_{1} . D = denaming (v,D) ) )

for b_{1}, b_{2} being PartFunc of (ND (V,A)),(ND (V,A)) st dom b_{1} = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b_{1} holds

b_{1} . D = denaming (v,D) ) & dom b_{2} = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b_{2} holds

b_{2} . D = denaming (v,D) ) holds

b_{1} = b_{2}

end;
let v be object ;

set Dom = { d where d is NonatomicND of V,A : v in dom d } ;

func denaming (V,A,v) -> PartFunc of (ND (V,A)),(ND (V,A)) means :: NOMIN_1:def 18

( dom it = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom it holds

it . D = denaming (v,D) ) );

existence ( dom it = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom it holds

it . D = denaming (v,D) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines denaming NOMIN_1:def 18 :

for V, A being set

for v being object

for b_{4} being PartFunc of (ND (V,A)),(ND (V,A)) holds

( b_{4} = denaming (V,A,v) iff ( dom b_{4} = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b_{4} holds

b_{4} . D = denaming (v,D) ) ) );

for V, A being set

for v being object

for b

( b

b

definition

let V, A be set ;

let v be object ;

ex b_{1} being Function of (ND (V,A)),(ND (V,A)) st

for D being TypeSCNominativeData of V,A holds b_{1} . D = naming (V,A,v,D)

for b_{1}, b_{2} being Function of (ND (V,A)),(ND (V,A)) st ( for D being TypeSCNominativeData of V,A holds b_{1} . D = naming (V,A,v,D) ) & ( for D being TypeSCNominativeData of V,A holds b_{2} . D = naming (V,A,v,D) ) holds

b_{1} = b_{2}

end;
let v be object ;

func naming (V,A,v) -> Function of (ND (V,A)),(ND (V,A)) means :: NOMIN_1:def 19

for D being TypeSCNominativeData of V,A holds it . D = naming (V,A,v,D);

existence for D being TypeSCNominativeData of V,A holds it . D = naming (V,A,v,D);

ex b

for D being TypeSCNominativeData of V,A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines naming NOMIN_1:def 19 :

for V, A being set

for v being object

for b_{4} being Function of (ND (V,A)),(ND (V,A)) holds

( b_{4} = naming (V,A,v) iff for D being TypeSCNominativeData of V,A holds b_{4} . D = naming (V,A,v,D) );

for V, A being set

for v being object

for b

( b

definition

let V, A be set ;

let v be object ;

ex b_{1} being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st

( dom b_{1} = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b_{1} . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) )

for b_{1}, b_{2} being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st dom b_{1} = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b_{1} . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) & dom b_{2} = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b_{2} . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) holds

b_{1} = b_{2}

end;
let v be object ;

func local_overlapping (V,A,v) -> PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) means :: NOMIN_1:def 20

( dom it = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

it . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) );

existence ( dom it = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

it . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) );

ex b

( dom b

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b

proof end;

uniqueness for b

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b

b

proof end;

:: deftheorem defines local_overlapping NOMIN_1:def 20 :

for V, A being set

for v being object

for b_{4} being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) holds

( b_{4} = local_overlapping (V,A,v) iff ( dom b_{4} = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b_{4} . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) ) );

for V, A being set

for v being object

for b

( b

for d2 being object st not d1 in A & d2 in ND (V,A) holds

b