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

::

:: Received June 29, 2018

:: Copyright (c) 2018-2021 Association of Mizar Users

registration
end;

registration

let V be set ;

ex b_{1} being FinSequence st

( b_{1} is one-to-one & b_{1} is V -valued )

end;
cluster Relation-like NAT -defined V -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

registration

let V, A be set ;

coherence

not NDSS (V,A) is with_non-empty_elements by NOMIN_1:6;

coherence

not ND (V,A) is with_non-empty_elements by NOMIN_1:38;

end;
coherence

not NDSS (V,A) is with_non-empty_elements by NOMIN_1:6;

coherence

not ND (V,A) is with_non-empty_elements by NOMIN_1:38;

theorem Th5: :: NOMIN_2:5

for v being object

for V, A being set

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

{[v,d]} is NonatomicND of V,A

for V, A being set

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

{[v,d]} is NonatomicND of V,A

proof end;

theorem Th6: :: NOMIN_2:6

for V, A being set

for D being finite Function st dom D c= V & rng D c= ND (V,A) holds

D is NonatomicND of V,A

for D being finite Function st dom D c= V & rng D c= ND (V,A) holds

D is NonatomicND of V,A

proof end;

theorem :: NOMIN_2:7

for V, A being set

for d1, d2 being TypeSCNominativeData of V,A holds d2 c= global_overlapping (V,A,d1,d2)

for d1, d2 being TypeSCNominativeData of V,A holds d2 c= global_overlapping (V,A,d1,d2)

proof end;

theorem :: NOMIN_2:8

theorem Th9: :: NOMIN_2:9

for V, A being set

for d1, d2 being NonatomicND of V,A holds global_overlapping (V,A,d1,d2) is NonatomicND of V,A

for d1, d2 being NonatomicND of V,A holds global_overlapping (V,A,d1,d2) is NonatomicND of V,A

proof end;

registration

let V, A be set ;

let d1, d2 be NonatomicND of V,A;

coherence

( global_overlapping (V,A,d1,d2) is Function-like & global_overlapping (V,A,d1,d2) is Relation-like ) by Th9;

end;
let d1, d2 be NonatomicND of V,A;

coherence

( global_overlapping (V,A,d1,d2) is Function-like & global_overlapping (V,A,d1,d2) is Relation-like ) by Th9;

registration

let V, A be set ;

let v be object ;

let d1 be NonatomicND of V,A;

let d2 be object ;

coherence

( local_overlapping (V,A,d1,d2,v) is Function-like & local_overlapping (V,A,d1,d2,v) is Relation-like ) ;

end;
let v be object ;

let d1 be NonatomicND of V,A;

let d2 be object ;

coherence

( local_overlapping (V,A,d1,d2,v) is Function-like & local_overlapping (V,A,d1,d2,v) is Relation-like ) ;

theorem Th10: :: NOMIN_2:10

for v being object

for V, A being set st v in V holds

for d1, d2 being TypeSCNominativeData of V,A

for L being Function st L = local_overlapping (V,A,d1,d2,v) holds

L . v = d2

for V, A being set st v in V holds

for d1, d2 being TypeSCNominativeData of V,A

for L being Function st L = local_overlapping (V,A,d1,d2,v) holds

L . v = d2

proof end;

theorem :: NOMIN_2:11

for v being object

for V, A being set

for d being TypeSCNominativeData of V,A

for d1 being NonatomicND of V,A

for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds

(local_overlapping (V,A,d1,d,z)) . z = d1 . v

for V, A being set

for d being TypeSCNominativeData of V,A

for d1 being NonatomicND of V,A

for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds

(local_overlapping (V,A,d1,d,z)) . z = d1 . v

proof end;

theorem :: NOMIN_2:12

for v, v1 being object

for V, A being set st v in V & v <> v1 holds

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1

for V, A being set st v in V & v <> v1 holds

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1

proof end;

theorem Th12: :: NOMIN_2:13

for v being object

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & not v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & not v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

proof end;

theorem Th13: :: NOMIN_2:14

for v being object

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = dom d1

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = dom d1

proof end;

theorem Th14: :: NOMIN_2:15

for v being object

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

for V, A being set

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A st v in V & not d1 in A & not naming (V,A,v,d2) in A holds

dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

proof end;

definition
end;

