NOMIN_2: On an algorithmic algebra over simple-named complex-valued nominative data

proof end;

end;

theorem Th2: :: NOMIN_2:2

for a, b, c, d, e, f being object holds dom {[a,b],[c,d],[e,f]} = {a,c,e}

proof end;

theorem Th3: :: NOMIN_2:3

for a, b, c, d, e, f being object holds rng {[a,b],[c,d],[e,f]} = {b,d,f}

proof end;

registration

let V be set ;

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

proof end;

end;

theorem Th4: :: NOMIN_2:4

for a, b, c being object holds dom <*a,b,c*> = {1,2,3}

proof end;

registration

let V, A be set ;

cluster NDSS (V,A) -> non with_non-empty_elements ;

coherence by NOMIN_1:6;

cluster ND (V,A) -> non with_non-empty_elements ;

coherence by NOMIN_1:38;

end;

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

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

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)

proof end;

theorem :: NOMIN_2:8

for V, A being set
for d being NonatomicND of V,A holds d is TypeSCNominativeData of V,A ;

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

proof end;

registration

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

cluster global_overlapping (V,A,d1,d2) -> Relation-like Function-like ;

coherence by Th9;

end;

registration

let V, A be set ;
let v be object ;
let d1 be NonatomicND of V,A;
let d2 be object ;

cluster local_overlapping (V,A,d1,d2,v) -> Relation-like Function-like ;

end;

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

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

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

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)

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

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)

proof end;

definition

let V, A be set ;
mode SCPartialNominativePredicate of V,A is PartialPredicate of (ND (V,A));

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 ) ) }

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 ) ) }

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 ) ) }

proof end;

definition

let V, A be set ;
let v be object ;
defpred S₁[ 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₂[ 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₁( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( S₁[d,$1] or S₂[d,$1] ) } ;

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 ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def1 defines SCexists NOMIN_2:def 1 :

definition

let V, A be set ;
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;

proof end;

end;

:: deftheorem defines SC_exists NOMIN_2:def 2 :

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 ) )

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))

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)))

proof end;

definition

let F be Function-yielding Function;
let d be object ;

pred d in_doms F means :Def3: :: NOMIN_2:def 3
for x being object st x in dom F holds
d in dom (F . x);

end;

:: deftheorem Def3 defines in_doms NOMIN_2:def 3 :

definition

let g be Function-yielding Function;
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)] ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines NDdataSeq NOMIN_2:def 4 :

registration

let g be Function-yielding Function;
let X be finite Function;
let d be object ;

cluster NDdataSeq (g,X,d) -> finite ;

proof end;

end;

registration

let g be Function-yielding Function;
let X be FinSequence;
let d be object ;

cluster NDdataSeq (g,X,d) -> FinSequence-like ;

proof end;

end;

definition

let g be Function-yielding Function;
let X be Function;
let d be object ;

func NDentry (g,X,d) -> set equals :: NOMIN_2:def 5
rng (NDdataSeq (g,X,d));

end;

:: deftheorem defines NDentry NOMIN_2:def 5 :

theorem :: NOMIN_2:22

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

proof end;

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)]}

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)]}

proof end;

registration

let g be Function-yielding Function;
let X be Function;
let d be object ;

cluster NDentry (g,X,d) -> Relation-like ;

proof end;

end;

registration

let g be Function-yielding Function;
let X be one-to-one Function;
let d be object ;

cluster NDentry (g,X,d) -> Function-like ;

proof end;

end;

registration

let g be Function-yielding Function;
let X be finite Function;
let d be object ;

cluster NDentry (g,X,d) -> finite ;

end;

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

proof end;

definition

let V, A be set ;
mode SCBinominativeFunction of V,A is PartFunc of (ND (V,A)),(ND (V,A));

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)

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))

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

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

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

proof end;

definition

let V, A be set ;
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;

end;

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

registration

let V, A be set ;
let f be SCBinominativeFunction of V,A;

cluster <*f*> -> V,A -FPrg-yielding ;

proof end;

end;

registration

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

cluster <*f,g*> -> V,A -FPrg-yielding ;

proof end;

end;

registration

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

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

proof end;

end;

registration

let V, A be set ;
let n be Nat;

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

proof end;

end;

registration

let V, A be set ;
let x be object ;
let g be V,A -FPrg-yielding FinSequence;

cluster g . x -> Relation-like Function-like ;

proof end;

end;

registration

let V, A be set ;

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

end;

theorem Th30: :: NOMIN_2:31

for V, A being set
for d being TypeSCNominativeData of V,A
for g being b₁,b₂ -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)

proof end;

theorem :: NOMIN_2:32

for V, A being set
for d being TypeSCNominativeData of V,A
for g being b₁,b₂ -FPrg-yielding FinSequence
for X being b₁ -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A

proof end;

Assignment composition

definition

let V, A be set ;
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) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines SCassignment NOMIN_2:def 7 :

Assignment composition

definition

let V, A be set ;
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;

proof end;

end;

:: deftheorem defines SC_assignment NOMIN_2:def 8 :

registration

let V, A be set ;
let f be SCBinominativeFunction of V,A;
let v be object ;
let d be NonatomicND of V,A;

cluster (SC_assignment (f,v)) . d -> Relation-like Function-like ;

The composition of superposition into a predicate

proof end;

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}

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₁[ object ] means $1 in_doms g;
deffunc H₁( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom $1 & S₁[d] ) } ;

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))) ) );

proof end;

The composition of superposition into a predicate

proof end;

end;

:: deftheorem Def9 defines SCPsuperpos NOMIN_2:def 9 :

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;

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

The composition of superposition into a predicate (one function)

proof end;

end;

:: deftheorem Def10 defines SC_Psuperpos NOMIN_2:def 10 :

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₁,b₂ -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)))) )

proof end;

definition

let V, A be set ;
let v be object ;
deffunc H₁( 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 ) } ;

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) ) );

proof end;

The composition of superposition into a predicate (one function)

proof end;

end;

:: deftheorem Def11 defines SCPsuperpos NOMIN_2:def 11 :

definition

let V, A be set ;
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);

The composition of superposition into a function

proof end;

end;

:: deftheorem defines SC_Psuperpos NOMIN_2:def 12 :

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 )

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*>)

proof end;

definition

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))) ) );

proof end;

The composition of superposition into a function

proof end;

end;

:: deftheorem Def13 defines SCFsuperpos NOMIN_2:def 13 :

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;

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

The composition of superposition into a function (one function)

proof end;

end;

:: deftheorem Def14 defines SC_Fsuperpos NOMIN_2:def 14 :

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₁,b₂ -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)))) )

proof end;

definition

let V, A be set ;
let v be object ;
deffunc H₁( 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 ) } ;

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) ) );

proof end;

The composition of superposition into a function (one function)

proof end;

end;

:: deftheorem Def15 defines SCFsuperpos NOMIN_2:def 15 :

definition

let V, A be set ;
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);

proof end;

end;

:: deftheorem defines SC_Fsuperpos NOMIN_2:def 16 :

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 )

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*>)

proof end;

Name checking predicate

definition

let V, A be set ;
let v be object ;
defpred S₁[ object ] means ex d being NonatomicND of V,A st
( 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 ) ) ) );

proof end;