:: Introduction to Circuits, II
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received April 10, 1995
:: Copyright (c) 1995-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 MSAFREE2, STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE,
FUNCOP_1, FUNCT_1, TREES_3, FINSEQ_1, SUBSET_1, TREES_4, MSUALG_3,
MARGREL1, FINSEQ_4, TARSKI, DTCONSTR, NAT_1, NUMBERS, TREES_2, CARD_3,
PARTFUN1, ZFMISC_1, TDGROUP, CIRCUIT1, FSM_1, FUNCT_4, GLIB_000,
UNIALG_2, MSATERM, PRELAMB, REALSET1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_6,
TREES_A, FINSET_1, CIRCUIT2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, XXREAL_0, XCMPLX_0, NAT_1,
FINSEQ_1, FINSEQ_2, FINSET_1, TREES_2, TREES_3, TREES_4, CARD_3, FUNCT_6,
LANG1, DTCONSTR, PBOOLE, FUNCOP_1, XXREAL_2, STRUCT_0, PRALG_1, MSUALG_1,
MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, MSATERM;
constructors PRALG_1, MSUALG_3, MSATERM, CIRCUIT1, SEQ_4, RELSET_1, FUNCT_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, MEMBERED, FINSEQ_1, CARD_3, TREES_3, PRE_CIRC, STRUCT_0,
MSUALG_1, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, XXREAL_2, CARD_1,
RELSET_1, PBOOLE;
requirements NUMERALS, BOOLE, SUBSET;
definitions PBOOLE;
equalities MSAFREE2;
expansions PBOOLE, MSAFREE2;
theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RELAT_1, GRFUNC_1,
FUNCT_1, FUNCT_2, FUNCT_4, TREES_3, TREES_4, DTCONSTR, FUNCT_6, ZFMISC_1,
CARD_3, MSATERM, PARTFUN2, FUNCOP_1, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2,
MSUALG_3, MSAFREE, PRE_CIRC, MSAFREE2, CIRCUIT1, TREES_1, EXTENS_1,
RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, XXREAL_0, PARTFUN1, XXREAL_2,
CARD_1, XTUPLE_0;
schemes NAT_1, FINSEQ_1, PRE_CIRC, PBOOLE;
begin
reserve IIG for monotonic Circuit-like non void non empty ManySortedSign;
Lm1: for x being set holds not x in x;
theorem Th1:
for X being non-empty ManySortedSet of the carrier of IIG,
H being ManySortedFunction of FreeMSA X, FreeMSA X,
HH being Function-yielding Function,
v being SortSymbol of IIG,
p being DTree-yielding FinSequence,
t being Element of (the Sorts of FreeMSA X).v st
v in InnerVertices IIG & t = [action_at v,the carrier of IIG]-tree p &
H is_homomorphism FreeMSA X, FreeMSA X
& HH = H * the_arity_of action_at v ex HHp being DTree-yielding FinSequence st
HHp = HH..p & H.v.t = [action_at v,the carrier of IIG]-tree HHp
proof
let X be non-empty ManySortedSet of the carrier of IIG, H be
ManySortedFunction of FreeMSA X, FreeMSA X, HH be Function-yielding Function, v
be SortSymbol of IIG, p be DTree-yielding FinSequence, t be Element of (the
Sorts of FreeMSA X).v such that
A1: v in InnerVertices IIG and
A2: t = [action_at v,the carrier of IIG]-tree p and
A3: H is_homomorphism FreeMSA X, FreeMSA X and
A4: HH = H * the_arity_of action_at v;
reconsider av = action_at v as OperSymbol of IIG;
A5: the_result_sort_of av = v by A1,MSAFREE2:def 7;
then len p = len the_arity_of av by A2,MSAFREE2:10;
then
A6: dom p = dom the_arity_of av by FINSEQ_3:29;
A7: rng the_arity_of av c= the carrier of IIG by FINSEQ_1:def 4; then
A8: rng the_arity_of av c= dom H by PARTFUN1:def 2; then
A9: dom the_arity_of av = dom HH by A4,RELAT_1:27;
A10: FreeMSA X = MSAlgebra (# FreeSort X, FreeOper X #) by MSAFREE:def 14;
then (the Sorts of FreeMSA X).v = FreeSort(X,v) by MSAFREE:def 11;
then [av,the carrier of IIG]-tree p in FreeSort(X,v) by A2;
then
A11: [av,the carrier of IIG]-tree p in {a where a is Element of TS(DTConMSA(
X)): (ex x be set st x in X.v & a = root-tree [x,v]) or ex o be OperSymbol of
IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v}
by MSAFREE:def 10;
reconsider HHp = HH..p as Function;
A12: dom HHp = dom HH /\ dom p by PRALG_1:def 19
.= dom HH by A6,A9;
H * the_arity_of av is FinSequence by A8,FINSEQ_1:16;
then ex n being Nat st dom HH = Seg n by A4,FINSEQ_1:def 2;
then reconsider HHp as FinSequence by A12,FINSEQ_1:def 2;
A13: now
reconsider HH9 = HH as FinSequence by A4,A8,FINSEQ_1:16;
let x9 be object;
set x = HHp.x9;
reconsider g = HH.x9 as Function;
assume
A14: x9 in dom HHp;
then reconsider k = x9 as Element of NAT;
A15: x = g.(p.k) by A14,PRALG_1:def 19;
len HH9 = len the_arity_of av by A4,A8,FINSEQ_2:29;
then
A16: dom HH9 = dom the_arity_of av by FINSEQ_3:29;
then reconsider s = (the_arity_of av).k as SortSymbol of IIG
by A12,A14,FINSEQ_2:11;
g = H.s by A4,A12,A14,A16,FUNCT_1:13;
then x in (the Sorts of FreeMSA X).s
by A2,A12,A5,A14,A16,A15,FUNCT_2:5,MSAFREE2:11;
hence x is DecoratedTree;
end;
set f = (the Sorts of FreeMSA X)*(the_arity_of av);
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1; then
A17: ((the Sorts of FreeMSA X)# * the Arity of IIG).av = (the Sorts of
FreeMSA X)#.((the Arity of IIG).av) by FUNCT_1:13
.= (the Sorts of FreeMSA X)#.(the_arity_of av) by MSUALG_1:def 1
.= product((the Sorts of FreeMSA X)*(the_arity_of av)) by FINSEQ_2:def 5;
reconsider HHp as DTree-yielding FinSequence by A13,TREES_3:24;
consider a being Element of TS(DTConMSA(X)) such that
A18: a = [av,the carrier of IIG]-tree p and
A19: (ex x be set st x in X.v & a = root-tree [x,v]) or ex o be
OperSymbol of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v
by A11;
consider x9 being set such that
A20: x9 in X.v & a = root-tree [x9,v] or ex o being OperSymbol of IIG st
[o,the carrier of IIG] = a.{} & the_result_sort_of o = v by A19;
dom the Sorts of FreeMSA X = the carrier of IIG by PARTFUN1:def 2; then
A21: dom f = dom the_arity_of av by A7,RELAT_1:27;
now
let x be object;
assume
A22: x in dom f;
then reconsider n = x as Element of NAT by A21;
(the_arity_of av).x in rng the_arity_of av by A21,A22,FUNCT_1:def 3;
then reconsider s = (the_arity_of av).x as SortSymbol of IIG by A7;
n in dom (the_arity_of av) & ((the Sorts of FreeMSA X)*(the_arity_of
av)).x = (the Sorts of FreeMSA X).s by A21,A22,FUNCT_1:13;
hence p.x in f.x by A2,A5,MSAFREE2:11;
end;
then p in ((the Sorts of FreeMSA X)# * the Arity of IIG).av
by A17,A21,A6,CARD_3:def 5;
then reconsider x = p as Element of Args(av, FreeMSA X) by MSUALG_1:def 4;
A23: a.{} = [av,the carrier of IIG] by A18,TREES_4:def 4;
reconsider Hx = H#x as Function;
A24: now
let x9 be set;
assume
A25: x9 in dom HH;
then reconsider n = x9 as Element of NAT by A9;
(the_arity_of av).n in rng the_arity_of av by A9,A25,FUNCT_1:def 3;
then reconsider s = (the_arity_of av).n as SortSymbol of IIG by A7;
Hx.n = (H.((the_arity_of av)/.n)).(p.n) by A9,A6,A25,MSUALG_3:def 6
.= (H.s).(p.n) by A9,A25,PARTFUN1:def 6;
hence Hx.x9 = (HH.x9).(p.x9) by A4,A9,A25,FUNCT_1:13;
end;
AA: dom Hx = dom HH by A9,MSUALG_3:6
.= dom HH /\ dom p by A12,PRALG_1:def 19;
A26: HHp = Hx by PRALG_1:def 19,AA,A24,A6,A9;
now
assume a = root-tree [x9,v]; then
A27: a.{} = [x9,v] by TREES_4:3;
a.{} = [av,the carrier of IIG] by A18,TREES_4:def 4;
then the carrier of IIG = v by A27,XTUPLE_0:1;
hence contradiction by Lm1;
end;
then consider o being OperSymbol of IIG such that
A28: [o,the carrier of IIG] = a.{} and
the_result_sort_of o = v by A20;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then [o,the carrier of IIG] in [:the carrier' of IIG,{the carrier of IIG}:]
by ZFMISC_1:87;
then reconsider
nt = [o,the carrier of IIG] as NonTerminal of DTConMSA(X) by MSAFREE:6;
consider ts being FinSequence of TS(DTConMSA(X)) such that
A29: a = nt-tree ts and
A30: nt ==> roots ts by A28,DTCONSTR:10;
take HHp;
thus HHp = HH..p;
A31: Sym(av, X) = [av,the carrier of IIG] by MSAFREE:def 9;
now
let x be object;
reconsider g = HH.x as Function;
assume
A32: x in dom f;
dom ((the Sorts of FreeMSA X)*(the_arity_of av)) c=
dom the_arity_of av by RELAT_1:25; then
A33: HHp.x = g.(p.x) by A32,A9,A12,PRALG_1:def 19;
(the_arity_of av).x in rng the_arity_of av by A21,A32,FUNCT_1:def 3;
then reconsider s = (the_arity_of av).x as SortSymbol of IIG by A7;
A34: the_result_sort_of av = v by A1,MSAFREE2:def 7;
((the Sorts of FreeMSA X)*(the_arity_of av)).x = (the Sorts of
FreeMSA X).s & g = H.s by A4,A21,A32,FUNCT_1:13;
hence HHp.x in f.x by A2,A21,A32,A34,A33,FUNCT_2:5,MSAFREE2:11;
end; then
A35: HHp in ((FreeSort X)# * (the Arity of IIG)).av by A12,A17,A21,A9,A10,
CARD_3:def 5;
then reconsider HHp9 = HHp as FinSequence of TS(DTConMSA(X)) by MSAFREE:8;
A36: Sym(av, X) ==> roots HHp9 by A35,MSAFREE:10;
reconsider p9 = p as FinSequence of TS(DTConMSA(X)) by A18,A29,TREES_4:15;
ts = p by A18,A29,TREES_4:15;
then
A37: DenOp(av, X).p9 = t by A2,A28,A23,A30,A31,MSAFREE:def 12;
Den(av, FreeMSA X) = (FreeOper X).av by A10,MSUALG_1:def 6
.= DenOp(av, X) by MSAFREE:def 13;
hence H.v.t = DenOp(av, X).HHp by A3,A5,A37,A26,MSUALG_3:def 7
.= [action_at v,the carrier of IIG]-tree HHp by A31,A36,MSAFREE:def 12;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS,
iv be InputValues of SCS;
redefine func s +* iv -> State of SCS; :: redefines +* (FUNCT_4, definition)
coherence
proof
A1: dom iv = InputVertices IIG by PARTFUN1:def 2;
then dom the Sorts of SCS = the carrier of IIG & for x be set st x in dom
iv holds iv.x in (the Sorts of SCS).x by MSAFREE2:def 5,PARTFUN1:def 2;
hence thesis by A1,PRE_CIRC:6;
end;
end;
definition
let IIG;
let A be non-empty Circuit of IIG, iv be InputValues of A;
func Fix_inp iv -> ManySortedFunction of FreeGen the Sorts of A, the Sorts
of FreeEnv A means
:Def1:
for v being Vertex of IIG holds (v in InputVertices
IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]) & (v in
SortsWithConstants IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree
[action_at v,the carrier of IIG]) & (v in (InnerVertices IIG \
SortsWithConstants IIG) implies it.v = id FreeGen(v, the Sorts of A));
existence
proof
defpred P[object,object] means
ex v being Vertex of IIG st v = $1 & ($1 in
InputVertices IIG implies $2 = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v
]) & ($1 in SortsWithConstants IIG implies $2 = FreeGen(v, the Sorts of A) -->
root-tree [action_at v,the carrier of IIG]) & ($1 in (InnerVertices IIG \
SortsWithConstants IIG) implies $2 = id FreeGen(v, the Sorts of A));
A1: now
let i be object;
assume
A2: i in the carrier of IIG;
then reconsider v = i as Vertex of IIG;
v in InputVertices IIG \/ InnerVertices IIG by A2,XBOOLE_1:45;
then
A3: v in InputVertices IIG or v in InnerVertices IIG by XBOOLE_0:def 3;
A4: (InnerVertices IIG \ SortsWithConstants IIG) \/ SortsWithConstants
IIG = InnerVertices IIG by MSAFREE2:3,XBOOLE_1:45;
thus ex j being object st P[i,j]
proof
per cases by A4,A3,XBOOLE_0:def 3;
suppose
A5: v in InputVertices IIG;
reconsider j = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v] as
set;
take j,v;
thus v = i;
thus i in InputVertices IIG implies j = FreeGen(v, the Sorts of A)
--> root-tree[iv.v, v];
thus i in SortsWithConstants IIG implies
j = FreeGen(v, the Sorts of A) --> root-tree [action_at v,the
carrier of IIG] by A5,MSAFREE2:4,XBOOLE_0:3;
A6: InnerVertices IIG \ SortsWithConstants IIG c= InnerVertices IIG
& InputVertices IIG misses InnerVertices IIG by XBOOLE_1:36,79;
assume i in InnerVertices IIG \ SortsWithConstants IIG;
hence thesis by A5,A6,XBOOLE_0:3;
end;
suppose
A7: v in SortsWithConstants IIG;
reconsider j = FreeGen(v, the Sorts of A) --> root-tree [action_at v
,the carrier of IIG] as set;
take j,v;
thus v = i;
thus i in InputVertices IIG implies
j = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]
by A7,MSAFREE2:4,XBOOLE_0:3;
thus i in SortsWithConstants IIG implies j = FreeGen(v, the Sorts of
A) --> root-tree [action_at v,the carrier of IIG];
A8: InnerVertices IIG \ SortsWithConstants IIG misses
SortsWithConstants IIG by XBOOLE_1:79;
assume i in InnerVertices IIG \ SortsWithConstants IIG;
hence thesis by A7,A8,XBOOLE_0:3;
end;
suppose
A9: v in InnerVertices IIG \ SortsWithConstants IIG;
reconsider j = id FreeGen(v, the Sorts of A) as set;
take j,v;
thus v = i;
hereby
A10: InnerVertices IIG \ SortsWithConstants IIG c= InnerVertices
IIG & InputVertices IIG misses InnerVertices IIG by XBOOLE_1:36,79;
assume i in InputVertices IIG;
hence
j = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v] by A9,A10,
XBOOLE_0:3;
end;
thus i in SortsWithConstants IIG implies
j = FreeGen(v, the Sorts of A) --> root-tree [action_at v,the
carrier of IIG] by A9,XBOOLE_0:3,XBOOLE_1:79;
assume i in InnerVertices IIG \ SortsWithConstants IIG;
thus thesis;
end;
end;
end;
consider M being ManySortedSet of the carrier of IIG such that
A11: for i being object st i in the carrier of IIG holds P[i,M.i] from
PBOOLE:sch 3(A1);
A12: now
let i be object;
A13: (InnerVertices IIG \ SortsWithConstants IIG) \/ SortsWithConstants
IIG = InnerVertices IIG by MSAFREE2:3,XBOOLE_1:45;
assume
A14: i in the carrier of IIG;
then reconsider v = i as Vertex of IIG;
v in InputVertices IIG \/ InnerVertices IIG by A14,XBOOLE_1:45;
then
A15: v in InputVertices IIG or v in InnerVertices IIG by XBOOLE_0:def 3;
A16: FreeGen(v, the Sorts of A) = (FreeGen the Sorts of A).v by MSAFREE:def 16
;
A17: FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the
Sorts of A#) by MSAFREE:def 14;
per cases by A13,A15,XBOOLE_0:def 3;
suppose
A18: v in InputVertices IIG;
then iv.v in (the Sorts of A).v by MSAFREE2:def 5;
then
A19: root-tree[iv.v, v] in FreeGen(v, the Sorts of A) by MSAFREE:def 15;
P[v,M.v] by A11;
hence M.i is Function of (FreeGen the Sorts of A).i, (the Sorts of
FreeEnv A).i by A16,A17,A18,A19,FUNCOP_1:45;
end;
suppose
A20: v in SortsWithConstants IIG;
reconsider sy = Sym(action_at v, the Sorts of A) as NonTerminal of
DTConMSA the Sorts of A;
set p = <*>TS(DTConMSA the Sorts of A);
set e = root-tree [action_at v,the carrier of IIG];
A21: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
v in { s where s is SortSymbol of IIG : s is with_const_op } by A20,
MSAFREE2:def 1;
then ex s being SortSymbol of IIG st v = s & s is with_const_op;
then consider o being OperSymbol of IIG such that
A22: (the Arity of IIG).o = {} and
A23: (the ResultSort of IIG).o = v by MSUALG_2:def 1;
A24: for n be Nat st n in dom p holds p.n in FreeSort(the Sorts of A,(
the_arity_of o)/.n qua SortSymbol of IIG);
p = the_arity_of o by A22,MSUALG_1:def 1;
then
A25: p in ((FreeSort the Sorts of A)# * (the Arity of IIG)).o by A24,
MSAFREE:9;
the_result_sort_of o = v by A23,MSUALG_1:def 2;
then o = action_at v by A20,A21,MSAFREE2:def 7;
then sy ==> roots p by A25,MSAFREE:10;
then {} = <*>(IIG-Terms the Sorts of A) & p is SubtreeSeq of Sym(
action_at v, the Sorts of A) by DTCONSTR:def 6;
then e = [action_at v,the carrier of IIG]-tree {} & {} is ArgumentSeq
of sy by MSATERM:def 2,TREES_4:20;
then e in IIG-Terms the Sorts of A by MSATERM:1;
then reconsider e as Element of TS(DTConMSA(the Sorts of A))
by MSATERM:def 1;
e.{} = [action_at v,the carrier of IIG] & the_result_sort_of
action_at v = v by A20,A21,MSAFREE2:def 7,TREES_4:3;
then
e in {a where a is Element of TS(DTConMSA(the Sorts of A)): (ex x
be set st x in (the Sorts of A).v & a = root-tree [x,v]) or ex o be OperSymbol
of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v};
then e in FreeSort(the Sorts of A,v) by MSAFREE:def 10;
then
A26: e in (the Sorts of FreeEnv A).v by A17,MSAFREE:def 11;
P[v,M.v] by A11;
hence M.i is Function of (FreeGen the Sorts of A).i, (the Sorts of
FreeEnv A).i by A16,A20,A26,FUNCOP_1:45;
end;
suppose
A27: v in InnerVertices IIG \ SortsWithConstants IIG;
A28: dom(id FreeGen(v, the Sorts of A)) = FreeGen(v, the Sorts of A) &
rng(id FreeGen(v, the Sorts of A)) = FreeGen(v, the Sorts of A);
P[v,M.v] by A11;
hence M.i is Function of (FreeGen the Sorts of A).i, (the Sorts of
FreeEnv A).i by A16,A17,A27,A28,FUNCT_2:def 1,RELSET_1:4;
end;
end;
now
let i be object;
assume i in dom M;
then i in the carrier of IIG by PARTFUN1:def 2;
hence M.i is Function by A12;
end;
then reconsider M as ManySortedFunction of the carrier of IIG by
FUNCOP_1:def 6;
reconsider M as ManySortedFunction of FreeGen the Sorts of A, the Sorts of
FreeEnv A by A12,PBOOLE:def 15;
take M;
let v be Vertex of IIG;
hereby
assume
A29: v in InputVertices IIG;
P[v,M.v] by A11;
hence M.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v] by A29;
end;
hereby
assume
A30: v in SortsWithConstants IIG;
P[v,M.v] by A11;
hence M.v = FreeGen(v, the Sorts of A) --> root-tree [action_at v,the
carrier of IIG] by A30;
end;
assume
A31: v in InnerVertices IIG \ SortsWithConstants IIG;
P[v,M.v] by A11;
hence thesis by A31;
end;
uniqueness
proof
let M1,M2 be ManySortedFunction of FreeGen the Sorts of A, the Sorts of
FreeEnv A such that
A32: for v being Vertex of IIG holds (v in InputVertices IIG implies
M1.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]) & (v in
SortsWithConstants IIG implies M1.v = FreeGen(v, the Sorts of A) --> root-tree
[action_at v,the carrier of IIG]) & (v in (InnerVertices IIG \
SortsWithConstants IIG) implies M1.v = id FreeGen(v, the Sorts of A)) and
A33: for v being Vertex of IIG holds (v in InputVertices IIG implies
M2.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]) & (v in
SortsWithConstants IIG implies M2.v = FreeGen(v, the Sorts of A) --> root-tree
[action_at v,the carrier of IIG]) & (v in (InnerVertices IIG \
SortsWithConstants IIG) implies M2.v = id FreeGen(v, the Sorts of A));
now
let i be object;
A34: (InnerVertices IIG \ SortsWithConstants IIG) \/ SortsWithConstants
IIG = InnerVertices IIG by MSAFREE2:3,XBOOLE_1:45;
assume
A35: i in the carrier of IIG;
then reconsider v = i as Vertex of IIG;
v in InputVertices IIG \/ InnerVertices IIG by A35,XBOOLE_1:45;
then
A36: v in InputVertices IIG or v in InnerVertices IIG by XBOOLE_0:def 3;
per cases by A34,A36,XBOOLE_0:def 3;
suppose
A37: v in InputVertices IIG;
then
M1.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v] by A32;
hence M1.i = M2.i by A33,A37;
end;
suppose
A38: v in SortsWithConstants IIG;
then M1.v = FreeGen(v, the Sorts of A) --> root-tree [action_at v,the
carrier of IIG] by A32;
hence M1.i = M2.i by A33,A38;
end;
suppose
A39: v in InnerVertices IIG \ SortsWithConstants IIG;
then M1.v = id FreeGen(v, the Sorts of A) by A32;
hence M1.i = M2.i by A33,A39;
end;
end;
hence M1 = M2;
end;
end;
definition
let IIG;
let A be non-empty Circuit of IIG, iv be InputValues of A;
func Fix_inp_ext iv -> ManySortedFunction of FreeEnv A, FreeEnv A means
:
Def2: it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it;
existence
proof
reconsider G = FreeGen the Sorts of A as free GeneratorSet of FreeEnv A by
MSAFREE:16;
consider h being ManySortedFunction of FreeEnv A, FreeEnv A such that
A1: h is_homomorphism FreeEnv A, FreeEnv A and
A2: h || G = Fix_inp iv by MSAFREE:def 5;
take h;
thus h is_homomorphism FreeEnv A, FreeEnv A by A1;
let i be object;
assume
A3: i in the carrier of IIG;
then reconsider
hi = h.i as Function of (the Sorts of FreeEnv A).i,(the Sorts
of FreeEnv A).i by PBOOLE:def 15;
(Fix_inp iv).i = hi | (G.i) by A2,A3,MSAFREE:def 1;
hence thesis by RELAT_1:59;
end;
uniqueness
proof
let h1,h2 be ManySortedFunction of FreeEnv A, FreeEnv A such that
A4: h1 is_homomorphism FreeEnv A, FreeEnv A and
A5: Fix_inp iv c= h1 and
A6: h2 is_homomorphism FreeEnv A, FreeEnv A and
A7: Fix_inp iv c= h2;
reconsider f1=h1, f2=h2 as ManySortedFunction of FreeMSA the Sorts of A,
FreeMSA the Sorts of A;
now
let i be set such that
A8: i in the carrier of IIG;
reconsider g = f2.i as Function of (the Sorts of FreeMSA the Sorts of A)
.i, (the Sorts of FreeMSA the Sorts of A).i by A8,PBOOLE:def 15;
A9: (Fix_inp iv).i c= g by A7,A8;
reconsider Fi = (Fix_inp iv).i as Function;
Fi is Function of (FreeGen the Sorts of A).i, (the Sorts of FreeMSA
the Sorts of A).i by A8,PBOOLE:def 15;
then
A10: dom Fi = (FreeGen the Sorts of A).i by A8,FUNCT_2:def 1;
A11: (Fix_inp iv).i c= f1.i by A5,A8;
thus (f2 || FreeGen the Sorts of A).i = g | ((FreeGen the Sorts of A).i)
by A8,MSAFREE:def 1
.= (Fix_inp iv).i by A10,A9,GRFUNC_1:23
.= (f1.i) | ((FreeGen the Sorts of A).i) by A10,A11,GRFUNC_1:23;
end;
then f1 || FreeGen the Sorts of A = f2 || FreeGen the Sorts of A
by MSAFREE:def 1;
hence h1 = h2 by A4,A6,EXTENS_1:14;
end;
end;
theorem Th2:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, x being
set st v in InnerVertices IIG \ SortsWithConstants IIG & e = root-tree[x,v]
holds (Fix_inp_ext iv).v.e = e
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, e be Element of (the Sorts of FreeEnv A).v, x be set such that
A1: v in InnerVertices IIG \ SortsWithConstants IIG and
A2: e = root-tree[x,v];
A3: e.{} = [x,v] by A2,TREES_4:3;
A4: now
given o being OperSymbol of IIG such that
A5: [o,the carrier of IIG] = e.{} and
the_result_sort_of o = v;
v = the carrier of IIG by A3,A5,XTUPLE_0:1;
hence contradiction by Lm1;
end;
set X = the Sorts of A;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then e in (FreeSort X).v;
then
A6: e in FreeSort(X,v) by MSAFREE:def 11;
Fix_inp iv c= Fix_inp_ext iv by Def2;
then
A7: (Fix_inp iv).v c= (Fix_inp_ext iv).v;
FreeSort(X,v) = {a where a is Element of TS(DTConMSA(X)): (ex x being
set st x in X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the
carrier of IIG] = a.{} & the_result_sort_of o = v} by MSAFREE:def 10;
then
ex a being Element of TS(DTConMSA(X)) st a = e &( (ex x being set st x in
X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the carrier of
IIG] = a.{} & the_result_sort_of o = v) by A6;
then
A8: e in FreeGen(v, the Sorts of A) by A4,MSAFREE:def 15;
then e in (FreeGen the Sorts of A).v by MSAFREE:def 16;
then e in dom((Fix_inp iv).v) by FUNCT_2:def 1;
hence (Fix_inp_ext iv).v.e = (Fix_inp iv).v.e by A7,GRFUNC_1:2
.= (id FreeGen(v, the Sorts of A)).e by A1,Def1
.= e by A8,FUNCT_1:17;
end;
theorem Th3:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, x being Element of (the Sorts of A).v st v in
InputVertices IIG holds (Fix_inp_ext iv).v.(root-tree[x,v]) = root-tree[iv.v,v]
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, x be Element of (the Sorts of A).v;
set e = root-tree[x,v];
assume
A1: v in InputVertices IIG;
A2: e in FreeGen(v, the Sorts of A) by MSAFREE:def 15;
Fix_inp iv c= Fix_inp_ext iv by Def2;
then
A3: (Fix_inp iv).v c= (Fix_inp_ext iv).v;
FreeEnv A = MSAlgebra (#FreeSort the Sorts of A,FreeOper the Sorts of A
#) by MSAFREE:def 14;
then reconsider e as Element of (the Sorts of FreeEnv A).v by A2;
e in (FreeGen the Sorts of A).v by A2,MSAFREE:def 16;
then e in dom((Fix_inp iv).v) by FUNCT_2:def 1;
hence (Fix_inp_ext iv).v.root-tree[x,v] = (Fix_inp iv).v.e by A3,GRFUNC_1:2
.= (FreeGen(v, the Sorts of A) --> root-tree [iv.v,v]).e by A1,Def1
.= root-tree[iv.v,v] by A2,FUNCOP_1:7;
end;
theorem Th4:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, p, q
being DTree-yielding FinSequence st v in InnerVertices IIG & e = [action_at v,
the carrier of IIG]-tree p & dom p = dom q & for k being Element of NAT st k in
dom p holds q.k = (Fix_inp_ext iv).((the_arity_of action_at v)/.k).(p.k) holds
(Fix_inp_ext iv).v.e = [action_at v,the carrier of IIG]-tree q
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, e be Element of (the Sorts of FreeEnv A).v, p, q be DTree-yielding
FinSequence such that
A1: v in InnerVertices IIG and
A2: e = [action_at v,the carrier of IIG]-tree p and
A3: dom p = dom q and
A4: for k being Element of NAT st k in dom p holds q.k = (Fix_inp_ext iv
).((the_arity_of action_at v)/.k).(p.k);
set o = action_at v;
A5: the_result_sort_of o = v by A1,MSAFREE2:def 7; then
A6: len p = len the_arity_of o by A2,MSAFREE2:10;
A7: now
let k be Nat;
assume
A8: k in dom q; then
A9: k in dom the_arity_of o by A3,A6,FINSEQ_3:29;
then p.k in (the Sorts of FreeEnv A).((the_arity_of o).k) by A2,A5,
MSAFREE2:11; then
A10: p.k in (the Sorts of FreeEnv A).((the_arity_of o)/.k) by A9,PARTFUN1:def 6
;
q.k = (Fix_inp_ext iv).((the_arity_of o)/.k).(p.k) by A3,A4,A8;
hence q.k in (the Sorts of FreeEnv A).((the_arity_of o)/.k) by A10,
FUNCT_2:5;
end;
A11: now
let k be Nat;
assume k in dom p;
then
A12: k in dom the_arity_of o by A6,FINSEQ_3:29;
then p.k in (the Sorts of FreeEnv A).((the_arity_of o).k) by A2,A5,
MSAFREE2:11;
hence p.k in (the Sorts of FreeEnv A).((the_arity_of o)/.k) by A12,
PARTFUN1:def 6;
end;
then reconsider x = p as Element of Args(o,FreeEnv A) by A6,MSAFREE2:5;
A13: FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then
A14: Args(o,FreeEnv A) = ((FreeSort the Sorts of A)# * (the Arity of IIG)).o
by MSUALG_1:def 4;
then reconsider
pp = p as FinSequence of TS(DTConMSA(the Sorts of A)) by A6,A11,MSAFREE:8
,MSAFREE2:5;
p in Args(o,FreeEnv A) by A6,A11,MSAFREE2:5;
then
A15: (Sym(o,the Sorts of A)) ==> roots pp by A14,MSAFREE:10;
A16: len q = len the_arity_of o by A3,A6,FINSEQ_3:29;
then reconsider y = q as Element of Args(o,FreeEnv A) by A7,MSAFREE2:5;
A17: Fix_inp_ext iv is_homomorphism FreeEnv A,FreeEnv A by Def2;
reconsider qq = q as FinSequence of TS(DTConMSA(the Sorts of A)) by A14,A16
,A7,MSAFREE:8,MSAFREE2:5;
q in Args(o,FreeEnv A) by A16,A7,MSAFREE2:5;
then
A18: (Sym(o,the Sorts of A)) ==> roots qq by A14,MSAFREE:10;
for k being Nat st k in dom p holds q.k = (Fix_inp_ext iv).((
the_arity_of action_at v)/.k).(p.k) by A4;
then
A19: y = (Fix_inp_ext iv)#x by MSUALG_3:def 6;
e = (Sym(action_at v,the Sorts of A))-tree pp by A2,MSAFREE:def 9
.= (DenOp(action_at v,the Sorts of A)).x by A15,MSAFREE:def 12
.= ((the Charact of FreeEnv A).o).x by A13,MSAFREE:def 13
.= Den(action_at v,FreeEnv A).x by MSUALG_1:def 6;
hence (Fix_inp_ext iv).v.e = Den(action_at v,FreeEnv A).q by A5,A19,A17,
MSUALG_3:def 7
.= ((FreeOper the Sorts of A).o).q by A13,MSUALG_1:def 6
.= (DenOp(action_at v,the Sorts of A)).q by MSAFREE:def 13
.= (Sym(action_at v,the Sorts of A))-tree qq by A18,MSAFREE:def 12
.= [action_at v,the carrier of IIG]-tree q by MSAFREE:def 9;
end;
theorem Th5:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st v in
SortsWithConstants IIG holds (Fix_inp_ext iv).v.e = root-tree[action_at v,the
carrier of IIG]
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, e be Element of (the Sorts of FreeEnv A).v;
set X = the Sorts of A;
assume
A1: v in SortsWithConstants IIG;
A2: FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then e in (FreeSort the Sorts of A).v;
then e in FreeSort(the Sorts of A,v) by MSAFREE:def 11;
then
e in {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.v
& a = root-tree [x,v]) or ex o be OperSymbol of IIG st [o,the carrier of IIG] =
a.{} & the_result_sort_of o = v} by MSAFREE:def 10;
then
A3: ex a being Element of TS(DTConMSA(X)) st e = a &( (ex x be set st x in X.
v & a = root-tree [x,v]) or ex o be OperSymbol of IIG st [o,the carrier of IIG]
= a.{} & the_result_sort_of o = v);
per cases by A3;
suppose
A4: ex x be set st x in X.v & e = root-tree [x,v];
Fix_inp iv c= Fix_inp_ext iv by Def2;
then
A5: (Fix_inp iv).v c= (Fix_inp_ext iv).v;
A6: e in FreeGen(v, the Sorts of A) by A4,MSAFREE:def 15;
then e in (FreeGen the Sorts of A).v by MSAFREE:def 16;
then e in dom((Fix_inp iv).v) by FUNCT_2:def 1;
hence (Fix_inp_ext iv).v.e = (Fix_inp iv).v.e by A5,GRFUNC_1:2
.= (FreeGen(v, the Sorts of A) --> root-tree [action_at v,the carrier
of IIG]).e by A1,Def1
.= root-tree[action_at v,the carrier of IIG] by A6,FUNCOP_1:7;
end;
suppose
ex o be OperSymbol of IIG st [o,the carrier of IIG] = e.{} &
the_result_sort_of o = v;
then consider o9 be OperSymbol of IIG such that
A7: [o9,the carrier of IIG] = e.{} and
A8: the_result_sort_of o9 = v;
A9: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then o9 = action_at v by A1,A8,MSAFREE2:def 7;
then consider q being DTree-yielding FinSequence such that
A10: e = [action_at v,the carrier of IIG]-tree q by A7,CIRCUIT1:9;
v in { s where s is SortSymbol of IIG : s is with_const_op } by A1,
MSAFREE2:def 1;
then ex s being SortSymbol of IIG st v = s & s is with_const_op;
then consider o being OperSymbol of IIG such that
A11: (the Arity of IIG).o = {} and
A12: (the ResultSort of IIG).o = v by MSUALG_2:def 1;
A13: Fix_inp_ext iv is_homomorphism FreeEnv A,FreeEnv A by Def2;
the_result_sort_of o = v by A12,MSUALG_1:def 2;
then
A14: o = action_at v by A1,A9,MSAFREE2:def 7;
action_at v in the carrier' of IIG;
then
A15: action_at v in dom the Arity of IIG by FUNCT_2:def 1;
A16: Args(action_at v,FreeEnv A) = ((the Sorts of FreeEnv A)# * the Arity
of IIG).action_at v by MSUALG_1:def 4
.= (the Sorts of FreeEnv A)#.<*>the carrier of IIG by A11,A14,A15,
FUNCT_1:13
.= {{}} by PRE_CIRC:2;
then reconsider x = {} as Element of Args(action_at v,FreeEnv A) by
TARSKI:def 1;
A17: x = (Fix_inp_ext iv)#x by A16,TARSKI:def 1;
A18: Args(action_at v,FreeEnv A) = ((FreeSort the Sorts of A)# * (the
Arity of IIG)).o by A2,A14,MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS(DTConMSA(the Sorts of A)) by
MSAFREE:8;
A19: (Sym(action_at v,the Sorts of A)) ==> roots p by A14,A18,MSAFREE:10;
A20: the_result_sort_of action_at v = v by A1,A9,MSAFREE2:def 7;
then len q = len the_arity_of action_at v by A10,MSAFREE2:10
.= len {} by A11,A14,MSUALG_1:def 1
.= 0;
then q = {};
then
A21: e = root-tree[action_at v,the carrier of IIG] by A10,TREES_4:20;
Den(action_at v,FreeEnv A).x = ((FreeOper the Sorts of A).action_at v
).x by A2,MSUALG_1:def 6
.= (DenOp(action_at v,the Sorts of A)).x by MSAFREE:def 13
.= (Sym(action_at v,the Sorts of A))-tree p by A19,MSAFREE:def 12
.= [action_at v,the carrier of IIG]-tree p by MSAFREE:def 9
.= root-tree[action_at v,the carrier of IIG] by TREES_4:20;
hence thesis by A20,A17,A13,A21,MSUALG_3:def 7;
end;
end;
theorem Th6:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v, t, t1
being DecoratedTree st t = e & t1 = e1 & e1 = (Fix_inp_ext iv).v.e holds dom t
= dom t1
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, e, e1 be Element of (the Sorts of FreeEnv A).v, t, t1 be DecoratedTree;
set X = the Sorts of A;
set FX = the Sorts of FreeEnv A;
defpred P[Nat] means for v being Vertex of IIG, e, e1 being
Element of FX.v, t, t1 being DecoratedTree st t = e & t1 = e1 & depth(v,A) <=
$1 & e1 = (Fix_inp_ext iv).v.e holds dom t = dom t1;
reconsider k = depth(v,A) as Element of NAT by ORDINAL1:def 12;
A1: depth(v,A) <= k;
A2: FreeMSA X = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 14;
A3: for k be Nat st P[k] holds P[k+1]
proof
A4: (InnerVertices IIG \ SortsWithConstants IIG ) \/ SortsWithConstants
IIG = InnerVertices IIG by MSAFREE2:3,XBOOLE_1:45;
let k be Nat;
assume
A5: P[k];
let v be Vertex of IIG, e, e1 be Element of FX.v, t, t1 be DecoratedTree;
assume that
A6: t = e and
A7: t1 = e1 and
A8: depth(v,A) <= (k+1) and
A9: e1 = (Fix_inp_ext iv).v.e;
A10: FreeSort(X,v) = {a where a is Element of TS(DTConMSA(X)): (ex x being
set st x in X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the
carrier of IIG] = a.{} & the_result_sort_of o = v} by MSAFREE:def 10;
InputVertices IIG \/ InnerVertices IIG = the carrier of IIG by XBOOLE_1:45;
then
A11: v in InputVertices IIG or v in InnerVertices IIG by XBOOLE_0:def 3;
e in FX.v & (FreeSort X).v = FreeSort(X,v) by MSAFREE:def 11;
then consider a being Element of TS(DTConMSA(X)) such that
A12: a = e and
A13: (ex x being set st x in X.v & a = root-tree[x,v]) or ex o being
OperSymbol of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v
by A2,A10;
per cases by A13,A11,A4,XBOOLE_0:def 3;
suppose
A14: v in InputVertices IIG;
then
A15: (Fix_inp_ext iv).v.a = root-tree[iv.v,v] by A13,Th3,MSAFREE2:2;
thus dom t = {{}} by A6,A12,A13,A14,MSAFREE2:2,TREES_1:29,TREES_4:3
.= dom t1 by A7,A9,A12,A15,TREES_1:29,TREES_4:3;
end;
suppose
v in InnerVertices IIG \ SortsWithConstants IIG & ex x being
set st x in X.v & a = root-tree[x,v];
hence thesis by A6,A7,A9,A12,Th2;
end;
suppose that
A16: v in SortsWithConstants IIG and
A17: ex x being set st x in X.v & a = root-tree[x,v];
A18: (Fix_inp_ext iv).v.a = root-tree[action_at v,the carrier of IIG] by A12
,A16,Th5;
thus dom t = {{}} by A6,A12,A17,TREES_1:29,TREES_4:3
.= dom t1 by A7,A9,A12,A18,TREES_1:29,TREES_4:3;
end;
suppose that
A19: v in InnerVertices IIG and
A20: ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v;
consider o being OperSymbol of IIG such that
A21: [o,the carrier of IIG] = a.{} and
A22: the_result_sort_of o = v by A20;
A23: o = action_at v by A19,A22,MSAFREE2:def 7;
then consider p being DTree-yielding FinSequence such that
A24: e = [action_at v,the carrier of IIG]-tree p by A12,A21,CIRCUIT1:9;
deffunc F(Nat) = (Fix_inp_ext iv).((the_arity_of action_at v)/.$1).(p.$1
);
consider q being FinSequence such that
A25: len q = len p and
A26: for k being Nat st k in dom q holds q.k = F(k) from FINSEQ_1:
sch 2;
A27: dom p = dom q by A25,FINSEQ_3:29;
len p = len the_arity_of action_at v by A22,A23,A24,MSAFREE2:10;
then
A28: dom p = dom the_arity_of action_at v by FINSEQ_3:29;
A29: now
let x be object;
assume
A30: x in dom q;
then reconsider i = x as Element of NAT;
set v1 = (the_arity_of action_at v)/.i;
v1 = (the_arity_of o).i by A23,A28,A27,A30,PARTFUN1:def 6;
then reconsider
ee = p.i as Element of FX.v1 by A22,A23,A24,A28,A27,A30,MSAFREE2:11;
reconsider fv1 = (Fix_inp_ext iv).v1 as Function of FX.v1,FX.v1;
q.i = fv1.ee by A26,A30;
hence q.x is DecoratedTree;
end;
A31: for k being Element of NAT st k in dom q holds q.k = F(k) by A26;
reconsider q as DTree-yielding FinSequence by A29,TREES_3:24;
A32: (Fix_inp_ext iv).v.e = [action_at v,the carrier of IIG]-tree q by A19,A24
,A31,A27,Th4;
A33: dom doms p = dom p by TREES_3:37;
A34: now
let i be Nat;
set v1 = (the_arity_of action_at v)/.i;
reconsider fv1 = (Fix_inp_ext iv).v1 as Function of FX.v1,FX.v1;
assume
A35: i in dom doms p;
then v1 = (the_arity_of o).i by A23,A28,A33,PARTFUN1:def 6;
then reconsider
ee = p.i as Element of FX.v1 by A22,A23,A24,A28,A33,A35,MSAFREE2:11;
q.i = fv1.ee by A26,A33,A27,A35;
then reconsider ee1 = q.i as Element of FX.v1;
v1 in rng the_arity_of action_at v by A28,A33,A35,PARTFUN2:2;
then depth(v1,A) < k+1 by A8,A19,CIRCUIT1:19,XXREAL_0:2;
then
A36: depth(v1,A) <= k by NAT_1:13;
q.i = (Fix_inp_ext iv).v1.(p.i) by A26,A33,A27,A35;
then dom ee = dom ee1 by A5,A36;
hence (doms p).i = dom ee1 by A33,A35,FUNCT_6:22
.= (doms q).i by A33,A27,A35,FUNCT_6:22;
end;
dom q = dom doms q by TREES_3:37;
then doms p = doms q by A27,A34,FINSEQ_1:13,TREES_3:37;
hence dom t = tree(doms q) by A6,A24,TREES_4:10
.= dom t1 by A7,A9,A32,TREES_4:10;
end;
end;
A37: P[ 0 ]
proof
let v be Vertex of IIG, e, e1 be Element of FX.v, t, t1 be DecoratedTree
such that
A38: t = e and
A39: t1 = e1 and
A40: depth(v,A) <= 0 and
A41: e1 = (Fix_inp_ext iv).v.e;
A42: depth(v,A) = 0 by A40,NAT_1:3;
A43: FreeSort(X,v) = {a where a is Element of TS(DTConMSA(X)): (ex x being
set st x in X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the
carrier of IIG] = a.{} & the_result_sort_of o = v} by MSAFREE:def 10;
e in FX.v & (FreeSort X).v = FreeSort(X,v) by MSAFREE:def 11;
then consider a being Element of TS(DTConMSA(X)) such that
A44: a = e and
A45: (ex x being set st x in X.v & a = root-tree[x,v]) or ex o being
OperSymbol of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v
by A2,A43;
per cases by A42,A45,CIRCUIT1:18;
suppose
A46: v in InputVertices IIG;
then
A47: (Fix_inp_ext iv).v.a = root-tree[iv.v,v] by A45,Th3,MSAFREE2:2;
thus dom t = {{}} by A38,A44,A45,A46,MSAFREE2:2,TREES_1:29,TREES_4:3
.= dom t1 by A39,A41,A44,A47,TREES_1:29,TREES_4:3;
end;
suppose that
A48: v in SortsWithConstants IIG and
A49: ex x being set st x in X.v & a = root-tree[x,v];
A50: (Fix_inp_ext iv).v.a = root-tree[action_at v,the carrier of IIG] by A44
,A48,Th5;
thus dom t = {{}} by A38,A44,A49,TREES_1:29,TREES_4:3
.= dom t1 by A39,A41,A44,A50,TREES_1:29,TREES_4:3;
end;
suppose that
A51: v in SortsWithConstants IIG and
A52: ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v;
A53: (Fix_inp_ext iv).v.a = root-tree[action_at v,the carrier of IIG] by A44
,A51,Th5;
consider o being OperSymbol of IIG such that
A54: [o,the carrier of IIG] = a.{} and
A55: the_result_sort_of o = v by A52;
A56: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then o = action_at v by A51,A55,MSAFREE2:def 7;
then consider p being DTree-yielding FinSequence such that
A57: a = [action_at v,the carrier of IIG]-tree p by A44,A54,CIRCUIT1:9;
v in { s where s is SortSymbol of IIG : s is with_const_op } by A51,
MSAFREE2:def 1;
then ex s being SortSymbol of IIG st v = s & s is with_const_op;
then consider o9 being OperSymbol of IIG such that
A58: (the Arity of IIG).o9 = {} and
A59: (the ResultSort of IIG).o9 = v by MSUALG_2:def 1;
A60: the_result_sort_of o9 = v by A59,MSUALG_1:def 2;
then
A61: o9 = action_at v by A51,A56,MSAFREE2:def 7;
then len p = len the_arity_of o9 by A44,A60,A57,MSAFREE2:10
.= len {} by A58,MSUALG_1:def 1
.= 0;
then p = {};
then a = root-tree[o9,the carrier of IIG] by A61,A57,TREES_4:20;
hence dom t = {{}} by A38,A44,TREES_1:29,TREES_4:3
.= dom t1 by A39,A41,A44,A53,TREES_1:29,TREES_4:3;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A37,A3);
hence thesis by A1;
end;
theorem Th7:
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v st e1
= (Fix_inp_ext iv).v.e holds card e = card e1
proof
let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of
IIG, e, e1 be Element of (the Sorts of FreeEnv A).v;
assume e1 = (Fix_inp_ext iv).v.e;
then dom e = dom e1 by Th6;
hence card e = card dom e1 by CARD_1:62
.= card e1 by CARD_1:62;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS;
func IGTree(v,iv) -> Element of (the Sorts of FreeEnv SCS).v means
:Def3:
ex
e being Element of (the Sorts of FreeEnv SCS).v st card e = size(v,SCS) & it =
(Fix_inp_ext iv).v.e;
existence
proof
reconsider SFv = (the Sorts of FreeEnv SCS).v as non empty set;
consider s being finite non empty Subset of NAT such that
A1: s = the set of all
card t where t is Element of (the Sorts of FreeEnv SCS).v and
A2: size(v,SCS) = max s by CIRCUIT1:def 4;
size(v,SCS) in s by A2,XXREAL_2:def 8;
then consider e being Element of (the Sorts of FreeEnv SCS).v such that
A3: size(v,SCS) = card e by A1;
reconsider Fiev = (Fix_inp_ext iv).v as Function of SFv, SFv;
reconsider e9 = e as Element of SFv;
reconsider IT = Fiev.e9 as Element of SFv;
reconsider IT as Element of (the Sorts of FreeEnv SCS).v;
take IT, e;
thus card e = size(v,SCS) by A3;
thus thesis;
end;
uniqueness
proof
defpred P[Nat] means ex v being Vertex of IIG, it1, it2 being Element of (
the Sorts of FreeEnv SCS).v st size(v,SCS) = $1 & (ex e1 being Element of (the
Sorts of FreeEnv SCS).v st card e1 = size(v,SCS) & it1 = (Fix_inp_ext iv).v.e1)
& (ex e2 being Element of (the Sorts of FreeEnv SCS).v st card e2 = size(v,SCS)
& it2 = (Fix_inp_ext iv).v.e2) & it1 <> it2;
let it1, it2 be Element of (the Sorts of FreeEnv SCS).v;
now
assume
A4: ex n being Nat st P[n];
consider n being Nat such that
A5: P[n] and
A6: for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A4);
consider v being Vertex of IIG, it1, it2 being Element of (the Sorts of
FreeEnv SCS).v such that
A7: size(v,SCS) = n and
A8: ex e1 being Element of (the Sorts of FreeEnv SCS).v st card e1
= size(v,SCS) & it1 = (Fix_inp_ext iv).v.e1 and
A9: ex e2 being Element of (the Sorts of FreeEnv SCS).v st card e2
= size(v,SCS) & it2 = (Fix_inp_ext iv).v.e2 and
A10: it1 <> it2 by A5;
consider e2 being Element of (the Sorts of FreeEnv SCS).v such that
A11: card e2 = size(v,SCS) and
A12: it2 = (Fix_inp_ext iv).v.e2 by A9;
consider e1 being Element of (the Sorts of FreeEnv SCS).v such that
A13: card e1 = size(v,SCS) and
A14: it1 = (Fix_inp_ext iv).v.e1 by A8;
per cases;
suppose
A15: v in InputVertices IIG; then
A16: ex x2 being Element of (the Sorts of SCS).v st e2 = root-tree[x2,v
] by MSAFREE2:9;
ex x1 being Element of (the Sorts of SCS).v st e1 = root-tree[x1,v
] by A15,MSAFREE2:9;
then it1 = root-tree[iv.v, v] by A14,A15,Th3
.= it2 by A12,A15,A16,Th3;
hence contradiction by A10;
end;
suppose
A17: v in SortsWithConstants IIG;
then it1 = root-tree[action_at v,the carrier of IIG] by A14,Th5
.= it2 by A12,A17,Th5;
hence contradiction by A10;
end;
suppose that
A18: not v in InputVertices IIG and
A19: not v in SortsWithConstants IIG;
set Ht = (Fix_inp_ext iv) * (the_arity_of action_at v);
InputVertices IIG \/ InnerVertices IIG = the carrier of IIG
by XBOOLE_1:45; then
A20: v in InnerVertices IIG by A18,XBOOLE_0:def 3; then
A21: v in (InnerVertices IIG \ SortsWithConstants IIG) by A19,XBOOLE_0:def 5
;
then consider q1 being DTree-yielding FinSequence such that
A22: e1 = [action_at v,the carrier of IIG]-tree q1 by A13,CIRCUIT1:12;
[action_at v,the carrier of IIG]-tree q1 in (the Sorts of FreeEnv
SCS).v by A22; then
[action_at v,the carrier of IIG]-tree q1 in (the Sorts of FreeEnv
SCS). (the_result_sort_of action_at v) by A20,MSAFREE2:def 7; then
B2: len q1 = len the_arity_of action_at v by MSAFREE2:10;
consider q2 being DTree-yielding FinSequence such that
A23: e2 = [action_at v,the carrier of IIG]-tree q2 by A11,A21,CIRCUIT1:12;
[action_at v,the carrier of IIG]-tree q2 in (the Sorts of FreeEnv
SCS). v by A23; then
A24: [action_at v,the carrier of IIG]-tree q2 in (the Sorts of FreeEnv
SCS). (the_result_sort_of action_at v) by A20,MSAFREE2:def 7; then
B1: len q2 = len the_arity_of action_at v by MSAFREE2:10; then
B3: dom q1 = dom q2 by B2,FINSEQ_3:29;
set acv = action_at v;
B4: dom q2 = dom the_arity_of acv by FINSEQ_3:29,B1;
A25: Fix_inp_ext iv is_homomorphism FreeEnv SCS, FreeEnv SCS by Def2;
then consider p1 being DTree-yielding FinSequence such that
A26: p1 = Ht..q1 and
A27: it1 = [action_at v,the carrier of IIG]-tree p1 by A14,A20,A22,Th1;
consider p2 being DTree-yielding FinSequence such that
A28: p2 = Ht..q2 and
A29: it2 = [action_at v,the carrier of IIG]-tree p2 by A12,A20,A23,A25,Th1;
rng (the_arity_of acv) c= the carrier of IIG by FINSEQ_1:def 4;
then rng (the_arity_of acv) c= dom (Fix_inp_ext iv)
by PARTFUN1:def 2; then
A33: dom the_arity_of action_at v = dom Ht by RELAT_1:27;
A30: dom p1 = dom Ht /\ dom q1 by A26,PRALG_1:def 19
.= dom Ht by A33,B4,B3;
a30: dom p2 = dom Ht /\ dom q2 by A28,PRALG_1:def 19
.= dom Ht by A33,B4;
then len p1 = len p2 by A30,FINSEQ_3:29;
then consider i being Nat such that
A31: i in dom p1 and
A32: p1.i <> p2.i by A10,A27,A29,FINSEQ_2:9;
reconsider w = (the_arity_of acv).i as Vertex of IIG
by A30,A31,A33,FINSEQ_2:11;
[acv,the carrier of IIG]-tree q1 in (the Sorts of FreeEnv
SCS). v by A22; then
A34: [acv,the carrier of IIG]-tree q1 in
(the Sorts of FreeEnv SCS). (the_result_sort_of acv)
by A20,MSAFREE2:def 7;
then reconsider
E1 = q1.i, E2 = q2.i as Element of (the Sorts of FreeEnv
SCS).w by A30,A33,A31,A24,MSAFREE2:11;
B2: len q1 = len the_arity_of acv by A34,MSAFREE2:10;
[acv,the carrier of IIG]-tree p2 in (the Sorts of FreeEnv
SCS). v by A29; then
A35: [acv,the carrier of IIG]-tree p2 in (the Sorts of FreeEnv
SCS). (the_result_sort_of acv) by A20,MSAFREE2:def 7;
[acv,the carrier of IIG]-tree p1 in (the Sorts of FreeEnv
SCS). v by A27; then
[acv,the carrier of IIG]-tree p1 in (the Sorts of FreeEnv
SCS). (the_result_sort_of acv) by A20,MSAFREE2:def 7;
then reconsider
It1 = p1.i, It2 = p2.i as Element of (the Sorts of FreeEnv SCS).w
by A30,A33,A31,A35,MSAFREE2:11;
reconsider Hti = Ht.i as Function;
A36: Hti = (Fix_inp_ext iv).((the_arity_of acv).i)
by A30,A31,FUNCT_1:12; then
A37: It2 = (Fix_inp_ext iv).w.E2 by a30,A28,A30,A31,PRALG_1:def 19;
i in dom q2 by B1,A30,A33,A31,FINSEQ_3:29;
then E2 in rng q2 by FUNCT_1:def 3; then
A38: card E2 = size(w,SCS) by A11,A21,A23,CIRCUIT1:11;
i in dom q1 by B2,A30,A33,A31,FINSEQ_3:29;
then E1 in rng q1 by FUNCT_1:def 3; then
A39: card E1 = size(w,SCS) by A13,A21,A22,CIRCUIT1:11;
A40: w in rng the_arity_of action_at v by A30,A33,A31,FUNCT_1:def 3;
It1 = (Fix_inp_ext iv).w.E1 by A26,A31,A36,PRALG_1:def 19;
hence contradiction by A6,A7,A20,A32,A39,A38,A37,A40,CIRCUIT1:14;
end;
end;
hence thesis;
end;
end;
theorem Th8:
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS holds
IGTree(v,iv) = (Fix_inp_ext iv).v.IGTree(v,iv)
proof
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS;
reconsider igt = IGTree(v,iv) as Element of (the Sorts of FreeEnv SCS).v;
ex e being Element of (the Sorts of FreeEnv SCS).v st card e = size(v,SCS
) & IGTree(v,iv) = (Fix_inp_ext iv).v.e by Def3;
then card igt = size(v,SCS) by Th7;
hence thesis by Def3;
end;
theorem Th9:
for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv
being InputValues of SCS, p being DTree-yielding FinSequence st v in
InnerVertices IIG & dom p = dom the_arity_of action_at v & for k being Element
of NAT st k in dom p holds p.k = IGTree((the_arity_of action_at v)/.k, iv)
holds IGTree(v,iv) = [action_at v,the carrier of IIG]-tree p
proof
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS, p be DTree-yielding FinSequence;
assume that
A1: v in InnerVertices IIG and
A2: dom p = dom the_arity_of action_at v and
A3: for k being Element of NAT st k in dom p holds p.k = IGTree((
the_arity_of action_at v)/.k, iv);
set U1 = FreeEnv SCS;
set o = action_at v;
A4: now
let k be Nat;
assume k in dom p;
then p.k = IGTree((the_arity_of o)/.k, iv) by A3;
hence p.k in (the Sorts of U1).((the_arity_of o)/.k);
end;
len p = len the_arity_of o by A2,FINSEQ_3:29;
then reconsider p99 = p as Element of Args(o,U1) by A4,MSAFREE2:5;
set X = the Sorts of SCS;
A5: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
A6: Result(o,U1) = ((the Sorts of U1) * the ResultSort of IIG).o by
MSUALG_1:def 5
.= (the Sorts of U1).((the ResultSort of IIG).o) by A5,FUNCT_1:13;
A7: U1 = MSAlgebra (# FreeSort(X), FreeOper(X) #) & Args(o,U1) = ((the Sorts
of U1)# * the Arity of IIG).o by MSAFREE:def 14,MSUALG_1:def 4;
then reconsider p9 = p99 as FinSequence of TS(DTConMSA(X)) by MSAFREE:8;
U1 = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 14;
then
A8: Den(o,U1) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o,X) by MSAFREE:def 13;
Sym(o,X) ==> roots p9 by A7,MSAFREE:10;
then
A9: Den(o,U1).p = (Sym(o,X))-tree p9 by A8,MSAFREE:def 12
.= [o,the carrier of IIG]-tree p9 by MSAFREE:def 9;
(the ResultSort of IIG).o = the_result_sort_of o by MSUALG_1:def 2
.= v by A1,MSAFREE2:def 7;
then reconsider
t = [action_at v,the carrier of IIG]-tree p as Element of (the
Sorts of FreeMSA X).v by A9,A6,FUNCT_2:5;
now
let k be Element of NAT;
set v1 = (the_arity_of action_at v)/.k;
assume k in dom p;
then
A10: p.k = IGTree(v1,iv) by A3;
then reconsider ek = p.k as Element of (the Sorts of FreeEnv SCS).v1;
take ek;
thus ek = p.k;
ex e1 being Element of (the Sorts of FreeMSA X).v1 st card e1 = size(
v1,SCS) & ek = (Fix_inp_ext iv).v1.e1 by A10,Def3;
hence card ek = size(v1,SCS) by Th7;
end;
then
A11: card t = size(v,SCS) by A1,CIRCUIT1:16;
now
let k be Element of NAT;
assume k in dom p;
then p.k = IGTree((the_arity_of action_at v)/.k, iv) by A3;
hence p.k = (Fix_inp_ext iv).((the_arity_of action_at v)/.k).(p.k) by Th8;
end;
then [action_at v,the carrier of IIG]-tree p = (Fix_inp_ext iv).v.t by A1,Th4
;
hence thesis by A11,Def3;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG,
iv be InputValues of SCS;
func IGValue(v,iv) -> Element of (the Sorts of SCS).v equals
(Eval SCS).v.(IGTree(v,iv));
coherence;
end;
theorem Th10:
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS st v in InputVertices IIG holds IGValue(v,iv) = iv.
v
proof
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS;
set X = the Sorts of SCS;
A1: (FreeSort X).v = FreeSort(X, v) & FreeSort(X,v) = {a where a is Element
of TS(DTConMSA(X)): (ex x being set st x in X.v & a = root-tree[x,v]) or ex o
being OperSymbol of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o
= v} by MSAFREE:def 10,def 11;
assume
A2: v in InputVertices IIG;
then
A3: iv.v in (the Sorts of SCS).v by MSAFREE2:def 5;
then root-tree[iv.v,v] in FreeGen(v, the Sorts of SCS) by MSAFREE:def 15;
then root-tree[iv.v,v] in (FreeSort(the Sorts of SCS)).v;
then
A4: root-tree[iv.v,v] in FreeSort(the Sorts of SCS,v) by MSAFREE:def 11;
consider e being Element of (the Sorts of FreeEnv SCS).v such that
card e = size(v,SCS) and
A5: IGTree(v,iv) = (Fix_inp_ext iv).v.e by Def3;
e in (the Sorts of FreeMSA X).v & FreeMSA X = MSAlgebra (# FreeSort(X),
FreeOper(X) #) by MSAFREE:def 14;
then
ex a being Element of TS(DTConMSA(X)) st a = e &( (ex x being set st x in
X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the carrier of
IIG] = a.{} & the_result_sort_of o = v) by A1;
then
A6: e in FreeGen(v,the Sorts of SCS) by A2,MSAFREE:def 15,MSAFREE2:2;
Fix_inp iv c= Fix_inp_ext iv by Def2;
then
A7: (Fix_inp iv).v c= (Fix_inp_ext iv).v;
A8: (Fix_inp iv).v = FreeGen(v,the Sorts of SCS) --> root-tree[iv.v,v] by A2
,Def1;
then e in dom ((Fix_inp iv).v) by A6;
then (Fix_inp iv).v.e = (Fix_inp_ext iv).v.e by A7,GRFUNC_1:2;
hence IGValue(v,iv) = (Eval SCS).v.(root-tree[iv.v,v]) by A5,A6,A8,FUNCOP_1:7
.= iv.v by A3,A4,MSAFREE2:def 9;
end;
theorem Th11:
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS st v in SortsWithConstants IIG holds IGValue(v,iv)
= (Set-Constants SCS).v
proof
reconsider p = {} as DTree-yielding FinSequence;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS;
assume
A1: v in SortsWithConstants IIG;
set e = (Eval SCS).v.root-tree[action_at v,the carrier of IIG];
A2: {} = <*>the carrier of IIG;
set X = the Sorts of SCS;
set F = Eval SCS;
A3: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
A4: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
set o = action_at v;
A5: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then
A6: v = the_result_sort_of o by A1,MSAFREE2:def 7;
SortsWithConstants IIG = {v1 where v1 is SortSymbol of IIG : v1 is
with_const_op } by MSAFREE2:def 1;
then consider x9 being SortSymbol of IIG such that
A7: x9=v and
A8: x9 is with_const_op by A1;
consider o1 being OperSymbol of IIG such that
A9: (the Arity of IIG).o1 = {} and
A10: (the ResultSort of IIG).o1 = x9 by A8,MSUALG_2:def 1;
(the ResultSort of IIG).o1 = the_result_sort_of o1 by MSUALG_1:def 2;
then
A11: o = o1 by A1,A5,A7,A10,MSAFREE2:def 7;
A12: Args(o,FreeEnv SCS) = ((the Sorts of FreeEnv SCS)# * the Arity of IIG).
o by MSUALG_1:def 4
.= (the Sorts of FreeEnv SCS)#.((the Arity of IIG).o) by A3,FUNCT_1:13
.= {{}} by A9,A11,A2,PRE_CIRC:2;
then reconsider x = {} as Element of Args(o,FreeEnv SCS) by TARSKI:def 1;
reconsider Fx = F#x as Element of Args(o,SCS);
F is_homomorphism FreeEnv SCS, SCS by MSAFREE2:def 9;
then
A13: (F.(the_result_sort_of o)).(Den(o,FreeEnv SCS).x) = Den(o, SCS).(Fx )
by MSUALG_3:def 7;
A14: FreeMSA X = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 14;
then
A15: Den(o,FreeEnv SCS) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o,X) by MSAFREE:def 13;
{} in Args(o,FreeEnv SCS) by A12,TARSKI:def 1;
then
A16: p in ((FreeSort X)# * (the Arity of IIG)).o by A14,MSUALG_1:def 4;
then reconsider p9 = {} as FinSequence of TS(DTConMSA(X)) by MSAFREE:8;
Sym(o,X) ==> roots p9 by A16,MSAFREE:10;
then
A17: Den(o,FreeEnv SCS).{} = (Sym(o,X))-tree p by A15,MSAFREE:def 12
.= [o,the carrier of IIG]-tree {} by MSAFREE:def 9
.= root-tree [o,the carrier of IIG] by TREES_4:20;
dom Den(o,SCS) = Args(o,SCS) by FUNCT_2:def 1;
then
A18: e in rng Den(o,SCS) by A6,A17,A13,FUNCT_1:def 3;
Result(o,SCS) = ((the Sorts of SCS) * the ResultSort of IIG).o by
MSUALG_1:def 5
.= (the Sorts of SCS).((the ResultSort of IIG).o) by A4,FUNCT_1:13;
then reconsider e as Element of (the Sorts of SCS).v by A6,A17,A13,
MSUALG_1:def 2;
ex A being non empty set st A =(the Sorts of SCS).v & Constants (SCS, v)
= { a where a is Element of A : ex o be OperSymbol of IIG st (the Arity of IIG)
.o = {} & (the ResultSort of IIG).o = v & a in rng Den(o,SCS) } by
MSUALG_2:def 3;
then
A19: e in Constants(SCS,v) by A7,A9,A10,A11,A18;
ex e being Element of (the Sorts of FreeEnv SCS).v st card e = size(v,SCS
) & IGTree(v,iv) = (Fix_inp_ext iv).v.e by Def3;
hence IGValue(v,iv) = e by A1,Th5
.= (Set-Constants SCS).v by A1,A19,CIRCUIT1:1;
end;
begin
::---------------------------------------------------------------------------
:: Computations
::---------------------------------------------------------------------------
definition
let IIG be Circuit-like non void non empty ManySortedSign;
let SCS be non-empty Circuit of IIG, s be State of SCS;
func Following s -> State of SCS means
:Def5:
for v being Vertex of IIG
holds (v in InputVertices IIG implies it.v = s.v) & (v in InnerVertices IIG
implies it.v = (Den(action_at v,SCS)).(action_at v depends_on_in s));
existence
proof
deffunc G(Vertex of IIG) = (Den(action_at $1,SCS)).(action_at $1
depends_on_in s);
deffunc F(set) = s.$1;
defpred P[set] means $1 in InputVertices IIG;
consider f being ManySortedSet of the carrier of IIG such that
A1: for v being Vertex of IIG st v in the carrier of IIG holds (P[v]
implies f.v = F(v)) & (not P[v] implies f.v = G(v)) from PRE_CIRC:sch 2;
A2: now
let x be object;
assume x in dom the Sorts of SCS;
then reconsider v = x as Vertex of IIG by PARTFUN1:def 2;
per cases;
suppose
v in InputVertices IIG;
then f.v = s.v by A1;
hence f.x in (the Sorts of SCS).x by CIRCUIT1:4;
end;
suppose
A3: not v in InputVertices IIG;
v in the carrier of IIG;
then v in InputVertices IIG \/ InnerVertices IIG by XBOOLE_1:45;
then v in InnerVertices IIG by A3,XBOOLE_0:def 3;
then
A4: the_result_sort_of action_at v = v by MSAFREE2:def 7;
f.x = (Den(action_at v,SCS)).(action_at v depends_on_in s) by A1,A3;
hence f.x in (the Sorts of SCS).x by A4,CIRCUIT1:8;
end;
end;
dom f = the carrier of IIG & dom the Sorts of SCS = the carrier of IIG
by PARTFUN1:def 2;
then reconsider f as State of SCS by A2,CARD_3:def 5;
take f;
let v be Vertex of IIG;
thus v in InputVertices IIG implies f.v = s.v by A1;
A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
assume v in InnerVertices IIG;
then not v in InputVertices IIG by A5,XBOOLE_0:3;
hence thesis by A1;
end;
uniqueness
proof
let it1, it2 be State of SCS such that
A6: for v being Vertex of IIG holds (v in InputVertices IIG implies
it1.v = s.v) & (v in InnerVertices IIG implies it1.v = (Den(action_at v,SCS)) .
(action_at v depends_on_in s)) and
A7: for v being Vertex of IIG holds (v in InputVertices IIG implies
it2.v = s.v) & (v in InnerVertices IIG implies it2.v = (Den(action_at v,SCS)) .
(action_at v depends_on_in s));
assume
A8: it1 <> it2;
dom it2 = the carrier of IIG by CIRCUIT1:3;
then consider x being object such that
A9: x in dom it1 and
A10: it1.x <> it2.x by A8,CIRCUIT1:3,FUNCT_1:2;
reconsider v = x as Vertex of IIG by A9,CIRCUIT1:3;
A11: v in InnerVertices IIG implies it1.v = (Den(action_at v,SCS)).(
action_at v depends_on_in s) by A6;
dom it1 = the carrier of IIG by CIRCUIT1:3;
then v in InputVertices IIG \/ InnerVertices IIG by A9,XBOOLE_1:45;
then
A12: v in InputVertices IIG or v in InnerVertices IIG by XBOOLE_0:def 3;
v in InputVertices IIG implies it1.v = s.v by A6;
hence contradiction by A7,A10,A12,A11;
end;
end;
theorem Th12:
for SCS being non-empty Circuit of IIG, s being State of SCS, iv
being InputValues of SCS st iv c= s holds iv c= Following s
proof
let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of
SCS such that
A1: iv c= s;
now
dom s = the carrier of IIG by CIRCUIT1:3
.= dom Following s by CIRCUIT1:3;
hence dom iv c= dom Following s by A1,RELAT_1:11;
let x be object such that
A2: x in dom iv;
A3: dom iv = InputVertices IIG by PARTFUN1:def 2;
then reconsider v = x as Vertex of IIG by A2;
iv.v = s.v by A1,A2,GRFUNC_1:2;
hence iv.x = (Following s).x by A2,A3,Def5;
end;
hence thesis by GRFUNC_1:2;
end;
definition
let IIG be Circuit-like non void non empty ManySortedSign;
let SCS be non-empty Circuit of IIG;
let IT be State of SCS;
attr IT is stable means
IT = Following IT;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of
SCS;
func Following(s,iv) -> State of SCS equals
Following(s+*iv);
coherence;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State
of SCS;
func InitialComp(s,InpFs) -> State of SCS equals
s +* (0-th_InputValues
InpFs) +* Set-Constants SCS;
coherence
proof
set sc = Set-Constants SCS;
A1: dom sc = SortsWithConstants IIG by PARTFUN1:def 2;
A2: now
let x be set;
assume
A3: x in dom sc;
then reconsider v = x as Vertex of IIG by A1;
sc.x in Constants(SCS,v) by A3,CIRCUIT1:def 1;
hence sc.x in (the Sorts of SCS).x;
end;
dom the Sorts of SCS = the carrier of IIG by PARTFUN1:def 2;
hence thesis by A1,A2,PRE_CIRC:6;
end;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State
of SCS;
func Computation(s,InpFs) -> sequence of (product the Sorts of SCS)
means
:Def9:
it.0 = InitialComp(s,InpFs) & for i being Nat holds it.(i+1) =
Following(it.i,(i+1)-th_InputValues InpFs);
correctness
proof
deffunc F(Nat,State of SCS) = Following($2,($1+1)-th_InputValues InpFs);
thus (ex IT being sequence of product the Sorts of SCS st IT.0 =
InitialComp(s,InpFs) & for i being Nat holds IT.(i+1) = F(i,IT.i)) & for IT1,
IT2 being sequence of product the Sorts of SCS st (IT1.0 = InitialComp(s,
InpFs) & for i being Nat holds IT1.(i+1) = F(i,IT1.i)) & (IT2.0 = InitialComp(s
,InpFs) & for i being Nat holds IT2.(i+1) = F(i,IT2.i)) holds IT1 = IT2 from
PRE_CIRC:sch 3;
end;
end;
reserve SCS for non-empty Circuit of IIG;
reserve s for State of SCS;
reserve iv for InputValues of SCS;
theorem Th13:
for k being Nat st for v being Vertex of IIG st depth
(v,SCS) <= k holds s.v = IGValue(v,iv) holds for v1 being Vertex of IIG st
depth(v1,SCS) <= k+1 holds (Following s).v1 = IGValue(v1,iv)
proof
let k be Nat such that
A1: for v being Vertex of IIG st depth(v,SCS) <= k holds s.v = IGValue(v ,iv);
let v be Vertex of IIG such that
A2: depth(v,SCS) <= k+1;
v in the carrier of IIG;
then
A3: v in InputVertices IIG \/ InnerVertices IIG by XBOOLE_1:45;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: v in InputVertices IIG;
then
A5: depth(v,SCS) = 0 by CIRCUIT1:18;
thus (Following s).v = s.v by A4,Def5
.= IGValue(v,iv) by A1,A5,NAT_1:2;
end;
suppose
A6: v in InnerVertices IIG;
set F = Eval SCS;
set X = the Sorts of SCS;
set U1 = FreeEnv SCS;
set o = action_at v;
set taofo =the_arity_of o;
deffunc F(Nat) = IGTree((taofo/.$1) qua Vertex of IIG, iv);
consider p being FinSequence such that
A7: len p = len the_arity_of o and
A8: for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch
2;
A9: for k being Element of NAT st k in dom p holds p.k = F(k) by A8;
A10: now
let k be Nat;
assume k in dom p;
then p.k = IGTree(taofo/.k, iv) by A8;
hence p.k in (the Sorts of U1).((the_arity_of o)/.k);
end;
U1 = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 14;
then
A11: Den(o,U1) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o,X) by MSAFREE:def 13;
reconsider ods = o depends_on_in s as Function;
A12: F is_homomorphism U1, SCS by MSAFREE2:def 9;
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
then
A13: ((the Sorts of SCS)# * the Arity of IIG).o = (the Sorts of SCS)#.((
the Arity of IIG).o) by FUNCT_1:13
.= (the Sorts of SCS)#.(the_arity_of o) by MSUALG_1:def 1
.= product ((the Sorts of SCS) * the_arity_of o) by FINSEQ_2:def 5;
A14: dom p = dom the_arity_of o by A7,FINSEQ_3:29;
reconsider p as Element of Args(o,U1) by A7,A10,MSAFREE2:5;
A15: U1 = MSAlgebra (# FreeSort(X), FreeOper(X) #) & Args(o,U1) = ((the
Sorts of U1)# * the Arity of IIG).o by MSAFREE:def 14,MSUALG_1:def 4;
then reconsider p9 = p as FinSequence of TS(DTConMSA(X)) by MSAFREE:8;
Sym(o,X) ==> roots p9 by A15,MSAFREE:10;
then
A16: Den(o,U1).p = (Sym(o,X))-tree p9 by A11,MSAFREE:def 12
.= [o,the carrier of IIG]-tree p9 by MSAFREE:def 9
.= IGTree(v,iv) by A6,A9,A14,Th9;
reconsider Fp = F#p as Function;
A17: Args(o,SCS) = ((the Sorts of SCS)# * the Arity of IIG).o by MSUALG_1:def 4
;
now
dom the Sorts of SCS = the carrier of IIG & rng the_arity_of o c=
the carrier of IIG by FINSEQ_1:def 4,PARTFUN1:def 2;
hence dom the_arity_of o = dom ((the Sorts of SCS) * the_arity_of o) by
RELAT_1:27
.= dom Fp by A13,A17,CARD_3:9;
dom s = the carrier of IIG & rng the_arity_of o c= the carrier of
IIG by CIRCUIT1:3,FINSEQ_1:def 4;
hence dom the_arity_of o = dom (s * the_arity_of o) by RELAT_1:27
.= dom ods by CIRCUIT1:def 3;
let x be object;
reconsider v1 = (the_arity_of o)/.x as Element of IIG;
assume
A18: x in dom the_arity_of o;
then reconsider x9 = x as Element of NAT;
A19: v1 = (the_arity_of o).x9 by A18,PARTFUN1:def 6;
then v1 in rng the_arity_of o by A18,FUNCT_1:def 3;
then depth(v1,SCS) < k+1 by A2,A6,CIRCUIT1:19,XXREAL_0:2;
then
A20: depth(v1,SCS) <= k by NAT_1:13;
thus Fp.x = (F.v1).(p9.x9) by A14,A18,MSUALG_3:def 6
.= IGValue(v1,iv) by A8,A14,A18
.= s.v1 by A1,A20
.= (s * (the_arity_of o)).x by A18,A19,FUNCT_1:13
.= ods.x by CIRCUIT1:def 3;
end;
then F#p = o depends_on_in s by FUNCT_1:2;
hence (Following s).v = Den(o,SCS).(F#p) by A6,Def5
.= (F.(the_result_sort_of o)).(Den(o,U1).p) by A12,MSUALG_3:def 7
.= IGValue(v,iv) by A6,A16,MSAFREE2:def 7;
end;
end;
reserve IIG for finite monotonic Circuit-like non void non empty
ManySortedSign;
reserve SCS for non-empty Circuit of IIG;
reserve InpFs for InputFuncs of SCS;
reserve s for State of SCS;
reserve iv for InputValues of SCS;
theorem Th14:
commute InpFs is constant & InputVertices IIG is non empty
implies for s, iv st iv = (commute InpFs).0 for k being Nat holds iv
c= (Computation(s,InpFs)).k
proof
assume that
A1: commute InpFs is constant and
A2: InputVertices IIG is non empty;
A3: dom commute InpFs = NAT by A2,PRE_CIRC:5;
let s, iv;
assume
A4: iv = (commute InpFs).0;
let k be Nat;
A5: k in NAT by ORDINAL1:def 12;
IIG is with_input_V by A2;
then
A6: k-th_InputValues InpFs = (commute InpFs).k by CIRCUIT1:def 2
.= iv by A1,A4,A3,FUNCT_1:def 10,A5;
set Ck = (Computation(s,InpFs)).k;
dom iv = InputVertices IIG & dom Set-Constants SCS = SortsWithConstants
IIG by PARTFUN1:def 2;
then
A7: dom iv misses dom Set-Constants SCS by MSAFREE2:4;
per cases by NAT_1:6;
suppose
A8: k = 0;
then Ck = InitialComp(s,InpFs) by Def9
.= s +* (0-th_InputValues InpFs) +* Set-Constants SCS;
hence thesis by A6,A7,A8,FUNCT_4:25,124;
end;
suppose
ex n being Nat st k=n+1;
then consider n being Nat such that
A9: k=n+1;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider Cn = (Computation(s,InpFs)).n as State of SCS;
Ck = Following(Cn,k-th_InputValues InpFs) by A9,Def9
.= Following(Cn+*iv) by A6;
hence thesis by Th12,FUNCT_4:25;
end;
end;
theorem
for n being Element of NAT st commute InpFs is constant &
InputVertices IIG is non empty & (Computation(s,InpFs)).n is stable
for m being Nat st n <= m
holds (Computation(s,InpFs)).n = (Computation(s,InpFs)).m
proof
let n be Element of NAT such that
A1: commute InpFs is constant and
A2: InputVertices IIG is non empty and
A3: (Computation(s,InpFs)).n is stable;
defpred P[Nat] means n <= $1 implies (Computation(s,InpFs)).n = (
Computation(s,InpFs)).$1;
A4: now
let m be Nat;
assume
A5: P[m];
thus P[m+1]
proof
A6: IIG is with_input_V by A2;
then reconsider iv = (commute InpFs).0 as InputValues of SCS by
CIRCUIT1:2;
reconsider Ckm = (Computation(s,InpFs)).m as State of SCS;
A7: dom commute InpFs = NAT by A2,PRE_CIRC:5;
(m+1)-th_InputValues InpFs = (commute InpFs).(m+1) by A6,CIRCUIT1:def 2
.= iv by A1,A7,FUNCT_1:def 10;
then
A8: (m+1)-th_InputValues InpFs c= (Computation(s,InpFs)).m by A1,A2,Th14;
assume
A9: n <= m+1;
per cases by A9,NAT_1:8;
suppose
n <= m;
hence (Computation(s,InpFs)).n = Following Ckm by A3,A5
.= Following((Computation(s,InpFs)).m, (m+1)-th_InputValues InpFs)
by A8,FUNCT_4:98
.= (Computation(s,InpFs)).(m+1) by Def9;
end;
suppose
n = m+1;
hence thesis;
end;
end;
end;
A10: P[ 0 ] by NAT_1:3;
thus for m being Nat holds P[m] from NAT_1:sch 2(A10,A4);
end;
theorem Th16:
commute InpFs is constant & InputVertices IIG is non empty
implies for s, iv st iv = (commute InpFs).0 for k being Nat, v being
Vertex of IIG st depth(v,SCS) <= k holds ((Computation(s,InpFs)).k qua Element
of product the Sorts of SCS).v = IGValue(v,iv)
proof
assume that
A1: commute InpFs is constant and
A2: InputVertices IIG is non empty;
let s, iv;
assume
A3: iv = (commute InpFs).0;
defpred P[Nat] means for v being Vertex of IIG st depth(v,SCS) <=
$1 holds ((Computation(s,InpFs)).$1 qua State of SCS).v = IGValue(v,iv);
A4: IIG is with_input_V by A2;
A5: P[ 0 ]
proof
let v be Vertex of IIG;
assume depth(v,SCS) <= 0;
then
A6: depth(v,SCS) = 0 by NAT_1:3;
A7: (Computation(s,InpFs)).0 = InitialComp(s,InpFs) by Def9
.= s +* (0-th_InputValues InpFs) +* Set-Constants SCS;
per cases by A6,CIRCUIT1:18;
suppose
A8: v in InputVertices IIG;
A9: dom (0-th_InputValues InpFs) = InputVertices IIG by PARTFUN1:def 2;
InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
then not v in SortsWithConstants IIG by A8,XBOOLE_0:3;
then not v in dom Set-Constants SCS by PARTFUN1:def 2;
hence
((Computation(s,InpFs)).0 qua Element of product the Sorts of SCS).
v = (s +* (0-th_InputValues InpFs)).v by A7,FUNCT_4:11
.= (0-th_InputValues InpFs).v by A8,A9,FUNCT_4:13
.= iv.v by A4,A3,CIRCUIT1:def 2
.= IGValue(v,iv) by A8,Th10;
end;
suppose
A10: v in SortsWithConstants IIG;
then v in dom Set-Constants SCS by PARTFUN1:def 2;
hence
((Computation(s,InpFs)).0 qua Element of product the Sorts of SCS).
v = (Set-Constants SCS).v by A7,FUNCT_4:13
.= IGValue(v,iv) by A10,Th11;
end;
end;
A11: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider Ck = (Computation(s,InpFs)).k as State of SCS;
assume
A12: P[k];
let v be Vertex of IIG such that
A13: depth(v,SCS) <= k+1;
A14: dom commute InpFs = NAT by A2,PRE_CIRC:5;
A15: (k+1)-th_InputValues InpFs = (commute InpFs).(k+1) by A4,CIRCUIT1:def 2
.= (commute InpFs).0 by A1,A14,FUNCT_1:def 10;
A16: iv c= Ck by A1,A2,A3,Th14;
thus ((Computation(s,InpFs)).(k+1) qua State of SCS).v = (Following(Ck,(k+
1)-th_InputValues InpFs)).v by Def9
.= (Following Ck).v by A3,A15,A16,FUNCT_4:98
.= IGValue(v,iv) by A12,A13,Th13;
end;
thus for k being Nat holds P[k] from NAT_1:sch 2(A5,A11);
end;
theorem Th17:
commute InpFs is constant & InputVertices IIG is non empty & iv
= (commute InpFs).0 implies for s being State of SCS, v being Vertex of IIG, n
being Element of NAT st n = depth SCS holds ((Computation(s,InpFs)).n qua State
of SCS).v = IGValue(v,iv)
proof
assume
A1: commute InpFs is constant & InputVertices IIG is non empty & iv = (
commute InpFs).0;
let s be State of SCS, v be Vertex of IIG;
A2: depth(v,SCS) <= depth SCS by CIRCUIT1:17;
let n be Element of NAT;
assume n = depth SCS;
hence thesis by A1,A2,Th16;
end;
theorem
commute InpFs is constant & InputVertices IIG is non empty implies for
s being State of SCS, n be Element of NAT st n = depth SCS holds (Computation(s
,InpFs)).n is stable
proof
assume that
A1: commute InpFs is constant and
A2: InputVertices IIG is non empty;
A3: dom commute InpFs = NAT by A2,PRE_CIRC:5;
A4: IIG is with_input_V by A2;
then reconsider iv = (commute InpFs).0 as InputValues of SCS by CIRCUIT1:2;
let s be State of SCS, n be Element of NAT such that
A5: n = depth SCS;
reconsider Cn = (Computation(s,InpFs)).n as State of SCS;
A6: iv c= Cn by A1,A2,Th14;
A7: (n+1)-th_InputValues InpFs = (commute InpFs).(n+1) by A4,CIRCUIT1:def 2
.= (commute InpFs).0 by A1,A3,FUNCT_1:def 10;
reconsider Cn1 = (Computation(s,InpFs)).(n+1) as State of SCS;
now
thus the carrier of IIG = dom Cn by CIRCUIT1:3;
thus the carrier of IIG = dom Cn1 by CIRCUIT1:3;
let x be object;
assume x in the carrier of IIG;
then reconsider x9 = x as Vertex of IIG;
A8: depth(x9,SCS) <= n by A5,CIRCUIT1:17;
then Cn.x9 = IGValue(x9,iv) by A1,A2,Th16;
hence Cn.x = Cn1.x by A1,A2,A8,Th16,NAT_1:12;
end;
hence (Computation(s,InpFs)).n = (Computation(s,InpFs)).(n+1)
.= Following(Cn,(n+1)-th_InputValues InpFs) by Def9
.= Following((Computation(s,InpFs)).n) by A7,A6,FUNCT_4:98;
end;
theorem
commute InpFs is constant & InputVertices IIG is non empty implies for
s1, s2 being State of SCS holds (Computation(s1,InpFs)).(depth SCS) = (
Computation(s2,InpFs)).(depth SCS)
proof
assume that
A1: commute InpFs is constant and
A2: InputVertices IIG is non empty;
IIG is with_input_V by A2;
then reconsider iv = (commute InpFs).0 as InputValues of SCS by CIRCUIT1:2;
reconsider dSCS = depth SCS as Element of NAT by ORDINAL1:def 12;
let s1, s2 be State of SCS;
reconsider Cs1 = (Computation(s1,InpFs)).dSCS as State of SCS;
reconsider Cs2 = (Computation(s2,InpFs)).dSCS as State of SCS;
now
thus the carrier of IIG = dom Cs1 by CIRCUIT1:3;
thus the carrier of IIG = dom Cs2 by CIRCUIT1:3;
let x be object;
assume x in the carrier of IIG;
then reconsider x9 = x as Vertex of IIG;
Cs1.x9 = IGValue(x9,iv) by A1,A2,Th17;
hence Cs1.x = Cs2.x by A1,A2,Th17;
end;
hence thesis;
end;