theorem Th15: :: NOMIN_2:16

for V, A being set

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_or (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) }

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_or (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) }

proof end;

theorem :: NOMIN_2:17

for V, A being set

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_and (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_and (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }

proof end;

theorem :: NOMIN_2:18

for V, A being set

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }

for p, q being SCPartialNominativePredicate of V,A holds dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }

proof end;

definition

let V, A be set ;

let v be object ;

defpred S_{1}[ object , Function] means ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,$1,d1,v) in dom $2 & $2 . (local_overlapping (V,A,$1,d1,v)) = TRUE );

defpred S_{2}[ object , Function] means for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,$1,d1,v) in dom $2 & $2 . (local_overlapping (V,A,$1,d1,v)) = FALSE );

deffunc H_{1}( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( S_{1}[d,$1] or S_{2}[d,$1] ) } ;

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

for p being SCPartialNominativePredicate of V,A holds

( dom (b_{1} . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b_{1} . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b_{1} . p) . d = FALSE ) ) ) )

for b_{1}, b_{2} being Function of (Pr (ND (V,A))),(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A holds

( dom (b_{1} . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b_{1} . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b_{1} . p) . d = FALSE ) ) ) ) ) & ( for p being SCPartialNominativePredicate of V,A holds

( dom (b_{2} . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b_{2} . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b_{2} . p) . d = FALSE ) ) ) ) ) holds

b_{1} = b_{2}

end;
let v be object ;

defpred S

( local_overlapping (V,A,$1,d1,v) in dom $2 & $2 . (local_overlapping (V,A,$1,d1,v)) = TRUE );

defpred S

( local_overlapping (V,A,$1,d1,v) in dom $2 & $2 . (local_overlapping (V,A,$1,d1,v)) = FALSE );

deffunc H

func SCexists (V,A,v) -> Function of (Pr (ND (V,A))),(Pr (ND (V,A))) means :Def1: :: NOMIN_2:def 1

for p being SCPartialNominativePredicate of V,A holds

( dom (it . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (it . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (it . p) . d = FALSE ) ) ) );

existence for p being SCPartialNominativePredicate of V,A holds

( dom (it . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (it . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (it . p) . d = FALSE ) ) ) );

ex b

for p being SCPartialNominativePredicate of V,A holds

