:: On an algorithmic algebra over simple-named complex-valued nominative data
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Received June 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NOMIN_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1,
MARGREL1, XBOOLEAN, TARSKI, ZFMISC_1, NOMIN_2, PARTPR_1, FUNCOP_1, NAT_1,
FINSEQ_1, FINSET_1, PARTPR_2, XXREAL_0, ARYTM_3, CARD_1, NUMBERS,
FINSEQ_2, CARD_3, ORDERS_5, SETFAM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, MARGREL1, RELAT_1,
ORDINAL1,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, BINOP_1,
SETFAM_1, XXREAL_0, NAT_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1, FINSEQ_2,
NOMIN_1, PARTPR_1, PARTPR_2;
constructors ENUMSET1, RELSET_1, SETFAM_1, NOMIN_1, PARTPR_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, RELSET_1, NOMIN_1,
PARTPR_1, FINSEQ_1, PARTPR_2, ORDINAL1, XREAL_0, FINSEQ_2, FINSET_1,
FINSEQ_3, JORDAN23;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1,
NOMIN_1;
equalities MARGREL1, XBOOLEAN, NOMIN_1, PARTPR_1, FUNCOP_1, FINSEQ_2,
PARTPR_2;
expansions TARSKI, FUNCOP_1, NOMIN_1, ZFMISC_1, SETFAM_1;
theorems TARSKI, RELAT_1, RELSET_1, FUNCOP_1, BINOP_1, PARTFUN1, FUNCT_1,
FUNCT_2, NOMIN_1, ZFMISC_1, PARTPR_1, XBOOLE_0, XBOOLE_1, GRFUNC_1,
XTUPLE_0, ENUMSET1, FINSEQ_1, FINSEQ_3, FINSET_1, XXREAL_0, FINSEQ_2;
schemes FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, PARTPR_2;
begin :: Preliminaries
reserve a,b,c,v,v1,x,y for object;
reserve V,A for set;
reserve d for TypeSCNominativeData of V,A;
theorem Th1:
{a,b,c} c= A iff a in A & b in A & c in A
proof
set X = {a,b,c};
a in X & b in X & c in X by ENUMSET1:def 1;
hence {a,b,c} c= A implies a in A & b in A & c in A;
assume
A1: a in A & b in A & c in A;
let x;
thus thesis by A1,ENUMSET1:def 1;
end;
registration
let a,b,c,d,e,f be object;
cluster {[a,b],[c,d],[e,f]} -> Relation-like;
coherence
proof
let x;
assume x in {[a,b],[c,d],[e,f]};
then x = [a,b] or x = [c,d] or x = [e,f] by ENUMSET1:def 1;
hence thesis;
end;
end;
theorem Th2:
for a,b,c,d,e,f being object holds dom {[a,b],[c,d],[e,f]} = {a,c,e}
proof
let a,b,c,d,e,f be object;
A1: dom {[a,b],[c,d]} = {a,c} by RELAT_1:10;
A2: dom {[e,f]} = {e} by RELAT_1:9;
{[a,b],[c,d],[e,f]} = {[a,b],[c,d]} \/ {[e,f]} by ENUMSET1:3;
hence dom {[a,b],[c,d],[e,f]} = dom {[a,b],[c,d]} \/ dom {[e,f]}
by XTUPLE_0:23
.= {a,c,e} by A1,A2,ENUMSET1:3;
end;
theorem Th3:
for a,b,c,d,e,f being object holds rng {[a,b],[c,d],[e,f]} = {b,d,f}
proof
let a,b,c,d,e,f be object;
A1: rng {[a,b],[c,d]} = {b,d} by RELAT_1:10;
A2: rng {[e,f]} = {f} by RELAT_1:9;
{[a,b],[c,d],[e,f]} = {[a,b],[c,d]} \/ {[e,f]} by ENUMSET1:3;
hence rng {[a,b],[c,d],[e,f]} = rng {[a,b],[c,d]} \/ rng {[e,f]}
by XTUPLE_0:27
.= {b,d,f} by A1,A2,ENUMSET1:3;
end;
registration
let V;
cluster one-to-one V-valued for FinSequence;
existence
proof
per cases;
suppose V is empty;
take <*>V;
thus thesis;
end;
suppose V is non empty;
then reconsider V as non empty set;
take <*the Element of V*>;
thus thesis;
end;
end;
end;
theorem Th4:
dom <*a,b,c*> = {1,2,3}
proof
thus dom <*a,b,c*> = Seg len <*a,b,c*> by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45,FINSEQ_3:1;
end;
registration
let V,A;
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:
v in V implies {[v,d]} is NonatomicND of V,A
proof
assume v in V;
then naming(V,A,v,d) = v.-->d by NOMIN_1:def 13
.= {[v,d]} by ZFMISC_1:29;
hence thesis;
end;
theorem Th6:
for D being finite Function st dom D c= V & rng D c= ND(V,A) holds
D is NonatomicND of V,A
proof
let D be finite Function such that
A1: dom D c= V and
A2: rng D c= ND(V,A);
defpred P[set] means $1 is NonatomicND of V,A;
A3: D is finite;
A4: P[{}] by NOMIN_1:30;
A5: for x,B being set st x in D & B c= D & P[B] holds P[B \/ {x}]
proof
let x,B be set such that
A6: x in D and
A7: B c= D;
assume P[B];
then reconsider B as NonatomicND of V,A;
consider a,b such that
A8: x = [a,b] by A6,RELAT_1:def 1;
A9: a in dom D by A6,A8,XTUPLE_0:def 12;
b in rng D by A6,A8,XTUPLE_0:def 13;
then b is TypeSCNominativeData of V,A by A2,NOMIN_1:39;
then
A10: {[a,b]} is NonatomicND of V,A by A1,A9,Th5;
{x} c= D by A6,ZFMISC_1:31;
then B \/ {[a,b]} is Function by A7,A8,GRFUNC_1:14;
hence thesis by A8,A10,NOMIN_1:36,PARTFUN1:51;
end;
P[D] from FINSET_1:sch 2(A3,A4,A5);
hence thesis;
end;
theorem
for d1,d2 being TypeSCNominativeData of V,A holds
d2 c= global_overlapping(V,A,d1,d2)
proof
let d1,d2 be TypeSCNominativeData of V,A;
per cases;
suppose not d1 in A & not d2 in A;
then ex f1,f2 being Function st f1 = d1 & f2 = d2 &
global_overlapping(V,A,d1,d2) = f2 \/ (f1|(dom(f1)\dom(f2)))
by NOMIN_1:def 16;
hence thesis by XBOOLE_1:7;
end;
suppose d1 in A or d2 in A;
hence thesis by NOMIN_1:def 16;
end;
end;
theorem
for d being NonatomicND of V,A holds d is TypeSCNominativeData of V,A;
theorem Th9:
for d1,d2 being NonatomicND of V,A holds
global_overlapping(V,A,d1,d2) is NonatomicND of V,A
proof
let d1,d2 be NonatomicND of V,A;
per cases;
suppose not d1 in A & not d2 in A;
then
A1: global_overlapping(V,A,d1,d2) = d2 \/ (d1|(dom(d1)\dom(d2)))
by NOMIN_1:64;
d1|(dom(d1)\dom(d2)) is NonatomicND of V,A by NOMIN_1:32,RELAT_1:59;
hence thesis by A1,NOMIN_1:36,PARTFUN1:51;
end;
suppose d1 in A or d2 in A;
hence thesis by NOMIN_1:def 16;
end;
end;
registration
let V,A;
let d1,d2 be NonatomicND of V,A;
cluster global_overlapping(V,A,d1,d2) -> Function-like Relation-like;
coherence by Th9;
end;
registration
let V,A,v;
let d1 be NonatomicND of V,A;
let d2 be object;
cluster local_overlapping(V,A,d1,d2,v) -> Function-like Relation-like;
coherence;
end;
theorem Th10:
v in V implies
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
assume
A1: v in V;
let d1,d2 be TypeSCNominativeData of V,A;
let L be Function such that
A2: L = local_overlapping(V,A,d1,d2,v);
A4: naming(V,A,v,d2) = v.-->d2 by A1,NOMIN_1:def 13;
A6: v in {v} by TARSKI:def 1;
A7: (v.-->d2).v = d2 by FUNCOP_1:72;
per cases;
suppose not d1 in A & not naming(V,A,v,d2) in A;
then consider f1,f2 being Function such that
f1 = d1 and
A8: f2 = naming(V,A,v,d2) and
A9: L = f2 \/ (f1|(dom(f1)\dom(f2))) by A2,NOMIN_1:def 16;
thus L.v = f2.v by A4,A6,A8,A9,GRFUNC_1:15
.= d2 by A8,A4,A6,FUNCOP_1:7;
end;
suppose d1 in A or naming(V,A,v,d2) in A;
hence thesis by A4,A7,A2,NOMIN_1:def 16;
end;
end;
theorem
for d1 being NonatomicND of V,A,
z being Element of V holds
V is non empty & v in dom d1 & d = denaming(V,A,v).d1
implies local_overlapping(V,A,d1,d,z).z = d1.v
proof
let d1 be NonatomicND of V,A,
z be Element of V;
assume
A1: V is non empty;
set Dj = denaming(V,A,v);
assume that
A2: v in dom d1 and
A3: d = Dj.d1;
dom Dj = {d where d is NonatomicND of V,A: v in dom d}
by NOMIN_1:def 18;
then
A4: d1 in dom Dj by A2;
thus local_overlapping(V,A,d1,d,z).z = Dj.d1 by A1,A3,Th10
.= denaming(v,d1) by A4,NOMIN_1:def 18
.= d1.v by A2,NOMIN_1:def 12;
end;
theorem
v in V & v <> v1 implies
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
assume that
A1: v in V and
A2: v <> v1;
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A such that
A4: v1 in dom d1 and
A5: not d1 in A & not naming(V,A,v,d2) in A;
A7: naming(V,A,v,d2) = v.-->d2 by A1,NOMIN_1:def 13;
consider f1,f2 being Function such that
A10: f1 = d1 and
A11: f2 = naming(V,A,v,d2) and
A12: local_overlapping(V,A,d1,d2,v) = f2 \/ (f1|(dom(f1)\dom(f2)))
by A5,NOMIN_1:def 16;
not v1 in {v} by A2,TARSKI:def 1;
then v1 in dom(f1)\dom(f2) by A4,A7,A10,A11,XBOOLE_0:def 5;
then
A13: v1 in dom(f1|(dom(f1)\dom(f2))) by RELAT_1:57;
hence local_overlapping(V,A,d1,d2,v).v1 = (f1|(dom(f1)\dom(f2))).v1
by A12,GRFUNC_1:15
.= d1.v1 by A10,A13,FUNCT_1:47;
end;
theorem Th12:
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
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A such that
A1: v in V and
A2: not v in dom d1 and
A3: not d1 in A & not naming(V,A,v,d2) in A;
set n = naming(V,A,v,d2);
A4: n = v .--> d2 by A1,NOMIN_1:def 13;
A5: dom (d1|(dom(d1)\dom(n))) = dom d1
proof
thus dom(d1|(dom(d1)\dom(n))) c= dom d1 by RELAT_1:60;
dom(d1) c= dom(d1)\dom(n) by A2,A4,ZFMISC_1:34;
hence thesis by RELAT_1:62;
end;
local_overlapping(V,A,d1,d2,v) = n \/ (d1|(dom(d1)\dom(n)))
by A3,NOMIN_1:64;
hence thesis by A4,A5,XTUPLE_0:23;
end;
theorem Th13:
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
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A such that
A1: v in V and
A2: v in dom d1 and
A3: not d1 in A & not naming(V,A,v,d2) in A;
set n = naming(V,A,v,d2);
A4: n = v .--> d2 by A1,NOMIN_1:def 13;
A5: dom(n) \/ dom(d1|(dom(d1)\dom(n))) = dom(d1)
proof
A6: dom(n) c= dom(d1) by A2,A4,ZFMISC_1:31;
dom(d1|(dom(d1)\dom(n))) c= dom(d1) by RELAT_1:60;
hence dom(n) \/ dom(d1|(dom(d1)\dom(n))) c= dom(d1) by A6,XBOOLE_1:8;
let x be object;
assume
A7: x in dom(d1);
per cases;
suppose x = v;
then x in dom(n) by A4,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose x <> v;
then not x in dom(n) by A4,TARSKI:def 1;
then x in dom(d1)\dom(n) by A7,XBOOLE_0:def 5;
then x in dom(d1|(dom(d1)\dom(n))) by RELAT_1:57;
hence thesis by XBOOLE_0:def 3;
end;
end;
local_overlapping(V,A,d1,d2,v) = n \/ (d1|(dom(d1)\dom(n)))
by A3,NOMIN_1:64;
hence thesis by A5,XTUPLE_0:23;
end;
theorem Th14:
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
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A such that
A1: v in V & not d1 in A & not naming(V,A,v,d2) in A;
per cases;
suppose
A2: v in dom d1;
then dom local_overlapping(V,A,d1,d2,v) = dom d1 by A1,Th13;
hence thesis by A2,ZFMISC_1:40;
end;
suppose not v in dom d1;
hence thesis by A1,Th12;
end;
end;
definition
let V,A;
mode SCPartialNominativePredicate of V,A is PartialPredicate of ND(V,A);
end;
reserve p,q,r for SCPartialNominativePredicate of V,A;
theorem Th15:
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
set X = {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};
set Y = {d where d is Element of ND(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};
X = Y
proof
thus X c= Y
proof
let x;
assume x in X;
then ex d being TypeSCNominativeData of V,A st d = x &
(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);
hence thesis;
end;
let x;
assume x in Y;
then consider d being Element of ND(V,A) such that
A1: d = x &
(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);
d is TypeSCNominativeData of V,A by NOMIN_1:39;
hence thesis by A1;
end;
hence thesis by PARTPR_1:def 4;
end;
theorem
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
set F = PP_and(p,q);
set P = PP_not(p);
set Q = PP_not(q);
set D = {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};
A1: dom F = dom PP_or(P,Q) by PARTPR_1:def 2;
A2: 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} by Th15;
A3: dom P = dom p by PARTPR_1:def 2;
A4: dom Q = dom q by PARTPR_1:def 2;
thus dom F c= D
proof
let x;
assume x in dom F;
then consider d being TypeSCNominativeData of V,A such that
A5: x = d and
A6: 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 by A1,A2;
per cases by A6;
suppose that
A7: d in dom P and
A8: P.d = TRUE;
p.d = FALSE by A3,A7,A8,PARTPR_1:5;
hence thesis by A3,A5,A7;
end;
suppose that
A9: d in dom Q and
A10: Q.d = TRUE;
q.d = FALSE by A4,A9,A10,PARTPR_1:5;
hence thesis by A4,A5,A9;
end;
suppose that
A11: d in dom P & d in dom Q and
A12: P.d = FALSE & Q.d = FALSE;
p.d = TRUE & q.d = TRUE by A3,A4,A11,A12,PARTPR_1:4;
hence thesis by A3,A4,A5,A11;
end;
end;
let x;
assume x in D;
then consider d being TypeSCNominativeData of V,A such that
A13: x = d and
A14: 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;
per cases by A14;
suppose that
A15: d in dom p and
A16: p.d = FALSE;
P.d = TRUE by A15,A16,PARTPR_1:def 2;
hence thesis by A1,A2,A3,A13,A15;
end;
suppose that
A17: d in dom q and
A18: q.d = FALSE;
Q.d = TRUE by A17,A18,PARTPR_1:def 2;
hence thesis by A1,A2,A4,A13,A17;
end;
suppose that
A19: d in dom p & d in dom q and
A20: p.d = TRUE & q.d = TRUE;
P.d = FALSE & Q.d = FALSE by A19,A20,PARTPR_1:def 2;
hence thesis by A1,A2,A3,A4,A13,A19;
end;
end;
theorem
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
set F = PP_imp(p,q);
set P = PP_not(p);
set D = {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};
A1: dom F = {d where d is Element of ND(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} by PARTPR_1:def 4;
A2: dom P = dom p by PARTPR_1:def 2;
thus dom F c= D
proof
let x;
assume x in dom F;
then consider d being Element of ND(V,A) such that
A3: x = d and
A4: 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 by A1;
reconsider d as TypeSCNominativeData of V,A by NOMIN_1:39;
per cases by A4;
suppose that
A5: d in dom P and
A6: P.d = TRUE;
p.d = FALSE by A2,A5,A6,PARTPR_1:5;
hence thesis by A2,A3,A5;
end;
suppose d in dom q & q.d = TRUE;
hence thesis by A3;
end;
suppose that
A7: d in dom P & d in dom q and
A8: P.d = FALSE and
A9: q.d = FALSE;
p.d = TRUE by A2,A7,A8,PARTPR_1:4;
hence thesis by A2,A3,A7,A9;
end;
end;
let x;
assume x in D;
then consider d being TypeSCNominativeData of V,A such that
A10: x = d and
A11: 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;
per cases by A11;
suppose that
A12: d in dom p and
A13: p.d = FALSE;
P.d = TRUE by A12,A13,PARTPR_1:def 2;
hence thesis by A1,A2,A10,A12;
end;
suppose d in dom q & q.d = TRUE;
hence thesis by A1,A10;
end;
suppose that
A14: d in dom p and
A15: d in dom q and
A16: p.d = TRUE and
A17: q.d = FALSE;
P.d = FALSE by A14,A16,PARTPR_1:def 2;
hence thesis by A1,A2,A10,A14,A15,A17;
end;
end;
definition
let V,A,v;
defpred D1[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 D2[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 D(Function) =
{d where d is TypeSCNominativeData of V,A: D1[d,$1] or D2[d,$1]};
func SCexists(V,A,v) -> Function of Pr(ND(V,A)),Pr(ND(V,A)) means :Def1:
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
proof
defpred P[object,object] means
for p being SCPartialNominativePredicate of V,A st p = $1 holds
for f being Function st f = $2 holds
dom f = D(p) &
for d being TypeSCNominativeData of V,A holds
(D1[d,p] implies f.d = TRUE) & (D2[d,p] implies f.d = FALSE);
A1: for x being object st x in Pr(ND(V,A))
ex y being object st y in Pr(ND(V,A)) & P[x,y]
proof
let x;
assume x in Pr(ND(V,A));
then reconsider X = x as PartFunc of ND(V,A),BOOLEAN by PARTFUN1:46;
defpred Q[object,object] means
for d being TypeSCNominativeData of V,A st d = $1 holds
(D1[d,X] implies $2 = TRUE) & (D2[d,X] implies $2 = FALSE);
A2: for a being object st a in D(X)
ex b being object st b in BOOLEAN & Q[a,b]
proof
let a be object;
assume a in D(X);
then consider d being TypeSCNominativeData of V,A such that
A3: a = d and
A4: D1[d,X] or D2[d,X];
per cases by A4;
suppose
A5: D1[d,X];
take TRUE;
thus thesis by A3,A5;
end;
suppose
A6: D2[d,X];
take FALSE;
thus thesis by A3,A6;
end;
end;
consider g being Function such that
A7: dom g = D(X) and
A8: rng g c= BOOLEAN and
A9: for x being object st x in D(X) holds Q[x,g.x] from FUNCT_1:sch 6(A2);
take g;
D(X) c= ND(V,A)
proof
let x;
assume x in D(X);
then ex d being TypeSCNominativeData of V,A st d = x &
(D1[d,X] or D2[d,X]);
hence thesis;
end;
then g is PartFunc of ND(V,A),BOOLEAN by A7,A8,RELSET_1:4;
hence g in Pr(ND(V,A)) by PARTFUN1:45;
let p be SCPartialNominativePredicate of V,A such that
A10: p = x;
let f be Function such that
A11: f = g;
thus dom f = D(p) by A7,A10,A11;
let d be TypeSCNominativeData of V,A;
hereby
assume
A12: D1[d,p];
then d in D(X) by A10;
hence f.d = TRUE by A9,A10,A11,A12;
end;
assume
A13: D2[d,p];
then d in D(X) by A10;
hence thesis by A9,A10,A11,A13;
end;
consider F being Function of Pr(ND(V,A)),Pr(ND(V,A)) such that
A14: for x being object st x in Pr(ND(V,A)) holds P[x,F.x]
from FUNCT_2:sch 1(A1);
take F;
let p be SCPartialNominativePredicate of V,A;
p in Pr(ND(V,A)) by PARTFUN1:45;
hence thesis by A14;
end;
uniqueness
proof
let f,g be Function of Pr(ND(V,A)),Pr(ND(V,A)) such that
A15: for p being SCPartialNominativePredicate of V,A holds
dom(f.p) = D(p) &
for d being TypeSCNominativeData of V,A holds
(D1[d,p] implies f.p.d = TRUE) & (D2[d,p] implies f.p.d = FALSE) and
A16: for p being SCPartialNominativePredicate of V,A holds
dom(g.p) = D(p) &
for d being TypeSCNominativeData of V,A holds
(D1[d,p] implies g.p.d = TRUE) & (D2[d,p] implies g.p.d = FALSE);
let x be Element of Pr(ND(V,A));
reconsider p = x as SCPartialNominativePredicate of V,A by PARTFUN1:46;
A17: dom(f.x) = D(p) by A15;
hence dom(f.x) = dom(g.x) by A16;
let a be object;
assume a in dom(f.x);
then consider d being TypeSCNominativeData of V,A such that
A18: a = d and
A19: D1[d,p] or D2[d,p] by A17;
per cases by A19;
suppose
A20: D1[d,p];
thus f.x.a = TRUE by A15,A18,A20
.= g.x.a by A16,A18,A20;
end;
suppose
A21: D2[d,p];
thus f.x.a = FALSE by A15,A18,A21
.= g.x.a by A16,A18,A21;
end;
end;
end;
definition
let V,A,v,p;
func SC_exists(p,v) -> SCPartialNominativePredicate of V,A equals
SCexists(V,A,v).p;
coherence
proof
p in Pr(ND(V,A)) by PARTFUN1:45;
hence thesis by PARTFUN1:46,FUNCT_2:5;
end;
end;
theorem Th18:
x in dom SC_exists(p,v) implies
(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
assume
A1: x in dom SC_exists(p,v);
dom(SC_exists(p,v)) = {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)} by Def1;
then ex d2 being TypeSCNominativeData of V,A st x = d2 &
((ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,d2,d1,v) in dom p &
p.local_overlapping(V,A,d2,d1,v) = TRUE) or
(for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,d2,d1,v) in dom p &
p.local_overlapping(V,A,d2,d1,v) = FALSE)) by A1;
hence thesis;
end;
theorem
SC_exists(PP_BottomPred(ND(V,A)),v) = PP_BottomPred(ND(V,A))
proof
set B = PP_BottomPred(ND(V,A));
set T = PP_True(ND(V,A));
set o = SC_exists(B,v);
thus dom o = dom B
proof
thus dom o c= dom B
proof
let x;
assume x in dom o;
then (ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom B &
B.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 B &
B.local_overlapping(V,A,x,d1,v) = FALSE) by Th18;
hence thesis;
end;
thus dom B c= dom o;
end;
let x;
assume x in dom o;
then (ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom B &
B.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 B &
B.local_overlapping(V,A,x,d1,v) = FALSE) by Th18;
hence thesis;
end;
::$N Distributivity law
theorem
SC_exists(PP_or(p,q),v) = PP_or(SC_exists(p,v),SC_exists(q,v))
proof
set a = PP_or(p,q);
set f = SC_exists(a,v);
set g = SC_exists(p,v);
set h = SC_exists(q,v);
set b = PP_or(g,h);
A1: dom a = {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} by Th15;
A2: dom b = {d where d is TypeSCNominativeData of V,A:
d in dom g & g.d = TRUE or d in dom h & h.d = TRUE
or d in dom g & g.d = FALSE & d in dom h & h.d = FALSE} by Th15;
A3: dom f = {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 a &
a.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 a &
a.local_overlapping(V,A,d,d1,v) = FALSE)} by Def1;
A4: dom g = {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)} by Def1;
A5: dom h = {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 q &
q.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 q &
q.local_overlapping(V,A,d,d1,v) = FALSE)} by Def1;
thus dom f = dom b
proof
thus dom f c= dom b
proof
let x;
assume
A6: x in dom f;
then
A7: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases by A6,Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom a &
a.local_overlapping(V,A,x,d1,v) = TRUE;
then consider d1 being TypeSCNominativeData of V,A such that
A8: local_overlapping(V,A,x,d1,v) in dom a and
A9: a.local_overlapping(V,A,x,d1,v) = TRUE;
set L = local_overlapping(V,A,x,d1,v);
per cases by A8,PARTPR_1:8;
suppose
A10: L in dom p & p.L = TRUE;
then
A11: x in dom g by A7,A4;
g.x = TRUE by A7,A10,Def1;
hence thesis by A2,A7,A11;
end;
suppose
A12: L in dom q & q.L = TRUE;
then
A13: x in dom h by A7,A5;
h.x = TRUE by A7,A12,Def1;
hence thesis by A2,A7,A13;
end;
suppose L in dom p & p.L = FALSE & L in dom q & q.L = FALSE;
hence thesis by A9,PARTPR_1:9;
end;
end;
suppose
A14: for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom a &
a.local_overlapping(V,A,x,d1,v) = FALSE;
A15: 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
let d1 be TypeSCNominativeData of V,A;
set O = local_overlapping(V,A,x,d1,v);
O in dom a & a.O = FALSE by A14;
hence thesis by PARTPR_1:13;
end;
then
A16: x in dom g by A7,A4;
A17: g.x = FALSE by A7,A15,Def1;
A18: for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom q &
q.local_overlapping(V,A,x,d1,v) = FALSE
proof
let d1 be TypeSCNominativeData of V,A;
set O = local_overlapping(V,A,x,d1,v);
O in dom a & a.O = FALSE by A14;
hence thesis by PARTPR_1:13;
end;
then
A19: x in dom h by A7,A5;
h.x = FALSE by A7,A18,Def1;
hence thesis by A2,A7,A16,A17,A19;
end;
end;
let x;
assume
A20: x in dom b;
then
A21: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases by A20,PARTPR_1:8;
suppose that
A22: x in dom g and
A23: g.x = TRUE;
per cases by A22,Th18;
suppose 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;
then consider d1 being TypeSCNominativeData of V,A such that
A24: local_overlapping(V,A,x,d1,v) in dom p and
A25: p.local_overlapping(V,A,x,d1,v) = TRUE;
set L = local_overlapping(V,A,x,d1,v);
L in dom a & a.L = TRUE by A1,A24,A25,PARTPR_1:def 4;
hence thesis by A3,A21;
end;
suppose 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;
hence thesis by A21,A23,Def1;
end;
end;
suppose that
A26: x in dom h and
A27: h.x = TRUE;
per cases by A26,Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom q &
q.local_overlapping(V,A,x,d1,v) = TRUE;
then consider d1 being TypeSCNominativeData of V,A such that
A28: local_overlapping(V,A,x,d1,v) in dom q and
A29: q.local_overlapping(V,A,x,d1,v) = TRUE;
set L = local_overlapping(V,A,x,d1,v);
L in dom a & a.L = TRUE by A1,A28,A29,PARTPR_1:def 4;
hence thesis by A3,A21;
end;
suppose for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom q &
q.local_overlapping(V,A,x,d1,v) = FALSE;
hence thesis by A21,A27,Def1;
end;
end;
suppose that
A30: x in dom g and
A31: g.x = FALSE and
A32: x in dom h and
A33: h.x = FALSE;
for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom a &
a.local_overlapping(V,A,x,d1,v) = FALSE
proof
let d1 be TypeSCNominativeData of V,A;
A34: not 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 by A21,A31,Def1;
A35: not ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom q &
q.local_overlapping(V,A,x,d1,v) = TRUE by A21,A33,Def1;
set L = local_overlapping(V,A,x,d1,v);
L in dom p & p.L = FALSE & L in dom q & q.L = FALSE
by A34,A35,A30,A32,Th18;
hence L in dom a & a.L = FALSE by A1,PARTPR_1:def 4;
end;
hence thesis by A3,A21;
end;
end;
let x;
assume
A36: x in dom f;
then
A37: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases by A36,Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
local_overlapping(V,A,x,d1,v) in dom a &
a.local_overlapping(V,A,x,d1,v) = TRUE;
then consider d1 being TypeSCNominativeData of V,A such that
A38: local_overlapping(V,A,x,d1,v) in dom a and
A39: a.local_overlapping(V,A,x,d1,v) = TRUE;
set L = local_overlapping(V,A,x,d1,v);
per cases by A38,PARTPR_1:8;
suppose
A40: L in dom p & p.L = TRUE;
then
A41: x in dom g by A37,A4;
g.x = TRUE by A37,A40,Def1;
hence b.x = TRUE by A41,PARTPR_1:def 4
.= f.x by A38,A39,A37,Def1;
end;
suppose
A42: L in dom q & q.L = TRUE;
then
A43: x in dom h by A37,A5;
h.x = TRUE by A37,A42,Def1;
hence b.x = TRUE by A43,PARTPR_1:def 4
.= f.x by A38,A39,A37,Def1;
end;
suppose L in dom p & p.L = FALSE & L in dom q & q.L = FALSE;
hence thesis by A39,PARTPR_1:9;
end;
end;
suppose
A44: for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom a &
a.local_overlapping(V,A,x,d1,v) = FALSE;
A45: 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
let d1 be TypeSCNominativeData of V,A;
set O = local_overlapping(V,A,x,d1,v);
O in dom a & a.O = FALSE by A44;
hence thesis by PARTPR_1:13;
end;
then
A46: x in dom g by A37,A4;
A47: g.x = FALSE by A37,A45,Def1;
A48: for d1 being TypeSCNominativeData of V,A holds
local_overlapping(V,A,x,d1,v) in dom q &
q.local_overlapping(V,A,x,d1,v) = FALSE
proof
let d1 be TypeSCNominativeData of V,A;
set O = local_overlapping(V,A,x,d1,v);
O in dom a & a.O = FALSE by A44;
hence thesis by PARTPR_1:13;
end;
then
A49: x in dom h by A37,A5;
h.x = FALSE by A37,A48,Def1;
hence b.x = FALSE by A46,A47,A49,PARTPR_1:def 4
.= f.x by A44,A37,Def1;
end;
end;
begin :: On an algorithmic algebra over simple-named complex-valued nominative data
reserve n for Nat;
reserve X for Function;
definition
let F be Function-yielding Function;
let d be object;
pred d in_doms F means :Def3:
for x being object st x in dom F holds d in dom(F.x);
end;
definition
let g be Function-yielding Function;
let X be Function;
let d be object;
func NDdataSeq(g,X,d) -> Function means :Def4:
dom it = dom X &
for x st x in dom X holds it.x = [X.x,g.x.d];
existence
proof
deffunc F(object) = [X.$1,g.$1.d];
consider p being Function such that
A1: dom p = dom X &
for x st x in dom X holds p.x = F(x) from FUNCT_1:sch 3;
take p;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function such that
A2: dom F = dom X and
A3: for x st x in dom X holds F.x = [X.x,g.x.d] and
A4: dom G = dom X and
A5: for x st x in dom X holds G.x = [X.x,g.x.d];
thus dom F = dom G by A2,A4;
let x;
assume
A6: x in dom F;
hence F.x = [X.x,g.x.d] by A2,A3
.= G.x by A2,A5,A6;
end;
end;
registration
let g be Function-yielding Function;
let X be finite Function;
let d be object;
cluster NDdataSeq(g,X,d) -> finite;
coherence
proof
dom NDdataSeq(g,X,d) = dom X by Def4;
hence thesis by FINSET_1:10;
end;
end;
registration
let g be Function-yielding Function;
let X be FinSequence;
let d be object;
cluster NDdataSeq(g,X,d) -> FinSequence-like;
coherence
proof
take len X;
thus dom NDdataSeq(g,X,d) = dom X by Def4
.= Seg len X by FINSEQ_1:def 3;
end;
end;
definition
let g be Function-yielding Function;
let X be Function;
let d be object;
func NDentry(g,X,d) -> set equals
rng NDdataSeq(g,X,d);
coherence;
end;
theorem
for f being Function, a,d being object holds
NDentry(<*f*>,<*a*>,d) = {[a,f.d]}
proof
let f be Function;
let a,d be object;
set X = <*a*>;
set G = <*f*>;
set A = {[a,f.d]};
set N = NDdataSeq(G,X,d);
set F = NDentry(G,X,d);
A1: dom N = dom X by Def4;
A2: dom X = {1} by FINSEQ_1:2,38;
A3: 1 in {1} by TARSKI:def 1;
then
A4: N.1 = [X.1,G.1.d] by A2,Def4;
thus F c= A
proof
let y be object;
assume y in F;
then consider z being object such that
A6: z in dom N and
A7: N.z = y by FUNCT_1:def 3;
z = 1 by A1,A2,A6,TARSKI:def 1;
hence thesis by A4,A7,TARSKI:def 1;
end;
let y,z be object;
assume [y,z] in A;
then [y,z] = [a,f.d] by TARSKI:def 1;
hence thesis by A1,A2,A3,A4,FUNCT_1:def 3;
end;
theorem Th22:
for f,g being Function, a,b,d being object holds
NDentry(<*f,g*>,<*a,b*>,d) = {[a,f.d],[b,g.d]}
proof
let f,g be Function;
let a,b,d be object;
set X = <*a,b*>;
set G = <*f,g*>;
set A = {[a,f.d],[b,g.d]};
set N = NDdataSeq(G,X,d);
set F = NDentry(G,X,d);
A1: dom N = dom X by Def4;
A2: dom X = {1,2} by FINSEQ_1:92;
A3: 1 in {1,2} by TARSKI:def 2;
then
A4: N.1 = [X.1,G.1.d] by A2,Def4;
A5: 2 in {1,2} by TARSKI:def 2;
then
A6: N.2 = [X.2,G.2.d] by A2,Def4;
thus F c= A
proof
let y be object;
assume y in F;
then consider z being object such that
A8: z in dom N and
A9: N.z = y by FUNCT_1:def 3;
z = 1 or z = 2 by A1,A2,A8,TARSKI:def 2;
hence thesis by A4,A6,A9,TARSKI:def 2;
end;
let y,z be object;
assume [y,z] in A;
then [y,z] = [a,f.d] or [y,z] = [b,g.d] by TARSKI:def 2;
hence thesis by A1,A2,A3,A4,A5,A6,FUNCT_1:def 3;
end;
theorem Th23:
for f,g,h being Function, 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
let f,g,h be Function;
let a,b,c,d be object;
set X = <*a,b,c*>;
set G = <*f,g,h*>;
set A = {[a,f.d],[b,g.d],[c,h.d]};
set N = NDdataSeq(G,X,d);
set F = NDentry(G,X,d);
A1: dom N = dom X by Def4;
A2: dom X = {1,2,3} by Th4;
A3: 1 in {1,2,3} by ENUMSET1:def 1;
then
A4: N.1 = [X.1,G.1.d] by A2,Def4;
A5: 2 in {1,2,3} by ENUMSET1:def 1;
then
A6: N.2 = [X.2,G.2.d] by A2,Def4;
A7: 3 in {1,2,3} by ENUMSET1:def 1;
then
A8: N.3 = [X.3,G.3.d] by A2,Def4;
thus F c= A
proof
let y be object;
assume y in F;
then consider z being object such that
A10: z in dom N and
A11: N.z = y by FUNCT_1:def 3;
z = 1 or z = 2 or z = 3 by A1,A2,A10,ENUMSET1:def 1;
hence thesis by A4,A6,A8,A11,ENUMSET1:def 1;
end;
let y,z be object;
assume [y,z] in A;
then [y,z] = [a,f.d] or [y,z] = [b,g.d] or [y,z] = [c,h.d]
by ENUMSET1:def 1;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,FUNCT_1:def 3;
end;
registration
let g be Function-yielding Function;
let X be Function;
let d be object;
cluster NDentry(g,X,d) -> Relation-like;
coherence
proof
set f = NDdataSeq(g,X,d);
let x;
assume x in NDentry(g,X,d);
then consider z being object such that
A1: z in dom f and
A2: f.z = x by FUNCT_1:def 3;
dom f = dom X by Def4;
then f.z = [X.z,g.z.d] by A1,Def4;
hence thesis by A2;
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;
coherence
proof
set f = NDdataSeq(g,X,d);
let x,y1,y2 be object such that
A1: [x,y1] in NDentry(g,X,d) and
A2: [x,y2] in NDentry(g,X,d);
consider a being object such that
A3: a in dom f and
A4: f.a = [x,y1] by A1,FUNCT_1:def 3;
consider b being object such that
A5: b in dom f and
A6: f.b = [x,y2] by A2,FUNCT_1:def 3;
A7: dom f = dom X by Def4;
A8: f.a = [X.a,g.a.d] by A3,A7,Def4;
f.b = [X.b,g.b.d] by A5,A7,Def4;
then x = X.a & x = X.b by A4,A6,A8,XTUPLE_0:1;
then a = b by A3,A5,A7,FUNCT_1:def 4;
hence y1 = y2 by A4,A6,XTUPLE_0:1;
end;
end;
registration
let g be Function-yielding Function;
let X be finite Function;
let d be object;
cluster NDentry(g,X,d) -> finite;
coherence;
end;
theorem Th24:
for g being Function-yielding Function, X being Function, d being object
holds dom NDentry(g,X,d) = rng X
proof
let g be Function-yielding Function;
let X be Function;
let d be object;
set f = NDentry(g,X,d);
set h = NDdataSeq(g,X,d);
A1: dom h = dom X by Def4;
thus dom f c= rng X
proof
let x;
assume x in dom f;
then consider v such that
A2: [x,v] in f by XTUPLE_0:def 12;
consider z being object such that
A3: z in dom h and
A4: h.z = [x,v] by A2,FUNCT_1:def 3;
h.z = [X.z,g.z.d] by A1,A3,Def4;
then X.z = x by A4,XTUPLE_0:1;
hence thesis by A1,A3,FUNCT_1:def 3;
end;
let x;
assume x in rng X;
then consider z being object such that
A5: z in dom X and
A6: X.z = x by FUNCT_1:def 3;
h.z = [X.z,g.z.d] by A5,Def4;
then [X.z,g.z.d] in rng h by A1,A5,FUNCT_1:3;
hence thesis by A6,XTUPLE_0:def 12;
end;
definition
let V,A;
mode SCBinominativeFunction of V,A is PartFunc of ND(V,A),ND(V,A);
end;
reserve f,g,h for SCBinominativeFunction of V,A;
theorem Th25:
rng NDdataSeq(<*f*>,<*v*>,d) = v.-->f.d
proof
set g = <*f*>;
set X = <*v*>;
set N = NDdataSeq(g,X,d);
set F = v.-->f.d;
A1: dom N = dom X by Def4;
A2: dom X = {1} by FINSEQ_1:2,38;
A5: F = {[v,f.d]} by ZFMISC_1:29;
thus rng N c= F
proof
let y be object;
assume y in rng N;
then consider z being object such that
A6: z in dom N and
A7: N.z = y by FUNCT_1:def 3;
A8: z = 1 by A1,A2,A6,TARSKI:def 1;
N.z = [X.z,g.z.d] by A1,A6,Def4;
hence thesis by A7,A8,A5,TARSKI:def 1;
end;
let m,n be object;
assume [m,n] in F;
then
A9: [m,n] = [v,f.d] by A5,TARSKI:def 1;
A10: 1 in dom N by A1,A2,TARSKI:def 1;
then N.1 = [X.1,g.1.d] by A1,Def4;
hence thesis by A9,A10,FUNCT_1:def 3;
end;
theorem Th26:
a in V & d in dom f implies NDentry(<*f*>,<*a*>,d) = naming(V,A,a,f.d)
proof
set g = <*f*>;
set X = <*a*>;
assume
A1: a in V;
assume d in dom f;
then
A2: f.d is TypeSCNominativeData of V,A by NOMIN_1:39,PARTFUN1:4;
rng NDdataSeq(g,X,d) = a.-->f.d by Th25;
hence thesis by A1,A2,NOMIN_1:def 13;
end;
theorem
a in V & d in dom f implies
NDentry(<*f*>,<*a*>,d) is NonatomicND of V,A
proof
assume a in V & d in dom f;
then NDentry(<*f*>,<*a*>,d) = naming(V,A,a,f.d) by Th26;
hence thesis;
end;
theorem
{a,b} c= V & a <> b & d in dom f & d in dom g implies
NDentry(<*f,g*>,<*a,b*>,d) is NonatomicND of V,A
proof
assume that
A1: {a,b} c= V and
A2: a <> b and
A3: d in dom f & d in dom g;
reconsider O = <*a,b*> as one-to-one FinSequence by A2,FINSEQ_3:94;
set F = NDentry(<*f,g*>,O,d);
A4: F = {[a,f.d],[b,g.d]} by Th22;
then
A5: dom F = {a,b} by RELAT_1:10;
A6: rng F = {f.d,g.d} by A4,RELAT_1:10;
f.d in ND(V,A) & g.d in ND(V,A) by A3,PARTFUN1:4;
then rng F c= ND(V,A) by A6,ZFMISC_1:32;
hence thesis by A1,A5,Th6;
end;
theorem
{a,b,c} c= V & a,b,c are_mutually_distinct &
d in dom f & d in dom g & d in dom h implies
NDentry(<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
proof
assume that
A1: {a,b,c} c= V and
A2: a,b,c are_mutually_distinct and
A3: d in dom f & d in dom g & d in dom h;
reconsider O = <*a,b,c*> as one-to-one FinSequence by A2,FINSEQ_3:95;
set F = NDentry(<*f,g,h*>,O,d);
A4: F = {[a,f.d],[b,g.d],[c,h.d]} by Th23;
then
A5: dom F = {a,b,c} by Th2;
A6: rng F = {f.d,g.d,h.d} by A4,Th3;
f.d in ND(V,A) & g.d in ND(V,A) & h.d in ND(V,A) by A3,PARTFUN1:4;
then rng F c= ND(V,A) by A6,Th1;
hence thesis by A1,A5,Th6;
end;
definition
let V,A;
let f be FinSequence;
attr f is (V,A)-FPrg-yielding means :Def6:
for n st 1 <= n <= len f holds f.n is SCBinominativeFunction of V,A;
end;
registration
let V,A,f;
cluster <*f*> -> (V,A)-FPrg-yielding;
coherence
proof
let n such that
A1: 1 <= n <= len <*f*>;
len <*f*> = 1 by FINSEQ_1:40;
then n = 1 by A1,XXREAL_0:1;
hence thesis;
end;
end;
registration
let V,A,f,g;
cluster <*f,g*> -> (V,A)-FPrg-yielding;
coherence
proof
let n such that
A1: 1 <= n <= len <*f,g*>;
len <*f,g*> = 1+1 by FINSEQ_1:44;
then n = 1 or ... or n = 2 by A1;
hence thesis;
end;
end;
registration
let V,A,f,g,h;
cluster <*f,g,h*> -> (V,A)-FPrg-yielding;
coherence
proof
let n such that
A1: 1 <= n <= len <*f,g,h*>;
len <*f,g,h*> = 1+2 by FINSEQ_1:45;
then n = 1 or ... or n = 3 by A1;
hence thesis;
end;
end;
registration
let V,A,n;
cluster (V,A)-FPrg-yielding n-element for FinSequence;
existence
proof
take f = n |-> the SCBinominativeFunction of V,A;
thus f is (V,A)-FPrg-yielding
proof
let a be Nat;
dom f = Seg n;
hence thesis by FINSEQ_2:57,FINSEQ_3:25;
end;
thus thesis;
end;
end;
registration
let V,A,x;
let g be (V,A)-FPrg-yielding FinSequence;
cluster g.x -> Function-like Relation-like;
coherence
proof
per cases;
suppose
A1: x in dom g; then
reconsider x as Element of NAT;
1 <= x <= len g by A1,FINSEQ_3:25;
hence thesis by Def6;
end;
suppose not x in dom g;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let V,A;
cluster (V,A)-FPrg-yielding -> Function-yielding for FinSequence;
coherence;
end;
theorem Th30:
for g being (V,A)-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
let g be (V,A)-FPrg-yielding FinSequence;
let X be one-to-one FinSequence;
assume that
A1: dom g = dom X and
A2: d in_doms g;
set f = NDdataSeq(g,X,d);
set D = NDentry(g,X,d);
A3: dom f = dom X by Def4;
let y be object;
assume y in rng D;
then consider a such that
A4: a in dom D and
A5: D.a = y by FUNCT_1:def 3;
[a,y] in D by A4,A5,FUNCT_1:1;
then consider v such that
A6: v in dom f and
A7: f.v = [a,y] by FUNCT_1:def 3;
reconsider v as Element of NAT by A6;
f.v = [X.v,g.v.d] by A3,A6,Def4;
then
A8: y = g.v.d by A7,XTUPLE_0:1;
1 <= v <= len g by A1,A3,A6,FINSEQ_3:25;
then g.v is SCBinominativeFunction of V,A by Def6;
then
A9: rng(g.v) c= ND(V,A) by RELAT_1:def 19;
d in dom(g.v) by A1,A3,A6,A2;
hence thesis by A8,A9,FUNCT_1:3;
end;
theorem
for g being (V,A)-FPrg-yielding FinSequence
for X being one-to-one V-valued FinSequence st
dom g = dom X & d in_doms g
holds NDentry(g,X,d) is NonatomicND of V,A
proof
let g be (V,A)-FPrg-yielding FinSequence;
let X be one-to-one V-valued FinSequence;
assume
A1: dom g = dom X & d in_doms g;
A2: dom NDentry(g,X,d) = rng X by Th24;
A3: rng X c= V by RELAT_1:def 19;
rng NDentry(g,X,d) c= ND(V,A) by A1,Th30;
hence thesis by A2,A3,Th6;
end;
::$N Assignment composition
definition
let V,A,v;
func SCassignment(V,A,v) -> Function of FPrg(ND(V,A)),FPrg(ND(V,A)) means
:Def7:
for f being SCBinominativeFunction of V,A holds
dom(it.f) = dom f &
for d being TypeSCNominativeData of V,A holds
d in dom(it.f) implies it.f.d = local_overlapping(V,A,d,f.d,v);
existence
proof
defpred P[Function,Function] means
for f being SCBinominativeFunction of V,A st f = $1 holds
dom $2 = dom f &
for d being TypeSCNominativeData of V,A holds
d in dom $2 implies $2.d = local_overlapping(V,A,d,$1.d,v);
A1: for x being Element of FPrg(ND(V,A))
ex y being Element of FPrg(ND(V,A)) st P[x,y]
proof
let x be Element of FPrg(ND(V,A));
defpred Q[object,object] means $2 = local_overlapping(V,A,$1,x.$1,v);
A2: for a being object st a in dom x
ex y being object st y in ND(V,A) & Q[a,y]
proof
let a be object;
local_overlapping(V,A,a,x.a,v) in ND(V,A);
hence thesis;
end;
consider F being Function such that
A3: dom F = dom x and
A4: rng F c= ND(V,A) and
A5: for a being object st a in dom x holds Q[a,F.a] from FUNCT_1:sch 6(A2);
F is PartFunc of ND(V,A),ND(V,A) by A3,A4,RELSET_1:4,RELAT_1:def 18;
then reconsider F as Element of FPrg(ND(V,A)) by PARTFUN1:45;
take F;
thus thesis by A3,A5;
end;
consider F being Function of FPrg(ND(V,A)),FPrg(ND(V,A)) such that
A6: for x being Element of FPrg(ND(V,A)) holds P[x,F.x] from FUNCT_2:sch 3(A1);
take F;
let f be SCBinominativeFunction of V,A;
f in FPrg(ND(V,A)) by PARTFUN1:45;
hence thesis by A6;
end;
uniqueness
proof
let F,G be Function of FPrg(ND(V,A)),FPrg(ND(V,A)) such that
A7: for f being SCBinominativeFunction of V,A holds
dom(F.f) = dom f &
for d being TypeSCNominativeData of V,A holds
d in dom(F.f) implies F.f.d = local_overlapping(V,A,d,f.d,v) and
A8: for f being SCBinominativeFunction of V,A holds
dom(G.f) = dom f &
for d being TypeSCNominativeData of V,A holds
d in dom(G.f) implies G.f.d = local_overlapping(V,A,d,f.d,v);
let f be Element of FPrg(ND(V,A));
A9: f is SCBinominativeFunction of V,A by PARTFUN1:46;
hence
A10: dom(F.f) = dom f by A7
.= dom(G.f) by A8,A9;
let d be object such that
A11: d in dom(F.f);
dom(F.f) c= ND(V,A) by RELAT_1:def 18;
then
A12: d is TypeSCNominativeData of V,A by A11,NOMIN_1:39;
hence F.f.d = local_overlapping(V,A,d,f.d,v) by A7,A9,A11
.= G.f.d by A8,A9,A10,A11,A12;
end;
end;
::$N Assignment composition
definition
let V,A,v,f;
func SC_assignment(f,v) -> SCBinominativeFunction of V,A equals
SCassignment(V,A,v).f;
coherence
proof
f in FPrg(ND(V,A)) by PARTFUN1:45;
hence thesis by PARTFUN1:46,FUNCT_2:5;
end;
end;
registration
let V,A,f,v;
let d be NonatomicND of V,A;
cluster (SC_assignment(f,v)).d -> Function-like Relation-like;
coherence
proof
set a = SC_assignment(f,v);
reconsider d1 = d as TypeSCNominativeData of V,A;
per cases;
suppose d in dom a;
then a.d1 = local_overlapping(V,A,d1,f.d1,v) by Def7;
hence thesis;
end;
suppose not d in dom a;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
theorem
for d being NonatomicND of V,A holds
v in V & not d in A & not naming(V,A,v,f.d) in A & d in dom f implies
dom (SC_assignment(f,v).d) = dom d \/ {v}
proof
set a = SC_assignment(f,v);
let d be NonatomicND of V,A;
assume that
A1: v in V & not d in A & not naming(V,A,v,f.d) in A and
A2: d in dom f;
A3: dom a = dom f by Def7;
reconsider d1 = d as TypeSCNominativeData of V,A;
reconsider d2 = f.d1 as TypeSCNominativeData of V,A
by A2,PARTFUN1:4,NOMIN_1:39;
dom local_overlapping(V,A,d,d2,v) = {v} \/ dom d by A1,Th14;
hence thesis by A2,A3,Def7;
end;
::$N The composition of superposition into a predicate
definition
let V,A;
let g be (V,A)-FPrg-yielding FinSequence such that
A1: product g <> {};
let X be Function;
defpred A[object] means $1 in_doms g;
deffunc D(Function) =
{d where d is TypeSCNominativeData of V,A:
global_overlapping(V,A,d,NDentry(g,X,d)) in dom $1 & A[d]};
func SCPsuperpos(g,X) -> Function of [:Pr(ND(V,A)),product g:],Pr(ND(V,A))
means :Def9:
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
proof
defpred P[object,object,object] means
for p being SCPartialNominativePredicate of V,A
for x being Element of product g st $1 = p & $2 = x holds
for f being Function st f = $3 holds
dom(f) = D(p) &
for d being TypeSCNominativeData of V,A holds
d in dom f implies f.d = p.global_overlapping(V,A,d,NDentry(g,X,d));
A2: for x1,x2 being object st x1 in Pr(ND(V,A)) & x2 in product g
ex y being object st y in Pr(ND(V,A)) & P[x1,x2,y]
proof
let x1,x2 be object;
assume x1 in Pr(ND(V,A));
then reconsider X1 = x1 as PartFunc of ND(V,A),BOOLEAN by PARTFUN1:46;
assume x2 in product g;
defpred Q[object,object] means
for d being TypeSCNominativeData of V,A st d = $1 holds
global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 implies
$2 = X1.global_overlapping(V,A,d,NDentry(g,X,d));
A3: for a being object st a in D(X1)
ex b being object st b in BOOLEAN & Q[a,b]
proof
let a be object;
assume a in D(X1);
then consider d being TypeSCNominativeData of V,A such that
A4: d = a and
A5: global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 and
A[d];
take X1.global_overlapping(V,A,d,NDentry(g,X,d));
thus thesis by A4,A5,PARTFUN1:4;
end;
consider K being Function such that
A6: dom K = D(X1) and
A7: rng K c= BOOLEAN and
A8: for x being object st x in D(X1) holds Q[x,K.x] from FUNCT_1:sch 6(A3);
take K;
D(X1) c= ND(V,A)
proof
let x;
assume x in D(X1);
then ex d being TypeSCNominativeData of V,A st d = x &
global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 & A[d];
hence thesis;
end;
then K is PartFunc of ND(V,A),BOOLEAN by A6,A7,RELSET_1:4;
hence K in Pr(ND(V,A)) by PARTFUN1:45;
let p be SCPartialNominativePredicate of V,A;
let q be Element of product g such that
A9: x1 = p & x2 = q;
let f be Function such that
A10: f = K;
thus dom(f) = D(p) by A6,A9,A10;
let d be TypeSCNominativeData of V,A;
assume
A11: d in dom f;
then ex d1 being TypeSCNominativeData of V,A st d1 = d &
global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom X1 & A[d1] by A6,A10;
hence f.d = p.global_overlapping(V,A,d,NDentry(g,X,d))
by A6,A8,A9,A10,A11;
end;
consider F being Function of [:Pr(ND(V,A)),product g:],Pr(ND(V,A))
such that
A12: for x,y being object st x in Pr(ND(V,A)) & y in product g holds
P[x,y,F.(x,y)] from BINOP_1:sch 1(A2);
take F;
let p be SCPartialNominativePredicate of V,A;
let q be Element of product g;
A13: p in Pr(ND(V,A)) & q in product g by A1,PARTFUN1:45;
hence
A14: dom(F.(p,q)) = D(p) by A12;
let d be TypeSCNominativeData of V,A such that
A15: A[d];
thus d in dom(F.(p,q))
iff global_overlapping(V,A,d,NDentry(g,X,d)) in dom p
proof
hereby
assume d in dom(F.(p,q));
then ex d1 being TypeSCNominativeData of V,A st d = d1 &
global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom p & A[d1] by A14;
hence global_overlapping(V,A,d,NDentry(g,X,d)) in dom p;
end;
thus thesis by A14,A15;
end;
thus thesis by A12,A13;
end;
uniqueness
proof
let F,G be Function of [:Pr(ND(V,A)),product g:],Pr(ND(V,A)) such that
A16: for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds dom(F.(p,x)) = D(p) &
for d being TypeSCNominativeData of V,A st A[d] holds
F.(p,x),d =~ p,global_overlapping(V,A,d,NDentry(g,X,d)) and
A17: for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds dom(G.(p,x)) = D(p) &
for d being TypeSCNominativeData of V,A st A[d] holds
G.(p,x),d =~ p,global_overlapping(V,A,d,NDentry(g,X,d));
let a,b be set;
assume a in Pr(ND(V,A));
then reconsider p = a as SCPartialNominativePredicate of V,A
by PARTFUN1:46;
assume
A18: b in product g;
then
A19: dom(F.(a,b)) = D(p) by A16;
hence dom(F.(a,b)) = dom(G.(a,b)) by A17,A18;
let z be object;
assume
A20: z in dom(F.(a,b));
then consider d being TypeSCNominativeData of V,A such that
A21: d = z and global_overlapping(V,A,d,NDentry(g,X,d)) in dom p and
A22: A[d] by A19;
A23: G.(p,b),d =~ p,global_overlapping(V,A,d,NDentry(g,X,d)) by A17,A18,A22;
F.(p,b),d =~ p,global_overlapping(V,A,d,NDentry(g,X,d)) by A16,A18,A22;
hence thesis by A20,A23,A21;
end;
end;
::$N The composition of superposition into a predicate
definition
let V,A,p;
let g be (V,A)-FPrg-yielding FinSequence such that
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:
SCPsuperpos(g,X).(p,x);
coherence
proof
p in Pr(ND(V,A)) & x in product g by A1,PARTFUN1:45;
hence thesis by PARTFUN1:46,BINOP_1:17;
end;
end;
theorem Th33:
for g being (V,A)-FPrg-yielding FinSequence st product g <> {}
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
let g be (V,A)-FPrg-yielding FinSequence such that
A1: product g <> {};
let x be Element of product g such that
A2: d in dom(SC_Psuperpos(p,x,X));
SC_Psuperpos(p,x,X) = SCPsuperpos(g,X).(p,x) by A1,Def10;
then dom(SC_Psuperpos(p,x,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}
by A1,Def9;
then
A3: ex d1 being TypeSCNominativeData of V,A st d1 = d &
global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom p & d1 in_doms g by A2;
then SCPsuperpos(g,X).(p,x),d =~ p,global_overlapping(V,A,d,NDentry(g,X,d))
by A1,Def9;
hence thesis by A1,A3,Def10;
end;
::$N The composition of superposition into a predicate (one function)
definition
let V,A,v;
deffunc D(Function,Function) =
{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:
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
proof
defpred P[object,object,object] means
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st $1 = p & $2 = f
for F being Function st F = $3 holds
dom(F) = D(p,f) &
for d being TypeSCNominativeData of V,A holds
d in dom F implies F.d = p.local_overlapping(V,A,d,f.d,v);
A1: for x1,x2 being object st x1 in Pr(ND(V,A)) & x2 in FPrg(ND(V,A))
ex y being object st y in Pr(ND(V,A)) & P[x1,x2,y]
proof
let x1,x2 be object;
assume x1 in Pr(ND(V,A));
then reconsider X1 = x1 as PartFunc of ND(V,A),BOOLEAN by PARTFUN1:46;
assume x2 in FPrg(ND(V,A));
then reconsider X2 = x2 as PartFunc of ND(V,A),ND(V,A) by PARTFUN1:46;
defpred Q[object,object] means
for d being TypeSCNominativeData of V,A st d = $1 holds
local_overlapping(V,A,d,X2.d,v) in dom X1 implies
$2 = X1.local_overlapping(V,A,d,X2.d,v);
A2: for a being object st a in D(X1,X2)
ex b being object st b in BOOLEAN & Q[a,b]
proof
let a be object;
assume a in D(X1,X2);
then consider d being TypeSCNominativeData of V,A such that
A3: d = a & local_overlapping(V,A,d,X2.d,v) in dom X1 & d in dom X2;
take X1.local_overlapping(V,A,d,X2.d,v);
thus thesis by A3,PARTFUN1:4;
end;
consider K being Function such that
A4: dom K = D(X1,X2) and
A5: rng K c= BOOLEAN and
A6: for x being object st x in D(X1,X2) holds Q[x,K.x]
from FUNCT_1:sch 6(A2);
take K;
D(X1,X2) c= ND(V,A)
proof
let x;
assume x in D(X1,X2);
then ex d being TypeSCNominativeData of V,A st d = x &
local_overlapping(V,A,d,X2.d,v) in dom X1 & d in dom X2;
hence thesis;
end;
then K is PartFunc of ND(V,A),BOOLEAN by A4,A5,RELSET_1:4;
hence K in Pr(ND(V,A)) by PARTFUN1:45;
let p be SCPartialNominativePredicate of V,A;
let f be SCBinominativeFunction of V,A such that
A7: x1 = p & x2 = f;
let F be Function such that
A8: F = K;
thus dom(F) = D(p,f) by A4,A7,A8;
let d be TypeSCNominativeData of V,A;
assume
A9: d in dom F;
then ex d1 being TypeSCNominativeData of V,A st d1 = d &
local_overlapping(V,A,d1,X2.d1,v) in dom X1 & d1 in dom X2 by A4,A8;
hence thesis by A4,A6,A7,A8,A9;
end;
consider F being Function of [:Pr(ND(V,A)),FPrg(ND(V,A)):],Pr(ND(V,A))
such that
A10: for x,y being object st x in Pr(ND(V,A)) & y in FPrg(ND(V,A)) holds
P[x,y,F.(x,y)] from BINOP_1:sch 1(A1);
take F;
let p be SCPartialNominativePredicate of V,A;
let f be SCBinominativeFunction of V,A;
A11: p in Pr(ND(V,A)) & f in FPrg(ND(V,A)) by PARTFUN1:45;
hence
A12: dom(F.(p,f)) = D(p,f) by A10;
let d be TypeSCNominativeData of V,A such that
A13: d in dom f;
thus d in dom(F.(p,f)) iff local_overlapping(V,A,d,f.d,v) in dom p
proof
hereby
assume d in dom(F.(p,f));
then ex d1 being TypeSCNominativeData of V,A st d = d1 &
local_overlapping(V,A,d1,f.d1,v) in dom p & d1 in dom f by A12;
hence local_overlapping(V,A,d,f.d,v) in dom p;
end;
thus thesis by A12,A13;
end;
thus thesis by A10,A11;
end;
uniqueness
proof
let F,G be Function of [:Pr(ND(V,A)),FPrg(ND(V,A)):],Pr(ND(V,A)) such that
A14: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds dom(F.(p,f)) = D(p,f) &
for d being TypeSCNominativeData of V,A st d in dom f holds
F.(p,f),d =~ p,local_overlapping(V,A,d,f.d,v) and
A15: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds dom(G.(p,f)) = D(p,f) &
for d being TypeSCNominativeData of V,A st d in dom f holds
G.(p,f),d =~ p,local_overlapping(V,A,d,f.d,v);
let a,b be set;
assume a in Pr(ND(V,A));
then reconsider p = a as SCPartialNominativePredicate of V,A
by PARTFUN1:46;
assume b in FPrg(ND(V,A));
then reconsider f = b as SCBinominativeFunction of V,A by PARTFUN1:46;
A16: dom(F.(a,b)) = D(p,f) by A14;
hence dom(F.(a,b)) = dom(G.(a,b)) by A15;
let z be object;
assume z in dom(F.(a,b));
then consider d being TypeSCNominativeData of V,A such that
A17: z = d & local_overlapping(V,A,d,f.d,v) in dom p and
A18: d in dom f by A16;
A19: G.(p,f),d =~ p,local_overlapping(V,A,d,f.d,v) by A15,A18;
F.(p,f),d =~ p,local_overlapping(V,A,d,f.d,v) by A14,A18;
hence thesis by A17,A19;
end;
end;
::$N The composition of superposition into a predicate (one function)
definition
let V,A,v,p,f;
func SC_Psuperpos(p,f,v) -> SCPartialNominativePredicate of V,A equals
SCPsuperpos(V,A,v).(p,f);
coherence
proof
p in Pr(ND(V,A)) & f in FPrg(ND(V,A)) by PARTFUN1:45;
hence thesis by PARTFUN1:46,BINOP_1:17;
end;
end;
theorem Th34:
d in dom(SC_Psuperpos(p,f,v)) implies
SC_Psuperpos(p,f,v).d = p.local_overlapping(V,A,d,f.d,v) & d in dom f
proof
set F = SC_Psuperpos(p,f,v);
assume
A1: d in dom(F);
dom(F) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,f.d,v) in dom p & d in dom f} by Def11;
then
A2: ex d1 being TypeSCNominativeData of V,A st d1 = d &
local_overlapping(V,A,d1,f.d1,v) in dom p & d1 in dom f
by A1;
then F,d =~ p,local_overlapping(V,A,d,f.d,v) by Def11;
hence thesis by A2;
end;
theorem
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
set g = <*f*>;
let x be Element of product g;
assume that
A1: v in V and
A2: product g <> {};
set X = <*v*>;
set S1 = SC_Psuperpos(p,f,v);
set S2 = SC_Psuperpos(p,x,X);
defpred A[object] means $1 in_doms g;
A3: g.1 = f;
A4: dom g = {1} by FINSEQ_1:2,38;
A5: dom(S1) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,f.d,v) in dom p & d in dom f} by Def11;
S2 = SCPsuperpos(g,X).(p,x) by A2,Def10;
then
A6: dom(S2) = {d where d is TypeSCNominativeData of V,A:
global_overlapping(V,A,d,NDentry(g,X,d)) in dom p & A[d]} by A2,Def9;
thus
A7: dom S1 = dom S2
proof
thus dom S1 c= dom S2
proof
let a be object;
assume a in dom S1;
then consider d such that
A8: d = a and
A9: local_overlapping(V,A,d,f.d,v) in dom p and
A10: d in dom f by A5;
A11: A[d]
proof
let x;
thus thesis by A10,A3,A4,TARSKI:def 1;
end;
NDentry(g,X,d) = naming(V,A,v,f.d) by A1,A10,Th26;
hence thesis by A8,A9,A11,A6;
end;
let a be object;
assume a in dom S2;
then consider d such that
A12: a = d and
A13: global_overlapping(V,A,d,NDentry(g,X,d)) in dom p and
A14: A[d] by A6;
1 in dom g by A4,TARSKI:def 1;
then
A15: d in dom(g.1) by A14,Def3;
then local_overlapping(V,A,d,f.d,v) in dom p by A1,Th26,A13;
hence thesis by A5,A12,A15;
end;
let a be object;
assume
A16: a in dom S1;
then consider d such that
A17: d = a and
local_overlapping(V,A,d,f.d,v) in dom p and
A18: d in dom f by A5;
NDentry(g,X,d) = naming(V,A,v,f.d) by A1,A18,Th26;
hence S2.a = p.local_overlapping(V,A,d,f.d,v) by A7,A16,A17,A2,Th33
.= S1.a by A16,A17,Th34;
end;
::$N The composition of superposition into a function
definition
let V,A;
let g be (V,A)-FPrg-yielding FinSequence such that
A1: product g <> {};
let X be Function;
defpred A[object] means $1 in_doms g;
deffunc D(Function) =
{d where d is TypeSCNominativeData of V,A:
global_overlapping(V,A,d,NDentry(g,X,d)) in dom $1 & A[d]};
func SCFsuperpos(g,X) ->
Function of [:FPrg(ND(V,A)),product g:],FPrg(ND(V,A))
means :Def13:
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
proof
defpred P[object,object,object] means
for f being SCBinominativeFunction of V,A
for x being Element of product g st $1 = f & $2 = x holds
for h being Function st h = $3 holds
dom(h) = D(f) &
for d being TypeSCNominativeData of V,A holds
d in dom h implies h.d = f.global_overlapping(V,A,d,NDentry(g,X,d));
A2: for x1,x2 being object st x1 in FPrg(ND(V,A)) & x2 in product g
ex y being object st y in FPrg(ND(V,A)) & P[x1,x2,y]
proof
let x1,x2 be object;
assume x1 in FPrg(ND(V,A));
then reconsider X1 = x1 as PartFunc of ND(V,A),ND(V,A) by PARTFUN1:46;
assume x2 in product g;
defpred Q[object,object] means
for d being TypeSCNominativeData of V,A st d = $1 holds
global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 implies
$2 = X1.global_overlapping(V,A,d,NDentry(g,X,d));
A3: for a being object st a in D(X1)
ex b being object st b in ND(V,A) & Q[a,b]
proof
let a be object;
assume a in D(X1);
then consider d being TypeSCNominativeData of V,A such that
A4: d = a & global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 & A[d];
take X1.global_overlapping(V,A,d,NDentry(g,X,d));
thus thesis by A4,PARTFUN1:4;
end;
consider K being Function such that
A5: dom K = D(X1) and
A6: rng K c= ND(V,A) and
A7: for x being object st x in D(X1) holds Q[x,K.x] from FUNCT_1:sch 6(A3);
take K;
D(X1) c= ND(V,A)
proof
let x;
assume x in D(X1);
then ex d being TypeSCNominativeData of V,A st d = x &
global_overlapping(V,A,d,NDentry(g,X,d)) in dom X1 & A[d];
hence thesis;
end;
then K is PartFunc of ND(V,A),ND(V,A) by A5,A6,RELSET_1:4;
hence K in FPrg(ND(V,A)) by PARTFUN1:45;
let f be SCBinominativeFunction of V,A;
let q be Element of product g such that
A8: x1 = f & x2 = q;
let h be Function such that
A9: h = K;
thus dom(h) = D(f) by A5,A8,A9;
let d be TypeSCNominativeData of V,A;
assume
A10: d in dom h;
then ex d1 being TypeSCNominativeData of V,A st d1 = d &
global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom X1 & A[d1] by A5,A9;
hence h.d = f.global_overlapping(V,A,d,NDentry(g,X,d))
by A5,A7,A8,A9,A10;
end;
consider F being Function of [:FPrg(ND(V,A)),product g:],FPrg(ND(V,A))
such that
A11: for x,y being object st x in FPrg(ND(V,A)) & y in product g holds
P[x,y,F.(x,y)] from BINOP_1:sch 1(A2);
take F;
let f be SCBinominativeFunction of V,A;
let q be Element of product g;
A12: f in FPrg(ND(V,A)) & q in product g by A1,PARTFUN1:45;
hence
A13: dom(F.(f,q)) = D(f) by A11;
let d be TypeSCNominativeData of V,A such that
A14: A[d];
thus d in dom(F.(f,q))
iff global_overlapping(V,A,d,NDentry(g,X,d)) in dom f
proof
hereby
assume d in dom(F.(f,q));
then ex d1 being TypeSCNominativeData of V,A st d = d1 &
global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom f & A[d1] by A13;
hence global_overlapping(V,A,d,NDentry(g,X,d)) in dom f;
end;
thus thesis by A13,A14;
end;
thus thesis by A11,A12;
end;
uniqueness
proof
let F,G be Function of [:FPrg(ND(V,A)),product g:],FPrg(ND(V,A)) such that
A15: for f being SCBinominativeFunction of V,A
for x being Element of product g holds dom(F.(f,x)) = D(f) &
for d being TypeSCNominativeData of V,A st d in_doms g holds
F.(f,x),d =~ f,global_overlapping(V,A,d,NDentry(g,X,d)) and
A16: for f being SCBinominativeFunction of V,A
for x being Element of product g holds dom(G.(f,x)) = D(f) &
for d being TypeSCNominativeData of V,A st d in_doms g holds
G.(f,x),d =~ f,global_overlapping(V,A,d,NDentry(g,X,d));
let a,b be set;
assume a in FPrg(ND(V,A));
then reconsider f = a as SCBinominativeFunction of V,A by PARTFUN1:46;
assume
A17: b in product g;
then
A18: dom(F.(a,b)) = D(f) by A15;
hence dom(F.(a,b)) = dom(G.(a,b)) by A16,A17;
let z be object;
assume z in dom(F.(a,b));
then consider d being TypeSCNominativeData of V,A such that
A19: z = d & global_overlapping(V,A,d,NDentry(g,X,d)) in dom f & A[d] by A18;
A20: G.(f,b),d =~ f,global_overlapping(V,A,d,NDentry(g,X,d)) by A16,A17,A19;
F.(f,b),d =~ f,global_overlapping(V,A,d,NDentry(g,X,d)) by A15,A17,A19;
hence thesis by A19,A20;
end;
end;
::$N The composition of superposition into a function
definition
let V,A,f;
let g be (V,A)-FPrg-yielding FinSequence such that
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:
SCFsuperpos(g,X).(f,x);
coherence
proof
f in FPrg(ND(V,A)) & x in product g by A1,PARTFUN1:45;
hence thesis by PARTFUN1:46,BINOP_1:17;
end;
end;
theorem Th36:
for g being (V,A)-FPrg-yielding FinSequence st product g <> {}
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
let g be (V,A)-FPrg-yielding FinSequence such that
A1: product g <> {};
let x be Element of product g such that
A2: d in dom(SC_Fsuperpos(f,x,X));
A3: dom(SCFsuperpos(g,X).(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}
by A1,Def13;
SC_Fsuperpos(f,x,X) = SCFsuperpos(g,X).(f,x) by A1,Def14;
then
A4: ex d1 being TypeSCNominativeData of V,A st d1 = d &
(global_overlapping(V,A,d1,NDentry(g,X,d1)) in dom f & d1 in_doms g)
by A2,A3;
then SCFsuperpos(g,X).(f,x),d =~ f,global_overlapping(V,A,d,NDentry(g,X,d))
by A1,Def13;
hence thesis by A1,A4,Def14;
end;
::$N The composition of superposition into a function (one function)
definition
let V,A,v;
deffunc D(Function,Function) =
{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:
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
proof
defpred P[object,object,object] means
for f,g being SCBinominativeFunction of V,A st $1 = f & $2 = g
for F being Function st F = $3 holds dom(F) = D(f,g) &
for d being TypeSCNominativeData of V,A holds
d in dom F implies F.d = f.local_overlapping(V,A,d,g.d,v);
A1: for x1,x2 being object st x1 in FPrg(ND(V,A)) & x2 in FPrg(ND(V,A))
ex y being object st y in FPrg(ND(V,A)) & P[x1,x2,y]
proof
let x1,x2 be object;
assume x1 in FPrg(ND(V,A));
then reconsider X1 = x1 as PartFunc of ND(V,A),ND(V,A) by PARTFUN1:46;
assume x2 in FPrg(ND(V,A));
then reconsider X2 = x2 as PartFunc of ND(V,A),ND(V,A) by PARTFUN1:46;
defpred Q[object,object] means
for d being TypeSCNominativeData of V,A st d = $1 holds
local_overlapping(V,A,d,X2.d,v) in dom X1 implies
$2 = X1.local_overlapping(V,A,d,X2.d,v);
A2: for a being object st a in D(X1,X2)
ex b being object st b in ND(V,A) & Q[a,b]
proof
let a be object;
assume a in D(X1,X2);
then consider d being TypeSCNominativeData of V,A such that
A3: d = a & local_overlapping(V,A,d,X2.d,v) in dom X1 & d in dom X2;
take X1.local_overlapping(V,A,d,X2.d,v);
thus thesis by A3,PARTFUN1:4;
end;
consider K being Function such that
A4: dom K = D(X1,X2) and
A5: rng K c= ND(V,A) and
A6: for x being object st x in D(X1,X2) holds Q[x,K.x]
from FUNCT_1:sch 6(A2);
take K;
D(X1,X2) c= ND(V,A)
proof
let x;
assume x in D(X1,X2);
then ex d being TypeSCNominativeData of V,A st d = x &
local_overlapping(V,A,d,X2.d,v) in dom X1 & d in dom X2;
hence thesis;
end;
then K is PartFunc of ND(V,A),ND(V,A) by A4,A5,RELSET_1:4;
hence K in FPrg(ND(V,A)) by PARTFUN1:45;
let f,g be SCBinominativeFunction of V,A such that
A7: x1 = f & x2 = g;
let F be Function such that
A8: F = K;
thus dom(F) = D(f,g) by A4,A7,A8;
let d be TypeSCNominativeData of V,A;
assume
A9: d in dom F;
then ex d1 being TypeSCNominativeData of V,A st d1 = d &
local_overlapping(V,A,d1,X2.d1,v) in dom X1 & d1 in dom X2 by A4,A8;
hence thesis by A4,A6,A7,A8,A9;
end;
consider F being Function of [:FPrg(ND(V,A)),FPrg(ND(V,A)):],FPrg(ND(V,A))
such that
A10: for x,y being object st x in FPrg(ND(V,A)) & y in FPrg(ND(V,A)) holds
P[x,y,F.(x,y)] from BINOP_1:sch 1(A1);
take F;
let f,g;
A11: f in FPrg(ND(V,A)) & g in FPrg(ND(V,A)) by PARTFUN1:45;
hence
A12: dom(F.(f,g)) = D(f,g) by A10;
let d be TypeSCNominativeData of V,A such that
A13: d in dom g;
thus d in dom(F.(f,g)) iff local_overlapping(V,A,d,g.d,v) in dom f
proof
hereby
assume d in dom(F.(f,g));
then ex d1 being TypeSCNominativeData of V,A st d = d1 &
local_overlapping(V,A,d1,g.d1,v) in dom f & d1 in dom g by A12;
hence local_overlapping(V,A,d,g.d,v) in dom f;
end;
thus thesis by A12,A13;
end;
thus thesis by A10,A11;
end;
uniqueness
proof
let F,G be Function of [:FPrg(ND(V,A)),FPrg(ND(V,A)):],FPrg(ND(V,A))
such that
A14: for f,g being SCBinominativeFunction of V,A holds dom(F.(f,g)) = D(f,g) &
for d being TypeSCNominativeData of V,A st d in dom g holds
F.(f,g),d =~ f,local_overlapping(V,A,d,g.d,v) and
A15: for f,g being SCBinominativeFunction of V,A holds dom(G.(f,g)) = D(f,g) &
for d being TypeSCNominativeData of V,A st d in dom g holds
G.(f,g),d =~ f,local_overlapping(V,A,d,g.d,v);
let a,b be set;
assume a in FPrg(ND(V,A));
then reconsider f = a as SCBinominativeFunction of V,A by PARTFUN1:46;
assume b in FPrg(ND(V,A));
then reconsider g = b as SCBinominativeFunction of V,A by PARTFUN1:46;
A16: dom(F.(a,b)) = D(f,g) by A14;
hence dom(F.(a,b)) = dom(G.(a,b)) by A15;
let z be object;
assume z in dom(F.(a,b));
then consider d being TypeSCNominativeData of V,A such that
A17: z = d & local_overlapping(V,A,d,g.d,v) in dom f and
A18: d in dom g by A16;
A19: G.(f,g),d =~ f,local_overlapping(V,A,d,g.d,v) by A15,A18;
F.(f,g),d =~ f,local_overlapping(V,A,d,g.d,v) by A14,A18;
hence thesis by A17,A19;
end;
end;
::$N The composition of superposition into a function (one function)
definition
let V,A,v,f,g;
func SC_Fsuperpos(f,g,v) -> SCBinominativeFunction of V,A equals
SCFsuperpos(V,A,v).(f,g);
coherence
proof
f in FPrg(ND(V,A)) & g in FPrg(ND(V,A)) by PARTFUN1:45;
hence thesis by PARTFUN1:46,BINOP_1:17;
end;
end;
theorem Th37:
d in dom(SC_Fsuperpos(f,g,v)) implies
SC_Fsuperpos(f,g,v).d = f.local_overlapping(V,A,d,g.d,v) & d in dom g
proof
set F = SC_Fsuperpos(f,g,v);
assume
A1: d in dom(F);
dom(F) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,g.d,v) in dom f & d in dom g} by Def15;
then
A2: ex d1 being TypeSCNominativeData of V,A st d1 = d &
(local_overlapping(V,A,d1,g.d1,v) in dom f & d1 in dom g) by A1;
F,d =~ f,local_overlapping(V,A,d,g.d,v) by A2,Def15;
hence thesis by A2;
end;
theorem
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
set G = <*g*>;
let x be Element of product G;
assume that
A1: v in V and
A2: product G <> {};
set X = <*v*>;
set S1 = SC_Fsuperpos(f,g,v);
set S2 = SC_Fsuperpos(f,x,X);
defpred A[object] means $1 in_doms G;
A3: G.1 = g;
A4: dom G = {1} by FINSEQ_1:2,38;
A5: dom(S1) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,g.d,v) in dom f & d in dom g} by Def15;
S2 = SCFsuperpos(G,X).(f,x) by A2,Def14;
then
A6: dom(S2) = {d where d is TypeSCNominativeData of V,A:
global_overlapping(V,A,d,NDentry(G,X,d)) in dom f & A[d]} by A2,Def13;
thus
A7: dom S1 = dom S2
proof
thus dom S1 c= dom S2
proof
let a be object;
assume a in dom S1;
then consider d such that
A8: d = a and
A9: local_overlapping(V,A,d,g.d,v) in dom f and
A10: d in dom g by A5;
A11: A[d]
proof
let x;
thus thesis by A10,A3,A4,TARSKI:def 1;
end;
NDentry(G,X,d) = naming(V,A,v,g.d) by A1,A10,Th26;
hence thesis by A8,A9,A11,A6;
end;
let a be object;
assume a in dom S2;
then consider d such that
A12: a = d and
A13: global_overlapping(V,A,d,NDentry(G,X,d)) in dom f and
A14: A[d] by A6;
1 in dom G by A4,TARSKI:def 1;
then
A15: d in dom(G.1) by A14,Def3;
then local_overlapping(V,A,d,g.d,v) in dom f by A1,Th26,A13;
hence thesis by A5,A12,A15;
end;
let a be object;
assume
A16: a in dom S1;
then consider d such that
A17: d = a and
local_overlapping(V,A,d,g.d,v) in dom f and
A18: d in dom g by A5;
NDentry(G,X,d) = naming(V,A,v,g.d) by A1,A18,Th26;
hence S2.a = f.local_overlapping(V,A,d,g.d,v) by A7,A16,A17,A2,Th36
.= S1.a by A16,A17,Th37;
end;
::$N Name checking predicate
definition
let V,A,v;
defpred P[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
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
proof
A1: ND(V,A) \ A c= ND(V,A);
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) \ A and
A3: for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE)
from PARTPR_2:sch 1(A1);
take p;
thus dom p = ND(V,A) \ A by A2;
let d be NonatomicND of V,A such that
A4: d in dom p;
thus denaming(v,d) in dom p implies p.d = TRUE by A2,A3,A4;
assume not denaming(v,d) in dom p;
then not P[d] by A2;
hence thesis by A3,A4;
end;
uniqueness
proof
let F,G be SCPartialNominativePredicate of V,A such that
A5: dom F = ND(V,A) \ A and
A6: for d being NonatomicND of V,A st d in dom F holds
(denaming(v,d) in dom F implies F.d = TRUE) &
(not denaming(v,d) in dom F implies F.d = FALSE) and
A7: dom G = ND(V,A) \ A and
A8: for d being NonatomicND of V,A st d in dom G holds
(denaming(v,d) in dom G implies G.d = TRUE) &
(not denaming(v,d) in dom G implies G.d = FALSE);
thus dom F = dom G by A5,A7;
let x;
assume
A9: x in dom F;
then reconsider d = x as NonatomicND of V,A by A5,NOMIN_1:43;
per cases;
suppose
A10: denaming(v,d) in dom F;
hence F.x = TRUE by A6,A9
.= G.x by A5,A7,A8,A9,A10;
end;
suppose
A11: not denaming(v,d) in dom F;
hence F.x = FALSE by A6,A9
.= G.x by A5,A7,A8,A9,A11;
end;
end;
end;