( dom (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b

proof end;

uniqueness for b

( dom (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b

( dom (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b

b

proof end;

:: deftheorem Def1 defines SCexists NOMIN_2:def 1 :

for V, A being set

for v being object

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

( b_{4} = SCexists (V,A,v) iff for p being SCPartialNominativePredicate of V,A holds

( dom (b_{4} . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b_{4} . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b_{4} . p) . d = FALSE ) ) ) ) );

for V, A being set

for v being object

for b

( b

( dom (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds

( ( ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b

( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b

definition

let V, A be set ;

let v be object ;

let p be SCPartialNominativePredicate of V,A;

(SCexists (V,A,v)) . p is SCPartialNominativePredicate of V,A

end;
let v be object ;

let p be SCPartialNominativePredicate of V,A;

func SC_exists (p,v) -> SCPartialNominativePredicate of V,A equals :: NOMIN_2:def 2

(SCexists (V,A,v)) . p;

coherence (SCexists (V,A,v)) . p;

(SCexists (V,A,v)) . p is SCPartialNominativePredicate of V,A

proof end;

:: deftheorem defines SC_exists NOMIN_2:def 2 :

for V, A being set

for v being object

for p being SCPartialNominativePredicate of V,A holds SC_exists (p,v) = (SCexists (V,A,v)) . p;

for V, A being set

for v being object

for p being SCPartialNominativePredicate of V,A holds SC_exists (p,v) = (SCexists (V,A,v)) . p;

theorem Th18: :: NOMIN_2:19

for v, x being object

for V, A being set

for p being SCPartialNominativePredicate of V,A holds

( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )

for V, A being set

for p being SCPartialNominativePredicate of V,A holds

( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st

( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds

( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )

proof end;

theorem :: NOMIN_2:20

for v being object

for V, A being set holds SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))

for V, A being set holds SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))

proof end;

:: Distributivity law

theorem :: NOMIN_2:21

for v being object

for V, A being set

for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))

for V, A being set

for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))

proof end;

:: deftheorem Def3 defines in_doms NOMIN_2:def 3 :

for F being Function-yielding Function

for d being object holds

( d in_doms F iff for x being object st x in dom F holds

d in dom (F . x) );

for F being Function-yielding Function

for d being object holds

( d in_doms F iff for x being object st x in dom F holds

d in dom (F . x) );

definition

let g be Function-yielding Function;

let X be Function;

let d be object ;

ex b_{1} being Function st

( dom b_{1} = dom X & ( for x being object st x in dom X holds

b_{1} . x = [(X . x),((g . x) . d)] ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom X & ( for x being object st x in dom X holds

b_{1} . x = [(X . x),((g . x) . d)] ) & dom b_{2} = dom X & ( for x being object st x in dom X holds

b_{2} . x = [(X . x),((g . x) . d)] ) holds

b_{1} = b_{2}

end;
let X be Function;

let d be object ;

func NDdataSeq (g,X,d) -> Function means :Def4: :: NOMIN_2:def 4

( dom it = dom X & ( for x being object st x in dom X holds

it . x = [(X . x),((g . x) . d)] ) );

existence ( dom it = dom X & ( for x being object st x in dom X holds

it . x = [(X . x),((g . x) . d)] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines NDdataSeq NOMIN_2:def 4 :

for g being Function-yielding Function

for X being Function

for d being object

for b_{4} being Function holds

( b_{4} = NDdataSeq (g,X,d) iff ( dom b_{4} = dom X & ( for x being object st x in dom X holds

b_{4} . x = [(X . x),((g . x) . d)] ) ) );

for g being Function-yielding Function

for X being Function

for d being object

for b

( b

b

registration

let g be Function-yielding Function;

let X be finite Function;

let d be object ;

coherence

NDdataSeq (g,X,d) is finite

end;
let X be finite Function;

let d be object ;

coherence

NDdataSeq (g,X,d) is finite

proof end;

registration

let g be Function-yielding Function;

let X be FinSequence;

let d be object ;

coherence

NDdataSeq (g,X,d) is FinSequence-like

end;
let X be FinSequence;

let d be object ;

coherence

NDdataSeq (g,X,d) is FinSequence-like

proof end;

definition

let g be Function-yielding Function;

let X be Function;

let d be object ;

coherence

rng (NDdataSeq (g,X,d)) is set ;

end;
let X be Function;

let d be object ;

coherence

rng (NDdataSeq (g,X,d)) is set ;

:: deftheorem defines NDentry NOMIN_2:def 5 :

for g being Function-yielding Function

for X being Function

for d being object holds NDentry (g,X,d) = rng (NDdataSeq (g,X,d));

for g being Function-yielding Function

for X being Function

for d being object holds NDentry (g,X,d) = rng (NDdataSeq (g,X,d));

theorem Th22: :: NOMIN_2:23

for f, g being Function

for a, b, d being object holds NDentry (<*f,g*>,<*a,b*>,d) = {[a,(f . d)],[b,(g . d)]}

for a, b, d being object holds NDentry (<*f,g*>,<*a,b*>,d) = {[a,(f . d)],[b,(g . d)]}

proof end;

theorem Th23: :: NOMIN_2:24

for f, g, h being Function

for a, b, c, d being object holds NDentry (<*f,g,h*>,<*a,b,c*>,d) = {[a,(f . d)],[b,(g . d)],[c,(h . d)]}

for a, b, c, d being object holds NDentry (<*f,g,h*>,<*a,b,c*>,d) = {[a,(f . d)],[b,(g . d)],[c,(h . d)]}

proof end;

registration

let g be Function-yielding Function;

let X be Function;

let d be object ;

coherence

NDentry (g,X,d) is Relation-like

end;
let X be Function;

let d be object ;

coherence

NDentry (g,X,d) is Relation-like

proof end;

registration

let g be Function-yielding Function;

let X be one-to-one Function;

let d be object ;

coherence

NDentry (g,X,d) is Function-like

end;
let X be one-to-one Function;

let d be object ;

coherence

NDentry (g,X,d) is Function-like

proof end;

registration

let g be Function-yielding Function;

let X be finite Function;

let d be object ;

coherence

NDentry (g,X,d) is finite ;

end;
let X be finite Function;

let d be object ;

coherence

NDentry (g,X,d) is finite ;

theorem Th24: :: NOMIN_2:25

for g being Function-yielding Function

for X being Function

for d being object holds dom (NDentry (g,X,d)) = rng X

for X being Function

for d being object holds dom (NDentry (g,X,d)) = rng X

proof end;

definition
end;

theorem Th25: :: NOMIN_2:26

for v being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)

proof end;

theorem Th26: :: NOMIN_2:27

for a being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A st a in V & d in dom f holds

NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A st a in V & d in dom f holds

NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))

proof end;

theorem :: NOMIN_2:28

for a being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A st a in V & d in dom f holds

NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A

for V, A being set

for d being TypeSCNominativeData of V,A

for f being SCBinominativeFunction of V,A st a in V & d in dom f holds

NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A

proof end;

theorem :: NOMIN_2:29

for a, b being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g being SCBinominativeFunction of V,A st {a,b} c= V & a <> b & d in dom f & d in dom g holds

NDentry (<*f,g*>,<*a,b*>,d) is NonatomicND of V,A

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g being SCBinominativeFunction of V,A st {a,b} c= V & a <> b & d in dom f & d in dom g holds

NDentry (<*f,g*>,<*a,b*>,d) is NonatomicND of V,A

proof end;

theorem :: NOMIN_2:30

for a, b, c being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds

NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds

NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A

proof end;

definition

let V, A be set ;

let f be FinSequence;

end;
let f be FinSequence;

attr f is V,A -FPrg-yielding means :Def6: :: NOMIN_2:def 6

for n being Nat st 1 <= n & n <= len f holds

f . n is SCBinominativeFunction of V,A;

for n being Nat st 1 <= n & n <= len f holds

f . n is SCBinominativeFunction of V,A;

:: deftheorem Def6 defines -FPrg-yielding NOMIN_2:def 6 :

for V, A being set

for f being FinSequence holds

( f is V,A -FPrg-yielding iff for n being Nat st 1 <= n & n <= len f holds

f . n is SCBinominativeFunction of V,A );

for V, A being set

for f being FinSequence holds

( f is V,A -FPrg-yielding iff for n being Nat st 1 <= n & n <= len f holds

f . n is SCBinominativeFunction of V,A );

registration

let V, A be set ;

let f be SCBinominativeFunction of V,A;

coherence

<*f*> is V,A -FPrg-yielding

end;
let f be SCBinominativeFunction of V,A;

coherence

<*f*> is V,A -FPrg-yielding

proof end;

registration

let V, A be set ;

let f, g be SCBinominativeFunction of V,A;

coherence

<*f,g*> is V,A -FPrg-yielding

end;
let f, g be SCBinominativeFunction of V,A;

coherence

<*f,g*> is V,A -FPrg-yielding

proof end;

registration

let V, A be set ;

let f, g, h be SCBinominativeFunction of V,A;

coherence

<*f,g,h*> is V,A -FPrg-yielding

end;
let f, g, h be SCBinominativeFunction of V,A;

coherence

<*f,g,h*> is V,A -FPrg-yielding

proof end;

registration

let V, A be set ;

let n be Nat;

ex b_{1} being FinSequence st

( b_{1} is V,A -FPrg-yielding & b_{1} is n -element )

end;
let n be Nat;

cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V,A -FPrg-yielding for set ;

existence ex b

( b

proof end;

registration

let V, A be set ;

let x be object ;

let g be V,A -FPrg-yielding FinSequence;

coherence

( g . x is Function-like & g . x is Relation-like )

end;
let x be object ;

let g be V,A -FPrg-yielding FinSequence;

coherence

( g . x is Function-like & g . x is Relation-like )

proof end;

registration

let V, A be set ;

for b_{1} being FinSequence st b_{1} is V,A -FPrg-yielding holds

b_{1} is Function-yielding
;

end;
cluster Relation-like Function-like FinSequence-like V,A -FPrg-yielding -> Function-yielding for set ;

coherence for b

b

theorem Th30: :: NOMIN_2:31

for V, A being set

for d being TypeSCNominativeData of V,A

for g being b_{1},b_{2} -FPrg-yielding FinSequence

for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds

rng (NDentry (g,X,d)) c= ND (V,A)

for d being TypeSCNominativeData of V,A

for g being b

for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds

rng (NDentry (g,X,d)) c= ND (V,A)

proof end;

theorem :: NOMIN_2:32

for V, A being set

for d being TypeSCNominativeData of V,A

for g being b_{1},b_{2} -FPrg-yielding FinSequence

for X being b_{1} -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds

NDentry (g,X,d) is NonatomicND of V,A

for d being TypeSCNominativeData of V,A

for g being b

for X being b

NDentry (g,X,d) is NonatomicND of V,A

proof end;

definition

let V, A be set ;

let v be object ;

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

for f being SCBinominativeFunction of V,A holds

( dom (b_{1} . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b_{1} . f) holds

(b_{1} . f) . d = local_overlapping (V,A,d,(f . d),v) ) )

for b_{1}, b_{2} being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) st ( for f being SCBinominativeFunction of V,A holds

( dom (b_{1} . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b_{1} . f) holds

(b_{1} . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for f being SCBinominativeFunction of V,A holds

( dom (b_{2} . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b_{2} . f) holds

(b_{2} . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) holds

b_{1} = b_{2}

end;
let v be object ;

func SCassignment (V,A,v) -> Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) means :Def7: :: NOMIN_2:def 7

for f being SCBinominativeFunction of V,A holds

( dom (it . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (it . f) holds

(it . f) . d = local_overlapping (V,A,d,(f . d),v) ) );

existence for f being SCBinominativeFunction of V,A holds

( dom (it . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (it . f) holds

(it . f) . d = local_overlapping (V,A,d,(f . d),v) ) );

ex b

for f being SCBinominativeFunction of V,A holds

( dom (b

(b

proof end;

uniqueness for b

( dom (b

(b

( dom (b

(b

b

proof end;

:: deftheorem Def7 defines SCassignment NOMIN_2:def 7 :

for V, A being set

for v being object

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

( b_{4} = SCassignment (V,A,v) iff for f being SCBinominativeFunction of V,A holds

( dom (b_{4} . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b_{4} . f) holds

(b_{4} . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) );

for V, A being set

for v being object

for b

( b

( dom (b

(b

definition

let V, A be set ;

let v be object ;

let f be SCBinominativeFunction of V,A;

(SCassignment (V,A,v)) . f is SCBinominativeFunction of V,A

end;
let v be object ;

let f be SCBinominativeFunction of V,A;

func SC_assignment (f,v) -> SCBinominativeFunction of V,A equals :: NOMIN_2:def 8

(SCassignment (V,A,v)) . f;

coherence (SCassignment (V,A,v)) . f;

(SCassignment (V,A,v)) . f is SCBinominativeFunction of V,A

proof end;

:: deftheorem defines SC_assignment NOMIN_2:def 8 :

for V, A being set

for v being object

for f being SCBinominativeFunction of V,A holds SC_assignment (f,v) = (SCassignment (V,A,v)) . f;

for V, A being set

for v being object

for f being SCBinominativeFunction of V,A holds SC_assignment (f,v) = (SCassignment (V,A,v)) . f;

registration

let V, A be set ;

let f be SCBinominativeFunction of V,A;

let v be object ;

let d be NonatomicND of V,A;

coherence

( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like )

end;
let f be SCBinominativeFunction of V,A;

let v be object ;

let d be NonatomicND of V,A;

coherence

( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like )

proof end;

theorem :: NOMIN_2:33

for v being object

for V, A being set

for f being SCBinominativeFunction of V,A

for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f holds

dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}

for V, A being set

for f being SCBinominativeFunction of V,A

for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f holds

dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}

proof end;

definition

let V, A be set ;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

defpred S_{1}[ object ] means $1 in_doms g;

deffunc H_{1}( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom $1 & S_{1}[d] ) } ;

ex b_{1} being Function of [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))) st

for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (b_{1} . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{1} . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )

for b_{1}, b_{2} being Function of [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (b_{1} . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{1} . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) & ( for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (b_{2} . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{2} . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) holds

b_{1} = b_{2}

end;
let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

defpred S

deffunc H

func SCPsuperpos (g,X) -> Function of [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))) means :Def9: :: NOMIN_2:def 9

for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (it . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

it . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) );

existence for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (it . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

it . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) );

ex b

for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (b

b

proof end;

uniqueness for b

for x being Element of product g holds

( dom (b

b

for x being Element of product g holds

( dom (b

b

b

proof end;

:: deftheorem Def9 defines SCPsuperpos NOMIN_2:def 9 :

for V, A being set

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for X being Function

for b_{5} being Function of [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))) holds

( b_{5} = SCPsuperpos (g,X) iff for p being SCPartialNominativePredicate of V,A

for x being Element of product g holds

( dom (b_{5} . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{5} . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) );

for V, A being set

for g being b

for X being Function

for b

( b

for x being Element of product g holds

( dom (b

b

definition

let V, A be set ;

let p be SCPartialNominativePredicate of V,A;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

let x be Element of product g;

(SCPsuperpos (g,X)) . (p,x) is SCPartialNominativePredicate of V,A

end;
let p be SCPartialNominativePredicate of V,A;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

let x be Element of product g;

func SC_Psuperpos (p,x,X) -> SCPartialNominativePredicate of V,A equals :Def10: :: NOMIN_2:def 10

(SCPsuperpos (g,X)) . (p,x);

coherence (SCPsuperpos (g,X)) . (p,x);

(SCPsuperpos (g,X)) . (p,x) is SCPartialNominativePredicate of V,A

proof end;

:: deftheorem Def10 defines SC_Psuperpos NOMIN_2:def 10 :

for V, A being set

for p being SCPartialNominativePredicate of V,A

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for X being Function

for x being Element of product g holds SC_Psuperpos (p,x,X) = (SCPsuperpos (g,X)) . (p,x);

for V, A being set

for p being SCPartialNominativePredicate of V,A

for g being b

for X being Function

for x being Element of product g holds SC_Psuperpos (p,x,X) = (SCPsuperpos (g,X)) . (p,x);

theorem Th33: :: NOMIN_2:34

for V, A being set

for d being TypeSCNominativeData of V,A

for p being SCPartialNominativePredicate of V,A

for X being Function

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds

( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )

for d being TypeSCNominativeData of V,A

for p being SCPartialNominativePredicate of V,A

for X being Function

for g being b

for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds

( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )

proof end;

definition

let V, A be set ;

let v be object ;

deffunc H_{1}( Function, Function) -> set = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,($2 . d),v) in dom $1 & d in dom $2 ) } ;

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

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (b_{1} . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

b_{1} . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) )

for b_{1}, b_{2} being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (b_{1} . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

b_{1} . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (b_{2} . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

b_{2} . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) holds

b_{1} = b_{2}

end;
let v be object ;

deffunc H

func SCPsuperpos (V,A,v) -> Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) means :Def11: :: NOMIN_2:def 11

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (it . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

it . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) );

existence for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (it . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

it . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) );

ex b

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (b

b

proof end;

uniqueness for b

for f being SCBinominativeFunction of V,A holds

( dom (b

b

for f being SCBinominativeFunction of V,A holds

( dom (b

b

b

proof end;

:: deftheorem Def11 defines SCPsuperpos NOMIN_2:def 11 :

for V, A being set

for v being object

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

( b_{4} = SCPsuperpos (V,A,v) iff for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds

( dom (b_{4} . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds

b_{4} . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) );

for V, A being set

for v being object

for b

( b

for f being SCBinominativeFunction of V,A holds

( dom (b

b

definition

let V, A be set ;

let v be object ;

let p be SCPartialNominativePredicate of V,A;

let f be SCBinominativeFunction of V,A;

(SCPsuperpos (V,A,v)) . (p,f) is SCPartialNominativePredicate of V,A

end;
let v be object ;

let p be SCPartialNominativePredicate of V,A;

let f be SCBinominativeFunction of V,A;

func SC_Psuperpos (p,f,v) -> SCPartialNominativePredicate of V,A equals :: NOMIN_2:def 12

(SCPsuperpos (V,A,v)) . (p,f);

coherence (SCPsuperpos (V,A,v)) . (p,f);

(SCPsuperpos (V,A,v)) . (p,f) is SCPartialNominativePredicate of V,A

proof end;

:: deftheorem defines SC_Psuperpos NOMIN_2:def 12 :

for V, A being set

for v being object

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds SC_Psuperpos (p,f,v) = (SCPsuperpos (V,A,v)) . (p,f);

for V, A being set

for v being object

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds SC_Psuperpos (p,f,v) = (SCPsuperpos (V,A,v)) . (p,f);

theorem Th34: :: NOMIN_2:35

for v being object

for V, A being set

for d being TypeSCNominativeData of V,A

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds

( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )

for V, A being set

for d being TypeSCNominativeData of V,A

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds

( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )

proof end;

theorem :: NOMIN_2:36

for v being object

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A

for x being Element of product <*f*> st v in V & product <*f*> <> {} holds

SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A

for x being Element of product <*f*> st v in V & product <*f*> <> {} holds

SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)

proof end;

definition

let V, A be set ;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

defpred S_{1}[ object ] means $1 in_doms g;

deffunc H_{1}( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom $1 & S_{1}[d] ) } ;

ex b_{1} being Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) st

for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (b_{1} . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{1} . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )

for b_{1}, b_{2} being Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) st ( for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (b_{1} . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{1} . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) & ( for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (b_{2} . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{2} . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) holds

b_{1} = b_{2}

end;
let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

defpred S

deffunc H

func SCFsuperpos (g,X) -> Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) means :Def13: :: NOMIN_2:def 13

for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (it . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

it . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) );

existence for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (it . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

it . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) );

ex b

for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (b

b

proof end;

uniqueness for b

for x being Element of product g holds

( dom (b

b

for x being Element of product g holds

( dom (b

b

b

proof end;

:: deftheorem Def13 defines SCFsuperpos NOMIN_2:def 13 :

for V, A being set

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for X being Function

for b_{5} being Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) holds

( b_{5} = SCFsuperpos (g,X) iff for f being SCBinominativeFunction of V,A

for x being Element of product g holds

( dom (b_{5} . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds

b_{5} . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) );

for V, A being set

for g being b

for X being Function

for b

( b

for x being Element of product g holds

( dom (b

b

definition

let V, A be set ;

let f be SCBinominativeFunction of V,A;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

let x be Element of product g;

(SCFsuperpos (g,X)) . (f,x) is SCBinominativeFunction of V,A

end;
let f be SCBinominativeFunction of V,A;

let g be V,A -FPrg-yielding FinSequence;

assume A1: product g <> {} ;

let X be Function;

let x be Element of product g;

func SC_Fsuperpos (f,x,X) -> SCBinominativeFunction of V,A equals :Def14: :: NOMIN_2:def 14

(SCFsuperpos (g,X)) . (f,x);

coherence (SCFsuperpos (g,X)) . (f,x);

(SCFsuperpos (g,X)) . (f,x) is SCBinominativeFunction of V,A

proof end;

:: deftheorem Def14 defines SC_Fsuperpos NOMIN_2:def 14 :

for V, A being set

for f being SCBinominativeFunction of V,A

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for X being Function

for x being Element of product g holds SC_Fsuperpos (f,x,X) = (SCFsuperpos (g,X)) . (f,x);

for V, A being set

for f being SCBinominativeFunction of V,A

for g being b

for X being Function

for x being Element of product g holds SC_Fsuperpos (f,x,X) = (SCFsuperpos (g,X)) . (f,x);

theorem Th36: :: NOMIN_2:37

for V, A being set

for d being TypeSCNominativeData of V,A

for X being Function

for f being SCBinominativeFunction of V,A

for g being b_{1},b_{2} -FPrg-yielding FinSequence st product g <> {} holds

for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds

( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )

for d being TypeSCNominativeData of V,A

for X being Function

for f being SCBinominativeFunction of V,A

for g being b

for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds

( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )

proof end;

definition

let V, A be set ;

let v be object ;

deffunc H_{1}( Function, Function) -> set = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,($2 . d),v) in dom $1 & d in dom $2 ) } ;

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

for f, g being SCBinominativeFunction of V,A holds

( dom (b_{1} . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

b_{1} . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) )

for b_{1}, b_{2} being Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) st ( for f, g being SCBinominativeFunction of V,A holds

( dom (b_{1} . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

b_{1} . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) ) & ( for f, g being SCBinominativeFunction of V,A holds

( dom (b_{2} . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

b_{2} . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) ) holds

b_{1} = b_{2}

end;
let v be object ;

deffunc H

func SCFsuperpos (V,A,v) -> Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) means :Def15: :: NOMIN_2:def 15

for f, g being SCBinominativeFunction of V,A holds

( dom (it . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

it . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) );

existence for f, g being SCBinominativeFunction of V,A holds

( dom (it . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

it . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) );

ex b

for f, g being SCBinominativeFunction of V,A holds

( dom (b

b

proof end;

uniqueness for b

( dom (b

b

( dom (b

b

b

proof end;

:: deftheorem Def15 defines SCFsuperpos NOMIN_2:def 15 :

for V, A being set

for v being object

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

( b_{4} = SCFsuperpos (V,A,v) iff for f, g being SCBinominativeFunction of V,A holds

( dom (b_{4} . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds

b_{4} . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) );

for V, A being set

for v being object

for b

( b

( dom (b

b

definition

let V, A be set ;

let v be object ;

let f, g be SCBinominativeFunction of V,A;

(SCFsuperpos (V,A,v)) . (f,g) is SCBinominativeFunction of V,A

end;
let v be object ;

let f, g be SCBinominativeFunction of V,A;

func SC_Fsuperpos (f,g,v) -> SCBinominativeFunction of V,A equals :: NOMIN_2:def 16

(SCFsuperpos (V,A,v)) . (f,g);

coherence (SCFsuperpos (V,A,v)) . (f,g);

(SCFsuperpos (V,A,v)) . (f,g) is SCBinominativeFunction of V,A

proof end;

:: deftheorem defines SC_Fsuperpos NOMIN_2:def 16 :

for V, A being set

for v being object

for f, g being SCBinominativeFunction of V,A holds SC_Fsuperpos (f,g,v) = (SCFsuperpos (V,A,v)) . (f,g);

for V, A being set

for v being object

for f, g being SCBinominativeFunction of V,A holds SC_Fsuperpos (f,g,v) = (SCFsuperpos (V,A,v)) . (f,g);

theorem Th37: :: NOMIN_2:38

for v being object

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds

( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )

for V, A being set

for d being TypeSCNominativeData of V,A

for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds

( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )

proof end;

theorem :: NOMIN_2:39

for v being object

for V, A being set

for f, g being SCBinominativeFunction of V,A

for x being Element of product <*g*> st v in V & product <*g*> <> {} holds

SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)

for V, A being set

for f, g being SCBinominativeFunction of V,A

for x being Element of product <*g*> st v in V & product <*g*> <> {} holds

SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)

proof end;

definition

let V, A be set ;

let v be object ;

defpred S_{1}[ object ] means ex d being NonatomicND of V,A st

( d = $1 & denaming (v,d) in (ND (V,A)) \ A );

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b_{1} holds

( ( denaming (v,d) in dom b_{1} implies b_{1} . d = TRUE ) & ( not denaming (v,d) in dom b_{1} implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b_{1} holds

( ( denaming (v,d) in dom b_{1} implies b_{1} . d = TRUE ) & ( not denaming (v,d) in dom b_{1} implies b_{1} . d = FALSE ) ) ) & dom b_{2} = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b_{2} holds

( ( denaming (v,d) in dom b_{2} implies b_{2} . d = TRUE ) & ( not denaming (v,d) in dom b_{2} implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let v be object ;

defpred S

( d = $1 & denaming (v,d) in (ND (V,A)) \ A );

func SC_name_check (V,A,v) -> SCPartialNominativePredicate of V,A means :: NOMIN_2:def 17

( dom it = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom it holds

( ( denaming (v,d) in dom it implies it . d = TRUE ) & ( not denaming (v,d) in dom it implies it . d = FALSE ) ) ) );

existence ( dom it = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom it holds

( ( denaming (v,d) in dom it implies it . d = TRUE ) & ( not denaming (v,d) in dom it implies it . d = FALSE ) ) ) );

ex b

( dom b

( ( denaming (v,d) in dom b

proof end;

uniqueness for b

( ( denaming (v,d) in dom b

( ( denaming (v,d) in dom b

b

proof end;

:: deftheorem defines SC_name_check NOMIN_2:def 17 :

for V, A being set

for v being object

for b_{4} being SCPartialNominativePredicate of V,A holds

( b_{4} = SC_name_check (V,A,v) iff ( dom b_{4} = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b_{4} holds

( ( denaming (v,d) in dom b_{4} implies b_{4} . d = TRUE ) & ( not denaming (v,d) in dom b_{4} implies b_{4} . d = FALSE ) ) ) ) );

for V, A being set

for v being object

for b

( b

( ( denaming (v,d) in dom b