:: CIRCTRM1 semantic presentation
begin
theorem Th1: :: CIRCTRM1:1
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A
for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
let V be Variables of A; ::_thesis: for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
defpred S1[ set ] means for t9 being Term of S,V
for T being c-Term of A,V st t9 = $1 & T = t9 holds
the_sort_of T = the_sort_of t9;
A1: for s being SortSymbol of S
for v being Element of V . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]]
let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]]
let t be Term of S,V; ::_thesis: for T being c-Term of A,V st t = root-tree [v,s] & T = t holds
the_sort_of T = the_sort_of t
let T be c-Term of A,V; ::_thesis: ( t = root-tree [v,s] & T = t implies the_sort_of T = the_sort_of t )
assume that
A2: t = root-tree [v,s] and
A3: T = t ; ::_thesis: the_sort_of T = the_sort_of t
the_sort_of t = s by A2, MSATERM:14;
hence the_sort_of T = the_sort_of t by A2, A3, MSATERM:16; ::_thesis: verum
end;
A4: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds
S1[t9] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds
S1[t9] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t9 being Term of S,V st t9 in rng p holds
S1[t9] ) implies S1[[o, the carrier of S] -tree p] )
assume for t9 being Term of S,V st t9 in rng p holds
for t being Term of S,V
for T being c-Term of A,V st t = t9 & T = t holds
the_sort_of T = the_sort_of t ; ::_thesis: S1[[o, the carrier of S] -tree p]
let t be Term of S,V; ::_thesis: for T being c-Term of A,V st t = [o, the carrier of S] -tree p & T = t holds
the_sort_of T = the_sort_of t
let T be c-Term of A,V; ::_thesis: ( t = [o, the carrier of S] -tree p & T = t implies the_sort_of T = the_sort_of t )
assume t = [o, the carrier of S] -tree p ; ::_thesis: ( not T = t or the_sort_of T = the_sort_of t )
then A5: t . {} = [o, the carrier of S] by TREES_4:def_4;
then the_sort_of t = the_result_sort_of o by MSATERM:17;
hence ( not T = t or the_sort_of T = the_sort_of t ) by A5, MSATERM:17; ::_thesis: verum
end;
for t being Term of S,V holds S1[t] from MSATERM:sch_1(A1, A4);
hence for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
funcX -CircuitStr -> non empty strict ManySortedSign equals :: CIRCTRM1:def 1
ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #);
correctness
coherence
ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #) is non empty strict ManySortedSign ;
;
end;
:: deftheorem defines -CircuitStr CIRCTRM1:def_1_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds X -CircuitStr = ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #);
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
clusterX -CircuitStr -> non empty strict unsplit ;
coherence
X -CircuitStr is unsplit
proof
thus the ResultSort of (X -CircuitStr) = id the carrier' of (X -CircuitStr) ; :: according to CIRCCOMB:def_7 ::_thesis: verum
end;
end;
theorem :: CIRCTRM1:2
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( X -CircuitStr is void iff for t being Element of X holds
( t is root & not t . {} in [: the carrier' of S,{ the carrier of S}:] ) ) by TREES_9:25;
theorem Th3: :: CIRCTRM1:3
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
let X be non empty Subset of (S -Terms V); ::_thesis: ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
hereby ::_thesis: ( not X -CircuitStr is void implies X is SetWithCompoundTerm of S,V )
assume X is SetWithCompoundTerm of S,V ; ::_thesis: not X -CircuitStr is void
then consider t being CompoundTerm of S,V such that
A1: t in X by MSATERM:def_7;
t . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def_6;
hence not X -CircuitStr is void by A1, TREES_9:25; ::_thesis: verum
end;
assume not X -CircuitStr is void ; ::_thesis: X is SetWithCompoundTerm of S,V
then consider t being Element of X such that
A2: ( not t is root or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by TREES_9:25;
t is CompoundTerm of S,V by A2, MSATERM:28, MSATERM:def_6;
hence X is SetWithCompoundTerm of S,V by MSATERM:def_7; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
clusterX -CircuitStr -> non empty non void strict ;
coherence
not X -CircuitStr is void by Th3;
end;
theorem Th4: :: CIRCTRM1:4
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) holds
( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
let X be non empty Subset of (S -Terms V); ::_thesis: ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
set C = [: the carrier' of S,{ the carrier of S}:];
hereby ::_thesis: for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V
let v be Vertex of (X -CircuitStr); ::_thesis: v is Term of S,V
consider t being Element of X, p being Node of t such that
A1: v = t | p by TREES_9:19;
thus v is Term of S,V by A1; ::_thesis: verum
end;
let s be set ; ::_thesis: ( s in the carrier' of (X -CircuitStr) implies s is CompoundTerm of S,V )
assume s in the carrier' of (X -CircuitStr) ; ::_thesis: s is CompoundTerm of S,V
then consider t being Element of X, p being Node of t such that
A2: s = t | p and
A3: ( not p in Leaves (dom t) or t . p in [: the carrier' of S,{ the carrier of S}:] ) by TREES_9:24;
reconsider s = s as Term of S,V by A2;
reconsider e = {} as Node of (t | p) by TREES_1:22;
A4: dom (t | p) = (dom t) | p by TREES_2:def_10;
p = p ^ e by FINSEQ_1:34;
then A5: t . p = s . e by A2, A4, TREES_2:def_10;
( p in Leaves (dom t) iff s is root ) by A2, TREES_9:6;
hence s is CompoundTerm of S,V by A3, A5, MSATERM:28, MSATERM:def_6; ::_thesis: verum
end;
theorem Th5: :: CIRCTRM1:5
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
let X be non empty Subset of (S -Terms V); ::_thesis: for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
let t be Vertex of (X -CircuitStr); ::_thesis: ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
thus ( t in the carrier' of (X -CircuitStr) implies t is CompoundTerm of S,V ) by Th4; ::_thesis: ( t is CompoundTerm of S,V implies t in the carrier' of (X -CircuitStr) )
set C = [: the carrier' of S,{ the carrier of S}:];
consider tt being Element of X, p being Node of tt such that
A1: t = tt | p by TREES_9:19;
assume t is CompoundTerm of S,V ; ::_thesis: t in the carrier' of (X -CircuitStr)
then reconsider t9 = t as CompoundTerm of S,V ;
A2: t9 . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def_6;
A3: p ^ (<*> NAT) = p by FINSEQ_1:34;
{} in (dom tt) | p by TREES_1:22;
then tt . p in [: the carrier' of S,{ the carrier of S}:] by A1, A2, A3, TREES_2:def_10;
hence t in the carrier' of (X -CircuitStr) by A1, TREES_9:24; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
let g be Gate of (X -CircuitStr);
cluster the_arity_of g -> DTree-yielding ;
coherence
the_arity_of g is DTree-yielding ;
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
cluster -> Relation-like Function-like finite for Element of the carrier of (X -CircuitStr);
coherence
for b1 being Vertex of (X -CircuitStr) holds
( b1 is finite & b1 is Function-like & b1 is Relation-like ) by Th4;
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
cluster -> DecoratedTree-like for Element of the carrier of (X -CircuitStr);
coherence
for b1 being Vertex of (X -CircuitStr) holds b1 is DecoratedTree-like ;
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> Relation-like Function-like finite for Element of the carrier' of (X -CircuitStr);
coherence
for b1 being Gate of (X -CircuitStr) holds
( b1 is finite & b1 is Function-like & b1 is Relation-like ) by Th4;
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> DecoratedTree-like for Element of the carrier' of (X -CircuitStr);
coherence
for b1 being Gate of (X -CircuitStr) holds b1 is DecoratedTree-like ;
end;
theorem Th6: :: CIRCTRM1:6
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let t1, t2 be non empty Subset of (S -Terms V); ::_thesis: ( the Arity of (t1 -CircuitStr) tolerates the Arity of (t2 -CircuitStr) & the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr) )
set C = [: the carrier' of S,{ the carrier of S}:];
A1: dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1 by FUNCT_2:def_1;
A2: dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t1)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1 ;
A3: dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t2) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2 by FUNCT_2:def_1;
A4: dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t2)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2 ;
hereby :: according to PARTFUN1:def_4 ::_thesis: the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr)
let x be set ; ::_thesis: ( x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) implies the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x )
assume A5: x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) ; ::_thesis: the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x
then A6: x in dom the Arity of (t1 -CircuitStr) by XBOOLE_0:def_4;
A7: x in dom the Arity of (t2 -CircuitStr) by A5, XBOOLE_0:def_4;
reconsider u = x as Element of Subtrees t1 by A1, A6;
([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) . x in (Subtrees t1) * by A1, A6, FUNCT_2:5;
then reconsider y1 = the Arity of (t1 -CircuitStr) . x as FinSequence of Subtrees t1 by FINSEQ_1:def_11;
the Arity of (t2 -CircuitStr) . x in (Subtrees t2) * by A3, A7, FUNCT_2:5;
then reconsider y2 = the Arity of (t2 -CircuitStr) . x as FinSequence of Subtrees t2 by FINSEQ_1:def_11;
A8: ( ( for t being Element of t1 holds t is finite ) & ( for t being Element of t2 holds t is finite ) ) ;
then A9: u = (u . {}) -tree y1 by A1, A6, TREES_9:def_13;
u = (u . {}) -tree y2 by A3, A7, A8, TREES_9:def_13;
hence the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x by A9, TREES_4:15; ::_thesis: verum
end;
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the ResultSort of (t1 -CircuitStr)) /\ (proj1 the ResultSort of (t2 -CircuitStr)) or the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x )
assume A10: x in (dom the ResultSort of (t1 -CircuitStr)) /\ (dom the ResultSort of (t2 -CircuitStr)) ; ::_thesis: the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x
then A11: x in dom the ResultSort of (t1 -CircuitStr) by XBOOLE_0:def_4;
A12: x in dom the ResultSort of (t2 -CircuitStr) by A10, XBOOLE_0:def_4;
thus the ResultSort of (t1 -CircuitStr) . x = x by A2, A11, FUNCT_1:18
.= the ResultSort of (t2 -CircuitStr) . x by A4, A12, FUNCT_1:18 ; ::_thesis: verum
end;
registration
let X, Y be constituted-DTrees set ;
clusterX \/ Y -> constituted-DTrees ;
coherence
X \/ Y is constituted-DTrees by TREES_3:9;
end;
theorem Th7: :: CIRCTRM1:7
for X1, X2 being non empty constituted-DTrees set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2)
proof
let X1, X2 be non empty constituted-DTrees set ; ::_thesis: Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (Subtrees X1) \/ (Subtrees X2) c= Subtrees (X1 \/ X2)
let x be set ; ::_thesis: ( x in Subtrees (X1 \/ X2) implies x in (Subtrees X1) \/ (Subtrees X2) )
assume x in Subtrees (X1 \/ X2) ; ::_thesis: x in (Subtrees X1) \/ (Subtrees X2)
then consider t being Element of X1 \/ X2, n being Node of t such that
A1: x = t | n by TREES_9:19;
( t in X1 or t in X2 ) by XBOOLE_0:def_3;
then ( x in Subtrees X1 or x in Subtrees X2 ) by A1, TREES_9:19;
hence x in (Subtrees X1) \/ (Subtrees X2) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Subtrees X1) \/ (Subtrees X2) or x in Subtrees (X1 \/ X2) )
assume A2: x in (Subtrees X1) \/ (Subtrees X2) ; ::_thesis: x in Subtrees (X1 \/ X2)
percases ( x in Subtrees X1 or x in Subtrees X2 ) by A2, XBOOLE_0:def_3;
suppose x in Subtrees X1 ; ::_thesis: x in Subtrees (X1 \/ X2)
then consider t being Element of X1, n being Node of t such that
A3: x = t | n by TREES_9:19;
t is Element of X1 \/ X2 by XBOOLE_0:def_3;
hence x in Subtrees (X1 \/ X2) by A3, TREES_9:19; ::_thesis: verum
end;
suppose x in Subtrees X2 ; ::_thesis: x in Subtrees (X1 \/ X2)
then consider t being Element of X2, n being Node of t such that
A4: x = t | n by TREES_9:19;
t is Element of X1 \/ X2 by XBOOLE_0:def_3;
hence x in Subtrees (X1 \/ X2) by A4, TREES_9:19; ::_thesis: verum
end;
end;
end;
theorem Th8: :: CIRCTRM1:8
for X1, X2 being non empty constituted-DTrees set
for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)
proof
let X1, X2 be non empty constituted-DTrees set ; ::_thesis: for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)
let C be set ; ::_thesis: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (C -Subtrees X1) \/ (C -Subtrees X2) c= C -Subtrees (X1 \/ X2)
let x be set ; ::_thesis: ( x in C -Subtrees (X1 \/ X2) implies x in (C -Subtrees X1) \/ (C -Subtrees X2) )
assume x in C -Subtrees (X1 \/ X2) ; ::_thesis: x in (C -Subtrees X1) \/ (C -Subtrees X2)
then consider t being Element of X1 \/ X2, n being Node of t such that
A1: x = t | n and
A2: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
( t in X1 or t in X2 ) by XBOOLE_0:def_3;
then ( x in C -Subtrees X1 or x in C -Subtrees X2 ) by A1, A2, TREES_9:24;
hence x in (C -Subtrees X1) \/ (C -Subtrees X2) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (C -Subtrees X1) \/ (C -Subtrees X2) or x in C -Subtrees (X1 \/ X2) )
assume A3: x in (C -Subtrees X1) \/ (C -Subtrees X2) ; ::_thesis: x in C -Subtrees (X1 \/ X2)
percases ( x in C -Subtrees X1 or x in C -Subtrees X2 ) by A3, XBOOLE_0:def_3;
suppose x in C -Subtrees X1 ; ::_thesis: x in C -Subtrees (X1 \/ X2)
then consider t being Element of X1, n being Node of t such that
A4: x = t | n and
A5: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
t is Element of X1 \/ X2 by XBOOLE_0:def_3;
hence x in C -Subtrees (X1 \/ X2) by A4, A5, TREES_9:24; ::_thesis: verum
end;
suppose x in C -Subtrees X2 ; ::_thesis: x in C -Subtrees (X1 \/ X2)
then consider t being Element of X2, n being Node of t such that
A6: x = t | n and
A7: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
t is Element of X1 \/ X2 by XBOOLE_0:def_3;
hence x in C -Subtrees (X1 \/ X2) by A6, A7, TREES_9:24; ::_thesis: verum
end;
end;
end;
theorem Th9: :: CIRCTRM1:9
for X1, X2 being non empty constituted-DTrees set st ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) holds
for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)
proof
let X1, X2 be non empty constituted-DTrees set ; ::_thesis: ( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) implies for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) )
assume that
A1: for t being Element of X1 holds t is finite and
A2: for t being Element of X2 holds t is finite ; ::_thesis: for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)
A3: now__::_thesis:_for_t_being_Element_of_X1_\/_X2_holds_t_is_finite
let t be Element of X1 \/ X2; ::_thesis: t is finite
( t in X1 or t in X2 ) by XBOOLE_0:def_3;
hence t is finite by A1, A2; ::_thesis: verum
end;
let C be set ; ::_thesis: C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)
set X = X1 \/ X2;
set f = C -ImmediateSubtrees (X1 \/ X2);
set f1 = C -ImmediateSubtrees X1;
set f2 = C -ImmediateSubtrees X2;
A4: dom (C -ImmediateSubtrees (X1 \/ X2)) = C -Subtrees (X1 \/ X2) by FUNCT_2:def_1;
A5: dom (C -ImmediateSubtrees X1) = C -Subtrees X1 by FUNCT_2:def_1;
A6: dom (C -ImmediateSubtrees X2) = C -Subtrees X2 by FUNCT_2:def_1;
A7: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) by Th8;
now__::_thesis:_for_x_being_set_st_x_in_(dom_(C_-ImmediateSubtrees_X1))_\/_(dom_(C_-ImmediateSubtrees_X2))_holds_
(_(_x_in_dom_(C_-ImmediateSubtrees_X2)_implies_(C_-ImmediateSubtrees_(X1_\/_X2))_._x_=_(C_-ImmediateSubtrees_X2)_._x_)_&_(_not_x_in_dom_(C_-ImmediateSubtrees_X2)_implies_(C_-ImmediateSubtrees_(X1_\/_X2))_._x_=_(C_-ImmediateSubtrees_X1)_._x_)_)
let x be set ; ::_thesis: ( x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) implies ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) ) )
assume A8: x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) ; ::_thesis: ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) )
then reconsider t = x as Element of Subtrees (X1 \/ X2) by A5, A6, A7;
(C -ImmediateSubtrees (X1 \/ X2)) . x in (Subtrees (X1 \/ X2)) * by A5, A6, A7, A8, FUNCT_2:5;
then reconsider p = (C -ImmediateSubtrees (X1 \/ X2)) . x as FinSequence of Subtrees (X1 \/ X2) by FINSEQ_1:def_11;
hereby ::_thesis: ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x )
assume A9: x in dom (C -ImmediateSubtrees X2) ; ::_thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x
then (C -ImmediateSubtrees X2) . x in (Subtrees X2) * by A6, FUNCT_2:5;
then reconsider p2 = (C -ImmediateSubtrees X2) . x as FinSequence of Subtrees X2 by FINSEQ_1:def_11;
A10: t = (t . {}) -tree p by A3, A5, A6, A7, A8, TREES_9:def_13;
t = (t . {}) -tree p2 by A2, A6, A9, TREES_9:def_13;
hence (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x by A10, TREES_4:15; ::_thesis: verum
end;
assume not x in dom (C -ImmediateSubtrees X2) ; ::_thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x
then A11: x in dom (C -ImmediateSubtrees X1) by A8, XBOOLE_0:def_3;
then (C -ImmediateSubtrees X1) . x in (Subtrees X1) * by A5, FUNCT_2:5;
then reconsider p1 = (C -ImmediateSubtrees X1) . x as FinSequence of Subtrees X1 by FINSEQ_1:def_11;
A12: t = (t . {}) -tree p by A3, A5, A6, A7, A8, TREES_9:def_13;
t = (t . {}) -tree p1 by A1, A5, A11, TREES_9:def_13;
hence (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x by A12, TREES_4:15; ::_thesis: verum
end;
hence C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) by A4, A5, A6, A7, FUNCT_4:def_1; ::_thesis: verum
end;
theorem Th10: :: CIRCTRM1:10
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
let X1, X2 be non empty Subset of (S -Terms V); ::_thesis: (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
set X = X1 \/ X2;
set C = [: the carrier' of S,{ the carrier of S}:];
A1: Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2) by Th7;
A2: [: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1) \/ ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2) by Th8;
( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) ) ;
then A3: [: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X1) +* ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X2) by Th9;
id ([: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2)) = (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1)) +* (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2)) by A2, FUNCT_4:22;
hence (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) by A1, A2, A3, CIRCCOMB:def_2; ::_thesis: verum
end;
theorem Th11: :: CIRCTRM1:11
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V)
for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
let X be non empty Subset of (S -Terms V); ::_thesis: for x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
set G = X -CircuitStr ;
A1: rng the ResultSort of (X -CircuitStr) = the carrier' of (X -CircuitStr) by RELAT_1:45;
let x be set ; ::_thesis: ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )
hereby ::_thesis: ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] implies x in InputVertices (X -CircuitStr) )
assume A2: x in InputVertices (X -CircuitStr) ; ::_thesis: ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] )
then A3: not x in the carrier' of (X -CircuitStr) by A1, XBOOLE_0:def_5;
thus x in Subtrees X by A2; ::_thesis: ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s]
reconsider t = x as Term of S,V by A2, Th4;
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
then ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t is CompoundTerm of S,V ) by MSATERM:def_6;
then consider s being SortSymbol of S, v being Element of V . s such that
A4: t . {} = [v,s] by A2, A3, Th5;
take s = s; ::_thesis: ex v being Element of V . s st x = root-tree [v,s]
reconsider v = v as Element of V . s ;
take v = v; ::_thesis: x = root-tree [v,s]
thus x = root-tree [v,s] by A4, MSATERM:5; ::_thesis: verum
end;
assume A5: x in Subtrees X ; ::_thesis: ( for s being SortSymbol of S
for v being Element of V . s holds not x = root-tree [v,s] or x in InputVertices (X -CircuitStr) )
given s being SortSymbol of S, v being Element of V . s such that A6: x = root-tree [v,s] ; ::_thesis: x in InputVertices (X -CircuitStr)
assume not x in InputVertices (X -CircuitStr) ; ::_thesis: contradiction
then x in the carrier' of (X -CircuitStr) by A1, A5, XBOOLE_0:def_5;
then reconsider t = x as CompoundTerm of S,V by Th4;
t . {} = [v,s] by A6, TREES_4:3;
then [v,s] in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def_6;
then s = the carrier of S by ZFMISC_1:106;
then s in s ;
hence contradiction ; ::_thesis: verum
end;
theorem Th12: :: CIRCTRM1:12
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let X be SetWithCompoundTerm of S,V; ::_thesis: for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let g be Gate of (X -CircuitStr); ::_thesis: g = (g . {}) -tree (the_arity_of g)
for t being Element of X holds t is finite ;
hence g = (g . {}) -tree (the_arity_of g) by TREES_9:def_13; ::_thesis: verum
end;
begin
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let v be Vertex of (X -CircuitStr);
let A be MSAlgebra over S;
func the_sort_of (v,A) -> set means :Def2: :: CIRCTRM1:def 2
for u being Term of S,V st u = v holds
it = the Sorts of A . (the_sort_of u);
uniqueness
for b1, b2 being set st ( for u being Term of S,V st u = v holds
b1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
b2 = the Sorts of A . (the_sort_of u) ) holds
b1 = b2
proof
let S1, S2 be set ; ::_thesis: ( ( for u being Term of S,V st u = v holds
S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
S2 = the Sorts of A . (the_sort_of u) ) implies S1 = S2 )
reconsider u = v as Term of S,V by Th4;
assume A1: ( ( for u being Term of S,V st u = v holds
S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
S2 = the Sorts of A . (the_sort_of u) ) & not S1 = S2 ) ; ::_thesis: contradiction
then S1 = the Sorts of A . (the_sort_of u) ;
hence contradiction by A1; ::_thesis: verum
end;
existence
ex b1 being set st
for u being Term of S,V st u = v holds
b1 = the Sorts of A . (the_sort_of u)
proof
reconsider u = v as Term of S,V by Th4;
take the Sorts of A . (the_sort_of u) ; ::_thesis: for u being Term of S,V st u = v holds
the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u)
thus for u being Term of S,V st u = v holds
the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u) ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines the_sort_of CIRCTRM1:def_2_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for v being Vertex of (X -CircuitStr)
for A being MSAlgebra over S
for b6 being set holds
( b6 = the_sort_of (v,A) iff for u being Term of S,V st u = v holds
b6 = the Sorts of A . (the_sort_of u) );
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let v be Vertex of (X -CircuitStr);
let A be non-empty MSAlgebra over S;
cluster the_sort_of (v,A) -> non empty ;
coherence
not the_sort_of (v,A) is empty
proof
reconsider u = v as Term of S,V by Th4;
the_sort_of (v,A) = the Sorts of A . (the_sort_of u) by Def2;
hence not the_sort_of (v,A) is empty ; ::_thesis: verum
end;
end;
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
assume A1: X is SetWithCompoundTerm of S,V ;
let o be Gate of (X -CircuitStr);
let A be MSAlgebra over S;
func the_action_of (o,A) -> Function means :Def3: :: CIRCTRM1:def 3
for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
it = the Charact of A . ((o9 . {}) `1);
uniqueness
for b1, b2 being Function st ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b2 = the Charact of A . ((o9 . {}) `1) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f2 = the Charact of A . ((o9 . {}) `1) ) implies f1 = f2 )
reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of (X9 -CircuitStr) ;
assume A2: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f2 = the Charact of A . ((o9 . {}) `1) ) & not f1 = f2 ) ; ::_thesis: contradiction
then f1 = the Charact of A . ((o9 . {}) `1) ;
hence contradiction by A2; ::_thesis: verum
end;
existence
ex b1 being Function st
for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b1 = the Charact of A . ((o9 . {}) `1)
proof
reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of (X9 -CircuitStr) ;
take the Charact of A . ((o9 . {}) `1) ; ::_thesis: for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1)
thus for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1) ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines the_action_of CIRCTRM1:def_3_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) st X is SetWithCompoundTerm of S,V holds
for o being Gate of (X -CircuitStr)
for A being MSAlgebra over S
for b6 being Function holds
( b6 = the_action_of (o,A) iff for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b6 = the Charact of A . ((o9 . {}) `1) );
scheme :: CIRCTRM1:sch 1
MSFuncEx{ F1() -> non empty set , F2() -> V2() ManySortedSet of F1(), F3() -> V2() ManySortedSet of F1(), P1[ set , set , set ] } :
ex f being ManySortedFunction of F2(),F3() st
for i being Element of F1()
for a being Element of F2() . i holds P1[i,a,(f . i) . a]
provided
A1: for i being Element of F1()
for a being Element of F2() . i ex b being Element of F3() . i st P1[i,a,b]
proof
defpred S1[ set , set ] means ex g being Function of (F2() . $1),(F3() . $1) st
( $2 = g & ( for a being set st a in F2() . $1 holds
P1[$1,a,g . a] ) );
A2: for i being set st i in F1() holds
ex y being set st S1[i,y]
proof
let i be set ; ::_thesis: ( i in F1() implies ex y being set st S1[i,y] )
assume i in F1() ; ::_thesis: ex y being set st S1[i,y]
then reconsider i = i as Element of F1() ;
defpred S2[ set , set ] means P1[i,$1,$2];
A3: for a being set st a in F2() . i holds
ex b being set st
( b in F3() . i & S2[a,b] )
proof
let a be set ; ::_thesis: ( a in F2() . i implies ex b being set st
( b in F3() . i & S2[a,b] ) )
assume a in F2() . i ; ::_thesis: ex b being set st
( b in F3() . i & S2[a,b] )
then ex b being Element of F3() . i st P1[i,a,b] by A1;
hence ex b being set st
( b in F3() . i & S2[a,b] ) ; ::_thesis: verum
end;
consider g being Function such that
A4: ( dom g = F2() . i & rng g c= F3() . i ) and
A5: for a being set st a in F2() . i holds
S2[a,g . a] from FUNCT_1:sch_5(A3);
take g ; ::_thesis: S1[i,g]
g is Function of (F2() . i),(F3() . i) by A4, FUNCT_2:2;
hence S1[i,g] by A5; ::_thesis: verum
end;
consider f being Function such that
A6: dom f = F1() and
A7: for i being set st i in F1() holds
S1[i,f . i] from CLASSES1:sch_1(A2);
reconsider f = f as ManySortedSet of F1() by A6, PARTFUN1:def_2, RELAT_1:def_18;
f is ManySortedFunction of F2(),F3()
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in F1() or f . i is Element of bool [:(F2() . i),(F3() . i):] )
assume i in F1() ; ::_thesis: f . i is Element of bool [:(F2() . i),(F3() . i):]
then ex g being Function of (F2() . i),(F3() . i) st
( f . i = g & ( for a being set st a in F2() . i holds
P1[i,a,g . a] ) ) by A7;
hence f . i is Element of bool [:(F2() . i),(F3() . i):] ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of F2(),F3() ;
take f ; ::_thesis: for i being Element of F1()
for a being Element of F2() . i holds P1[i,a,(f . i) . a]
let i be Element of F1(); ::_thesis: for a being Element of F2() . i holds P1[i,a,(f . i) . a]
let a be Element of F2() . i; ::_thesis: P1[i,a,(f . i) . a]
ex g being Function of (F2() . i),(F3() . i) st
( f . i = g & ( for a being set st a in F2() . i holds
P1[i,a,g . a] ) ) by A7;
hence P1[i,a,(f . i) . a] ; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be MSAlgebra over S;
funcX -CircuitSorts A -> ManySortedSet of the carrier of (X -CircuitStr) means :Def4: :: CIRCTRM1:def 4
for v being Vertex of (X -CircuitStr) holds it . v = the_sort_of (v,A);
uniqueness
for b1, b2 being ManySortedSet of the carrier of (X -CircuitStr) st ( for v being Vertex of (X -CircuitStr) holds b1 . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds b2 . v = the_sort_of (v,A) ) holds
b1 = b2
proof
let S1, S2 be ManySortedSet of the carrier of (X -CircuitStr); ::_thesis: ( ( for v being Vertex of (X -CircuitStr) holds S1 . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds S2 . v = the_sort_of (v,A) ) implies S1 = S2 )
assume that
A1: for v being Vertex of (X -CircuitStr) holds S1 . v = the_sort_of (v,A) and
A2: for v being Vertex of (X -CircuitStr) holds S2 . v = the_sort_of (v,A) ; ::_thesis: S1 = S2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(X_-CircuitStr)_holds_
S1_._x_=_S2_._x
let x be set ; ::_thesis: ( x in the carrier of (X -CircuitStr) implies S1 . x = S2 . x )
assume x in the carrier of (X -CircuitStr) ; ::_thesis: S1 . x = S2 . x
then reconsider v = x as Vertex of (X -CircuitStr) ;
thus S1 . x = the_sort_of (v,A) by A1
.= S2 . x by A2 ; ::_thesis: verum
end;
hence S1 = S2 by PBOOLE:3; ::_thesis: verum
end;
existence
ex b1 being ManySortedSet of the carrier of (X -CircuitStr) st
for v being Vertex of (X -CircuitStr) holds b1 . v = the_sort_of (v,A)
proof
deffunc H1( Vertex of (X -CircuitStr)) -> set = the_sort_of ($1,A);
thus ex f being ManySortedSet of the carrier of (X -CircuitStr) st
for d being Element of (X -CircuitStr) holds f . d = H1(d) from PBOOLE:sch_5(); ::_thesis: verum
end;
end;
:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def_4_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being MSAlgebra over S
for b5 being ManySortedSet of the carrier of (X -CircuitStr) holds
( b5 = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr) holds b5 . v = the_sort_of (v,A) );
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be non-empty MSAlgebra over S;
clusterX -CircuitSorts A -> V2() ;
coherence
X -CircuitSorts A is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of (X -CircuitStr) or not (X -CircuitSorts A) . i is empty )
assume i in the carrier of (X -CircuitStr) ; ::_thesis: not (X -CircuitSorts A) . i is empty
then reconsider i = i as Vertex of (X -CircuitStr) ;
(X -CircuitSorts A) . i = the_sort_of (i,A) by Def4;
hence not (X -CircuitSorts A) . i is empty ; ::_thesis: verum
end;
end;
theorem Th13: :: CIRCTRM1:13
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let A be non-empty MSAlgebra over S; ::_thesis: for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let t be SetWithCompoundTerm of S,V; ::_thesis: for g being Gate of (t -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let g be Gate of (t -CircuitStr); ::_thesis: for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
set X = t;
reconsider f = g as CompoundTerm of S,V by Th4;
reconsider ag = the_arity_of g as FinSequence of Subtrees t ;
A1: g = (f . {}) -tree ag by Th12;
let o be OperSymbol of S; ::_thesis: ( g . {} = [o, the carrier of S] implies (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) )
assume g . {} = [o, the carrier of S] ; ::_thesis: (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
then consider a being ArgumentSeq of Sym (o,V) such that
A2: f = [o, the carrier of S] -tree a by MSATERM:10;
A3: len a = len (the_arity_of o) by MSATERM:22;
A4: a = ag by A1, A2, TREES_4:15;
A5: dom (the_arity_of o) = Seg (len a) by A3, FINSEQ_1:def_3;
A6: dom (the_arity_of g) = Seg (len a) by A4, FINSEQ_1:def_3;
A7: rng (the_arity_of g) c= the carrier of (t -CircuitStr) by FINSEQ_1:def_4;
A8: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
A9: dom (t -CircuitSorts A) = the carrier of (t -CircuitStr) by PARTFUN1:def_2;
A10: dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
A11: dom ((t -CircuitSorts A) * (the_arity_of g)) = Seg (len a) by A6, A7, A9, RELAT_1:27;
A12: dom ( the Sorts of A * (the_arity_of o)) = Seg (len a) by A5, A8, A10, RELAT_1:27;
now__::_thesis:_for_i_being_set_st_i_in_Seg_(len_a)_holds_
((t_-CircuitSorts_A)_*_(the_arity_of_g))_._i_=_(_the_Sorts_of_A_*_(the_arity_of_o))_._i
let i be set ; ::_thesis: ( i in Seg (len a) implies ((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i )
assume A13: i in Seg (len a) ; ::_thesis: ((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i
then reconsider j = i as Element of NAT ;
ag . i in rng (the_arity_of g) by A6, A13, FUNCT_1:def_3;
then reconsider v = ag . j as Vertex of (t -CircuitStr) by A7;
(the_arity_of o) . i in rng (the_arity_of o) by A5, A13, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . j as SortSymbol of S by A8;
reconsider u = v as Term of S,V by A4, A6, A13, MSATERM:22;
A14: the_sort_of u = s by A4, A6, A13, MSATERM:23;
A15: ((t -CircuitSorts A) * (the_arity_of g)) . i = (t -CircuitSorts A) . v by A11, A13, FUNCT_1:12;
A16: ( the Sorts of A * (the_arity_of o)) . i = the Sorts of A . s by A12, A13, FUNCT_1:12;
thus ((t -CircuitSorts A) * (the_arity_of g)) . i = the_sort_of (v,A) by A15, Def4
.= ( the Sorts of A * (the_arity_of o)) . i by A14, A16, Def2 ; ::_thesis: verum
end;
hence (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) by A11, A12, FUNCT_1:2; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be non-empty MSAlgebra over S;
funcX -CircuitCharact A -> ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) means :Def5: :: CIRCTRM1:def 5
for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
it . g = the_action_of (g,A);
uniqueness
for b1, b2 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b2 . g = the_action_of (g,A) ) holds
b1 = b2
proof
let C1, C2 be ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr); ::_thesis: ( ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
C1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
C2 . g = the_action_of (g,A) ) implies C1 = C2 )
assume that
A1: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds
C1 . o = the_action_of (o,A) and
A2: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds
C2 . o = the_action_of (o,A) ; ::_thesis: C1 = C2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_(X_-CircuitStr)_holds_
C1_._x_=_C2_._x
let x be set ; ::_thesis: ( x in the carrier' of (X -CircuitStr) implies C1 . x = C2 . x )
assume A3: x in the carrier' of (X -CircuitStr) ; ::_thesis: C1 . x = C2 . x
then reconsider o = x as Gate of (X -CircuitStr) ;
C1 . o = the_action_of (o,A) by A1, A3;
hence C1 . x = C2 . x by A2, A3; ::_thesis: verum
end;
hence C1 = C2 by PBOOLE:3; ::_thesis: verum
end;
existence
ex b1 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st
for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b1 . g = the_action_of (g,A)
proof
defpred S1[ set , set ] means ex g being Gate of (X -CircuitStr) st
( g = $1 & $2 = the_action_of (g,A) );
A4: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_(X_-CircuitStr)_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in the carrier' of (X -CircuitStr) implies ex y being set st S1[x,y] )
assume x in the carrier' of (X -CircuitStr) ; ::_thesis: ex y being set st S1[x,y]
then reconsider g = x as Gate of (X -CircuitStr) ;
reconsider y = the_action_of (g,A) as set ;
take y = y; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider CHARACT being ManySortedSet of the carrier' of (X -CircuitStr) such that
A5: for x being set st x in the carrier' of (X -CircuitStr) holds
S1[x,CHARACT . x] from PBOOLE:sch_3(A4);
A6: dom CHARACT = the carrier' of (X -CircuitStr) by PARTFUN1:def_2;
CHARACT is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 CHARACT or CHARACT . x is set )
assume x in dom CHARACT ; ::_thesis: CHARACT . x is set
then ex g being Gate of (X -CircuitStr) st
( g = x & CHARACT . x = the_action_of (g,A) ) by A5, A6;
hence CHARACT . x is set ; ::_thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of the carrier' of (X -CircuitStr) ;
CHARACT is ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr)
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in the carrier' of (X -CircuitStr) or CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] )
assume A7: i in the carrier' of (X -CircuitStr) ; ::_thesis: CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):]
then not X -CircuitStr is void ;
then reconsider X9 = X as SetWithCompoundTerm of S,V by Th3;
reconsider g = i as Gate of (X9 -CircuitStr) by A7;
A8: the_result_sort_of g = g by FUNCT_1:18;
then reconsider v = g as Vertex of (X9 -CircuitStr) ;
reconsider I = i as CompoundTerm of S,V by A7, Th4;
I . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def_6;
then consider o, y being set such that
A9: o in the carrier' of S and
A10: y in { the carrier of S} and
A11: I . {} = [o,y] by ZFMISC_1:84;
reconsider o = o as OperSymbol of S by A9;
A12: o = (I . {}) `1 by A11, MCART_1:7;
A13: y = the carrier of S by A10, TARSKI:def_1;
ex g being Gate of (X -CircuitStr) st
( g = i & CHARACT . i = the_action_of (g,A) ) by A5, A7;
then A14: CHARACT . i = the_action_of (g,A)
.= the Charact of A . o by A12, Def3 ;
A15: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . (the_result_sort_of o) by FUNCT_2:15
.= the Sorts of A . (the_sort_of I) by A11, A13, MSATERM:17 ;
A16: ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . g = (X -CircuitSorts A) . (the_result_sort_of g) by FUNCT_2:15
.= the_sort_of (v,A) by A8, Def4
.= the Sorts of A . (the_sort_of I) by Def2 ;
A17: (((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . g = ((X -CircuitSorts A) #) . (the_arity_of g) by FUNCT_2:15
.= product ((X9 -CircuitSorts A) * (the_arity_of g)) by FINSEQ_2:def_5
.= product ( the Sorts of A * (the_arity_of o)) by A11, A13, Th13 ;
(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . (the_arity_of o) by FUNCT_2:15
.= product ( the Sorts of A * (the_arity_of o)) by FINSEQ_2:def_5 ;
hence CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] by A14, A15, A16, A17, PBOOLE:def_15; ::_thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) ;
take CHARACT ; ::_thesis: for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
CHARACT . g = the_action_of (g,A)
let g be Gate of (X -CircuitStr); ::_thesis: ( g in the carrier' of (X -CircuitStr) implies CHARACT . g = the_action_of (g,A) )
assume g in the carrier' of (X -CircuitStr) ; ::_thesis: CHARACT . g = the_action_of (g,A)
then ex h being Gate of (X -CircuitStr) st
( h = g & CHARACT . g = the_action_of (h,A) ) by A5;
hence CHARACT . g = the_action_of (g,A) ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def_5_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra over S
for b5 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) holds
( b5 = X -CircuitCharact A iff for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b5 . g = the_action_of (g,A) );
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let A be non-empty MSAlgebra over S;
funcX -Circuit A -> strict non-empty MSAlgebra over X -CircuitStr equals :: CIRCTRM1:def 6
MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);
correctness
coherence
MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #) is strict non-empty MSAlgebra over X -CircuitStr ;
by MSUALG_1:def_3;
end;
:: deftheorem defines -Circuit CIRCTRM1:def_6_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra over S holds X -Circuit A = MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);
theorem :: CIRCTRM1:14
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being non empty Subset of (S -Terms V)
for v being Vertex of (X -CircuitStr) holds the Sorts of (X -Circuit A) . v = the_sort_of (v,A) by Def4;
theorem :: CIRCTRM1:15
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr) holds Den (g,(X -Circuit A)) = the_action_of (g,A) by Def5;
theorem Th16: :: CIRCTRM1:16
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let X be SetWithCompoundTerm of S,V; ::_thesis: for g being OperSymbol of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let g be OperSymbol of (X -CircuitStr); ::_thesis: for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
Den (g,(X -Circuit A)) = Den (o,A)
let o be OperSymbol of S; ::_thesis: ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) )
Den (g,(X -Circuit A)) = the_action_of (g,A) by Def5
.= the Charact of A . ((g . {}) `1) by Def3 ;
hence ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) ) by MCART_1:7; ::_thesis: verum
end;
theorem Th17: :: CIRCTRM1:17
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding
let t be non empty Subset of (S -Terms V); ::_thesis: t -Circuit A is finite-yielding
let i be set ; :: according to MSAFREE2:def_11,FINSET_1:def_5 ::_thesis: ( not i in the carrier of (t -CircuitStr) or the Sorts of (t -Circuit A) . i is finite )
assume i in the carrier of (t -CircuitStr) ; ::_thesis: the Sorts of (t -Circuit A) . i is finite
then reconsider i = i as Vertex of (t -CircuitStr) ;
reconsider u = i as Term of S,V by Th4;
A1: the Sorts of A is V29() by MSAFREE2:def_11;
the Sorts of (t -Circuit A) . i = the_sort_of (i,A) by Def4
.= the Sorts of A . (the_sort_of u) by Def2 ;
hence the Sorts of (t -Circuit A) . i is finite by A1; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
let A be non-empty finite-yielding MSAlgebra over S;
clusterX -Circuit A -> strict non-empty finite-yielding ;
coherence
X -Circuit A is finite-yielding by Th17;
end;
theorem Th18: :: CIRCTRM1:18
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let X1, X2 be SetWithCompoundTerm of S,V; ::_thesis: for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let A be non-empty MSAlgebra over S; ::_thesis: X1 -Circuit A tolerates X2 -Circuit A
thus ( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) ) by Th6; :: according to CIRCCOMB:def_1,CIRCCOMB:def_3 ::_thesis: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) )
thus the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) ::_thesis: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A)
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Sorts of (X1 -Circuit A)) /\ (proj1 the Sorts of (X2 -Circuit A)) or the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x )
assume A1: x in (dom the Sorts of (X1 -Circuit A)) /\ (dom the Sorts of (X2 -Circuit A)) ; ::_thesis: the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x
then A2: x in dom the Sorts of (X1 -Circuit A) by XBOOLE_0:def_4;
A3: x in dom the Sorts of (X2 -Circuit A) by A1, XBOOLE_0:def_4;
A4: x in the carrier of (X1 -CircuitStr) by A2, PARTFUN1:def_2;
reconsider v1 = x as Vertex of (X1 -CircuitStr) by A2, PARTFUN1:def_2;
reconsider v2 = x as Vertex of (X2 -CircuitStr) by A3, PARTFUN1:def_2;
reconsider t = x as Term of S,V by A4, Th4;
thus the Sorts of (X1 -Circuit A) . x = the_sort_of (v1,A) by Def4
.= the Sorts of A . (the_sort_of t) by Def2
.= the_sort_of (v2,A) by Def2
.= the Sorts of (X2 -Circuit A) . x by Def4 ; ::_thesis: verum
end;
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Charact of (X1 -Circuit A)) /\ (proj1 the Charact of (X2 -Circuit A)) or the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x )
assume A5: x in (dom the Charact of (X1 -Circuit A)) /\ (dom the Charact of (X2 -Circuit A)) ; ::_thesis: the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x
then A6: x in dom the Charact of (X1 -Circuit A) by XBOOLE_0:def_4;
A7: x in dom the Charact of (X2 -Circuit A) by A5, XBOOLE_0:def_4;
reconsider g1 = x as Gate of (X1 -CircuitStr) by A6, PARTFUN1:def_2;
reconsider g2 = x as Gate of (X2 -CircuitStr) by A7, PARTFUN1:def_2;
thus the Charact of (X1 -Circuit A) . x = the_action_of (g1,A) by Def5
.= the Charact of A . ((g1 . {}) `1) by Def3
.= the_action_of (g2,A) by Def3
.= the Charact of (X2 -Circuit A) . x by Def5 ; ::_thesis: verum
end;
theorem :: CIRCTRM1:19
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let X1, X2 be SetWithCompoundTerm of S,V; ::_thesis: for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
consider t1 being CompoundTerm of S,V such that
A1: t1 in X1 by MSATERM:def_7;
t1 in X1 \/ X2 by A1, XBOOLE_0:def_3;
then reconsider X = X1 \/ X2 as SetWithCompoundTerm of S,V by MSATERM:def_7;
let A be non-empty MSAlgebra over S; ::_thesis: (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
set C1 = X1 -Circuit A;
set C2 = X2 -Circuit A;
set C = X -Circuit A;
A2: X1 -Circuit A tolerates X2 -Circuit A by Th18;
then A3: the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) by CIRCCOMB:def_3;
A4: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) by A2, CIRCCOMB:def_3;
A5: the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X1 -Circuit A) +* the Sorts of (X2 -Circuit A) by A3, CIRCCOMB:def_4;
A6: the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X1 -Circuit A) +* the Charact of (X2 -Circuit A) by A3, CIRCCOMB:def_4;
A7: X -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) by Th10;
A8: X1 -Circuit A tolerates X -Circuit A by Th18;
A9: X2 -Circuit A tolerates X -Circuit A by Th18;
A10: the Sorts of (X1 -Circuit A) tolerates the Sorts of (X -Circuit A) by A8, CIRCCOMB:def_3;
A11: the Sorts of (X2 -Circuit A) tolerates the Sorts of (X -Circuit A) by A9, CIRCCOMB:def_3;
A12: the Charact of (X1 -Circuit A) tolerates the Charact of (X -Circuit A) by A8, CIRCCOMB:def_3;
A13: the Charact of (X2 -Circuit A) tolerates the Charact of (X -Circuit A) by A9, CIRCCOMB:def_3;
A14: dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier of (X -CircuitStr) by A7, PARTFUN1:def_2;
dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier' of (X -CircuitStr) by A7, PARTFUN1:def_2;
then A15: dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Charact of (X -Circuit A) by PARTFUN1:def_2;
A16: dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Sorts of (X -Circuit A) by A14, PARTFUN1:def_2;
A17: the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X -Circuit A) by A4, A6, A12, A13, A15, FUNCT_4:125, PARTFUN1:55;
the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X -Circuit A) by A3, A5, A10, A11, A16, FUNCT_4:125, PARTFUN1:55;
hence (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A) by A17; ::_thesis: verum
end;
begin
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be Variables of A;
let t be DecoratedTree;
assume A1: t is Term of S,V ;
let f be ManySortedFunction of V, the Sorts of A;
funct @ (f,A) -> set means :Def7: :: CIRCTRM1:def 7
ex t9 being c-Term of A,V st
( t9 = t & it = t9 @ f );
correctness
existence
ex b1 being set ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f );
uniqueness
for b1, b2 being set st ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f ) & ex t9 being c-Term of A,V st
( t9 = t & b2 = t9 @ f ) holds
b1 = b2;
proof
reconsider t9 = t as c-Term of A,V by A1, MSATERM:27;
t9 @ f = t9 @ f ;
hence ( ex b1 being set ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f ) & ( for b1, b2 being set st ex t9 being c-Term of A,V st
( t9 = t & b1 = t9 @ f ) & ex t9 being c-Term of A,V st
( t9 = t & b2 = t9 @ f ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines @ CIRCTRM1:def_7_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being DecoratedTree st t is Term of S,V holds
for f being ManySortedFunction of V, the Sorts of A
for b6 being set holds
( b6 = t @ (f,A) iff ex t9 being c-Term of A,V st
( t9 = t & b6 = t9 @ f ) );
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
let A be non-empty finite-yielding MSAlgebra over S;
let s be State of (X -Circuit A);
defpred S1[ set , set , set ] means ( root-tree [$2,$1] in Subtrees X implies $3 = s . (root-tree [$2,$1]) );
A1: for x being Vertex of S
for v being Element of V . x ex a being Element of the Sorts of A . x st S1[x,v,a]
proof
let x be Vertex of S; ::_thesis: for v being Element of V . x ex a being Element of the Sorts of A . x st S1[x,v,a]
let v be Element of V . x; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a]
percases ( not root-tree [v,x] in Subtrees X or root-tree [v,x] in Subtrees X ) ;
suppose not root-tree [v,x] in Subtrees X ; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a]
hence ex a being Element of the Sorts of A . x st S1[x,v,a] ; ::_thesis: verum
end;
suppose root-tree [v,x] in Subtrees X ; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a]
then reconsider a = root-tree [v,x] as Vertex of (X -CircuitStr) ;
reconsider t = a as Term of S,V by MSATERM:4;
A2: the_sort_of t = x by MSATERM:14;
A3: the_sort_of (a,A) = the Sorts of A . (the_sort_of t) by Def2;
(X -CircuitSorts A) . a = the_sort_of (a,A) by Def4;
then reconsider b = s . a as Element of the Sorts of A . x by A2, A3, CIRCUIT1:4;
take b ; ::_thesis: S1[x,v,b]
thus S1[x,v,b] ; ::_thesis: verum
end;
end;
end;
mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A means :Def8: :: CIRCTRM1:def 8
for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(it . x) . v = s . (root-tree [v,x]);
existence
ex b1 being ManySortedFunction of V, the Sorts of A st
for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b1 . x) . v = s . (root-tree [v,x])
proof
thus ex f being ManySortedFunction of V, the Sorts of A st
for x being Element of S
for v being Element of V . x holds S1[x,v,(f . x) . v] from CIRCTRM1:sch_1(A1); ::_thesis: verum
end;
end;
:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def_8_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for A being non-empty finite-yielding MSAlgebra over S
for s being State of (X -Circuit A)
for b6 being ManySortedFunction of V, the Sorts of A holds
( b6 is CompatibleValuation of s iff for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b6 . x) . v = s . (root-tree [v,x]) );
theorem :: CIRCTRM1:20
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let X be SetWithCompoundTerm of S,V; ::_thesis: for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let s be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let f be CompatibleValuation of s; ::_thesis: for n being Element of NAT holds f is CompatibleValuation of Following (s,n)
let n be Element of NAT ; ::_thesis: f is CompatibleValuation of Following (s,n)
let x be Vertex of S; :: according to CIRCTRM1:def_8 ::_thesis: for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(f . x) . v = (Following (s,n)) . (root-tree [v,x])
let v be Element of V . x; ::_thesis: ( root-tree [v,x] in Subtrees X implies (f . x) . v = (Following (s,n)) . (root-tree [v,x]) )
assume A1: root-tree [v,x] in Subtrees X ; ::_thesis: (f . x) . v = (Following (s,n)) . (root-tree [v,x])
then root-tree [v,x] in InputVertices (X -CircuitStr) by Th11;
then s is_stable_at root-tree [v,x] by FACIRC_1:18;
then (Following (s,n)) . (root-tree [v,x]) = s . (root-tree [v,x]) by FACIRC_1:def_9;
hence (f . x) . v = (Following (s,n)) . (root-tree [v,x]) by A1, Def8; ::_thesis: verum
end;
registration
let x be set ;
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let p be FinSequence of S -Terms V;
clusterx -tree p -> finite ;
coherence
x -tree p is finite
proof
reconsider q = doms p as FinTree-yielding FinSequence ;
dom (x -tree p) = tree q by TREES_4:10;
hence x -tree p is finite by FINSET_1:10; ::_thesis: verum
end;
end;
theorem Th21: :: CIRCTRM1:21
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at t & (Following (s,(1 + (height (dom t))))) . t = t @ (f,A) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at t & (Following (s,(1 + (height (dom t))))) . t = t @ (f,A) )
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at t & (Following (s,(1 + (height (dom t))))) . t = t @ (f,A) )
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at t & (Following (s,(1 + (height (dom t))))) . t = t @ (f,A) )
let X be SetWithCompoundTerm of S,V; ::_thesis: for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at t & (Following (s,(1 + (height (dom t))))) . t = t @ (f,A) )
let q be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of q
for t being Term of S,V st t in Subtrees X holds
( Following (q,(1 + (height (dom t)))) is_stable_at t & (Following (q,(1 + (height (dom t))))) . t = t @ (f,A) )
let f be CompatibleValuation of q; ::_thesis: for t being Term of S,V st t in Subtrees X holds
( Following (q,(1 + (height (dom t)))) is_stable_at t & (Following (q,(1 + (height (dom t))))) . t = t @ (f,A) )
A1: X -CircuitStr = ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #) ;
defpred S1[ finite DecoratedTree] means ( $1 in Subtrees X implies ( Following (q,(1 + (height (dom $1)))) is_stable_at $1 & (Following (q,(1 + (height (dom $1))))) . $1 = $1 @ (f,A) ) );
A2: for s being SortSymbol of S
for v being Element of V . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]]
let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]]
assume A3: root-tree [v,s] in Subtrees X ; ::_thesis: ( Following (q,(1 + (height (dom (root-tree [v,s]))))) is_stable_at root-tree [v,s] & (Following (q,(1 + (height (dom (root-tree [v,s])))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) )
then A4: root-tree [v,s] in InputVertices (X -CircuitStr) by Th11;
hence Following (q,(1 + (height (dom (root-tree [v,s]))))) is_stable_at root-tree [v,s] by FACIRC_1:18; ::_thesis: (Following (q,(1 + (height (dom (root-tree [v,s])))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A)
reconsider t = root-tree [v,s] as c-Term of A,V by MSATERM:8;
A5: t is Term of S,V by MSATERM:4;
q is_stable_at root-tree [v,s] by A4, FACIRC_1:18;
hence (Following (q,(1 + (height (dom (root-tree [v,s])))))) . (root-tree [v,s]) = q . (root-tree [v,s]) by FACIRC_1:def_9
.= (f . s) . v by A3, Def8
.= (v -term A) @ f by MSATERM:42
.= t @ f by MSATERM:def_4
.= (root-tree [v,s]) @ (f,A) by A5, Def7 ;
::_thesis: verum
end;
A6: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t being Term of S,V st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume that
A7: for t being Term of S,V st t in rng p & t in Subtrees X holds
( Following (q,(1 + (height (dom t)))) is_stable_at t & (Following (q,(1 + (height (dom t))))) . t = t @ (f,A) ) and
A8: [o, the carrier of S] -tree p in Subtrees X ; ::_thesis: ( Following (q,(1 + (height (dom ([o, the carrier of S] -tree p))))) is_stable_at [o, the carrier of S] -tree p & (Following (q,(1 + (height (dom ([o, the carrier of S] -tree p)))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) )
consider tt being Element of X, n being Node of tt such that
A9: [o, the carrier of S] -tree p = tt | n by A8, TREES_9:19;
A10: <*> NAT in (dom tt) | n by TREES_1:22;
n ^ {} = n by FINSEQ_1:34;
then tt . n = (tt | n) . {} by A10, TREES_2:def_10
.= [o, the carrier of S] by A9, TREES_4:def_4 ;
then tt . n in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:106;
then reconsider g = [o, the carrier of S] -tree p as Gate of (X -CircuitStr) by A9, TREES_9:24;
A11: the_result_sort_of g = g by FUNCT_1:17;
A12: g . {} = [o, the carrier of S] by TREES_4:def_4;
g = (g . {}) -tree (the_arity_of g) by Th12;
then A13: the_arity_of g = p by TREES_4:15;
A14: rng (the_arity_of g) c= Subtrees X by FINSEQ_1:def_4;
A15: dom ([o, the carrier of S] -tree p) = tree (doms p) by TREES_4:10;
now__::_thesis:_for_x_being_set_st_x_in_rng_(the_arity_of_g)_holds_
Following_(q,(height_(dom_([o,_the_carrier_of_S]_-tree_p))))_is_stable_at_x
let x be set ; ::_thesis: ( x in rng (the_arity_of g) implies Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at x )
assume A16: x in rng (the_arity_of g) ; ::_thesis: Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at x
then reconsider t = x as Element of Subtrees X by A14;
reconsider t = t as Term of S,V by A1, Th4;
consider z being set such that
A17: z in dom p and
A18: t = p . z by A13, A16, FUNCT_1:def_3;
A19: z in dom (doms p) by A17, A18, FUNCT_6:22;
(doms p) . z = dom t by A17, A18, FUNCT_6:22;
then dom t in rng (doms p) by A19, FUNCT_1:def_3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then 1 + (height (dom t)) <= height (tree (doms p)) by NAT_1:13;
then consider i being Nat such that
A20: height (tree (doms p)) = (1 + (height (dom t))) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
Following (q,(height (dom ([o, the carrier of S] -tree p)))) = Following ((Following (q,(1 + (height (dom t))))),i) by A15, A20, FACIRC_1:13;
hence Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at x by A7, A13, A16, FACIRC_1:17; ::_thesis: verum
end;
then Following (Following (q,(height (dom ([o, the carrier of S] -tree p))))) is_stable_at [o, the carrier of S] -tree p by A11, FACIRC_1:19;
hence Following (q,(1 + (height (dom ([o, the carrier of S] -tree p))))) is_stable_at [o, the carrier of S] -tree p by FACIRC_1:12; ::_thesis: (Following (q,(1 + (height (dom ([o, the carrier of S] -tree p)))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A)
reconsider t = (Sym (o,V)) -tree p as c-Term of A,V by MSATERM:27;
A21: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9;
A22: Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9;
A23: t = [o, the carrier of S] -tree p by MSAFREE:def_9;
deffunc H1( set ) -> set = (Following (q,(height (dom t)))) . (p . $1);
consider vp being FinSequence such that
A24: len vp = len p and
A25: for i being Nat st i in dom vp holds
vp . i = H1(i) from FINSEQ_1:sch_2();
A26: dom vp = Seg (len p) by A24, FINSEQ_1:def_3;
A27: dom p = Seg (len p) by FINSEQ_1:def_3;
A28: dom p = dom (the_arity_of o) by MSATERM:22;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
ex_t9_being_c-Term_of_A,V_st_
(_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_)
let i be Nat; ::_thesis: ( i in dom p implies ex t9 being c-Term of A,V st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) )
assume A29: i in dom p ; ::_thesis: ex t9 being c-Term of A,V st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,V by MSATERM:22;
reconsider t9 = t as c-Term of A,V by MSATERM:27;
take t9 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
the_sort_of t = the_sort_of t9 by Th1;
hence ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) by A29, MSATERM:23; ::_thesis: verum
end;
then reconsider p9 = p as ArgumentSeq of o,A,V by A28, MSATERM:24;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
for_t_being_c-Term_of_A,V_st_t_=_p_._i_holds_
vp_._i_=_t_@_f
let i be Nat; ::_thesis: ( i in dom p implies for t being c-Term of A,V st t = p . i holds
vp . i = t @ f )
assume A30: i in dom p ; ::_thesis: for t being c-Term of A,V st t = p . i holds
vp . i = t @ f
let t be c-Term of A,V; ::_thesis: ( t = p . i implies vp . i = t @ f )
assume A31: t = p . i ; ::_thesis: vp . i = t @ f
then A32: t in rng p by A30, FUNCT_1:def_3;
then reconsider tt = t as Element of Subtrees X by A13, A14;
reconsider tt = tt as Term of S,V by A1, Th4;
A33: Following (q,(1 + (height (dom t)))) is_stable_at tt by A7, A32;
A34: (Following (q,(1 + (height (dom t))))) . tt = tt @ (f,A) by A7, A32;
A35: vp . i = (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . t by A23, A25, A26, A27, A30, A31;
A36: i in dom (doms p) by A30, A31, FUNCT_6:22;
(doms p) . i = dom t by A30, A31, FUNCT_6:22;
then dom t in rng (doms p) by A36, FUNCT_1:def_3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then 1 + (height (dom t)) <= height (tree (doms p)) by NAT_1:13;
then consider j being Nat such that
A37: height (tree (doms p)) = (1 + (height (dom t))) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
Following (q,(height (dom ([o, the carrier of S] -tree p)))) = Following ((Following (q,(1 + (height (dom t))))),j) by A15, A37, FACIRC_1:13;
then (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . t = (Following (q,(1 + (height (dom t))))) . t by A33, FACIRC_1:def_9;
hence vp . i = t @ f by A34, A35, Def7; ::_thesis: verum
end;
then A38: ((Sym (o,( the Sorts of A \/ V))) -tree p9) @ f = (Den (o,A)) . vp by A24, MSATERM:43;
now__::_thesis:_(_dom_((Following_(q,(height_(dom_t))))_*_p)_=_dom_p_&_(_for_z_being_set_st_z_in_Seg_(len_p)_holds_
vp_._z_=_((Following_(q,(height_(dom_t))))_*_p)_._z_)_)
A39: rng p c= the carrier of (X -CircuitStr) by A13, FINSEQ_1:def_4;
dom (Following (q,(height (dom t)))) = the carrier of (X -CircuitStr) by CIRCUIT1:3;
hence dom ((Following (q,(height (dom t)))) * p) = dom p by A39, RELAT_1:27; ::_thesis: for z being set st z in Seg (len p) holds
vp . z = ((Following (q,(height (dom t)))) * p) . z
let z be set ; ::_thesis: ( z in Seg (len p) implies vp . z = ((Following (q,(height (dom t)))) * p) . z )
assume A40: z in Seg (len p) ; ::_thesis: vp . z = ((Following (q,(height (dom t)))) * p) . z
then reconsider i = z as Element of NAT ;
vp . i = (Following (q,(height (dom t)))) . (p . i) by A25, A26, A40;
hence vp . z = ((Following (q,(height (dom t)))) * p) . z by A27, A40, FUNCT_1:13; ::_thesis: verum
end;
then A41: vp = (Following (q,(height (dom t)))) * (the_arity_of g) by A13, A26, A27, FUNCT_1:2;
Den (g,(X -Circuit A)) = Den (o,A) by A12, Th16;
then (Den (o,A)) . vp = (Following (Following (q,(height (dom t))))) . t by A11, A23, A41, FACIRC_1:10;
hence (Following (q,(1 + (height (dom ([o, the carrier of S] -tree p)))))) . ([o, the carrier of S] -tree p) = t @ f by A21, A22, A38, FACIRC_1:12
.= ([o, the carrier of S] -tree p) @ (f,A) by A22, Def7 ;
::_thesis: verum
end;
thus for t being Term of S,V holds S1[t] from MSATERM:sch_1(A2, A6); ::_thesis: verum
end;
theorem :: CIRCTRM1:22
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )
let X be SetWithCompoundTerm of S,V; ::_thesis: ( ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) implies for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) ) )
assume A1: for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ; ::_thesis: for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )
let q be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of q
for t being Term of S,V st t in Subtrees X holds
( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) )
let f be CompatibleValuation of q; ::_thesis: for t being Term of S,V st t in Subtrees X holds
( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) )
A2: X -CircuitStr = ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #) ;
defpred S1[ finite DecoratedTree] means ( $1 in Subtrees X implies ( Following (q,(height (dom $1))) is_stable_at $1 & (Following (q,(height (dom $1)))) . $1 = $1 @ (f,A) ) );
A3: for s being SortSymbol of S
for v being Element of V . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]]
let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]]
assume A4: root-tree [v,s] in Subtrees X ; ::_thesis: ( Following (q,(height (dom (root-tree [v,s])))) is_stable_at root-tree [v,s] & (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) )
then root-tree [v,s] in InputVertices (X -CircuitStr) by Th11;
hence Following (q,(height (dom (root-tree [v,s])))) is_stable_at root-tree [v,s] by FACIRC_1:18; ::_thesis: (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A)
reconsider t = root-tree [v,s] as c-Term of A,V by MSATERM:8;
A5: t is Term of S,V by MSATERM:4;
dom (root-tree [v,s]) = elementary_tree 0 by TREES_4:3;
hence (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = q . (root-tree [v,s]) by FACIRC_1:11, TREES_1:42
.= (f . s) . v by A4, Def8
.= (v -term A) @ f by MSATERM:42
.= t @ f by MSATERM:def_4
.= (root-tree [v,s]) @ (f,A) by A5, Def7 ;
::_thesis: verum
end;
A6: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t being Term of S,V st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume that
A7: for t being Term of S,V st t in rng p & t in Subtrees X holds
( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) ) and
A8: [o, the carrier of S] -tree p in Subtrees X ; ::_thesis: ( Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at [o, the carrier of S] -tree p & (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) )
consider tt being Element of X, n being Node of tt such that
A9: [o, the carrier of S] -tree p = tt | n by A8, TREES_9:19;
A10: <*> NAT in (dom tt) | n by TREES_1:22;
n ^ {} = n by FINSEQ_1:34;
then tt . n = (tt | n) . {} by A10, TREES_2:def_10
.= [o, the carrier of S] by A9, TREES_4:def_4 ;
then tt . n in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:106;
then reconsider g = [o, the carrier of S] -tree p as Gate of (X -CircuitStr) by A9, TREES_9:24;
A11: the_result_sort_of g = g by FUNCT_1:17;
A12: g . {} = [o, the carrier of S] by TREES_4:def_4;
g = (g . {}) -tree (the_arity_of g) by Th12;
then A13: the_arity_of g = p by TREES_4:15;
A14: rng (the_arity_of g) c= Subtrees X by FINSEQ_1:def_4;
A15: dom ([o, the carrier of S] -tree p) = tree (doms p) by TREES_4:10;
now__::_thesis:_not_height_(dom_([o,_the_carrier_of_S]_-tree_p))_=_0
assume height (dom ([o, the carrier of S] -tree p)) = 0 ; ::_thesis: contradiction
then [o, the carrier of S] -tree p = root-tree [o, the carrier of S] by A12, TREES_1:43, TREES_4:5;
then p = {} by TREES_4:17;
then len p = 0 ;
then len (the_arity_of o) = 0 by MSATERM:22;
then A16: the_arity_of o = {} ;
g is Term of S,V by Th4;
hence contradiction by A1, A8, A12, A16; ::_thesis: verum
end;
then consider h being Nat such that
A17: height (dom ([o, the carrier of S] -tree p)) = h + 1 by NAT_1:6;
reconsider h = h as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_x_being_set_st_x_in_rng_(the_arity_of_g)_holds_
Following_(q,h)_is_stable_at_x
let x be set ; ::_thesis: ( x in rng (the_arity_of g) implies Following (q,h) is_stable_at x )
assume A18: x in rng (the_arity_of g) ; ::_thesis: Following (q,h) is_stable_at x
then reconsider t = x as Element of Subtrees X by A14;
reconsider t = t as Term of S,V by A2, Th4;
consider z being set such that
A19: z in dom p and
A20: t = p . z by A13, A18, FUNCT_1:def_3;
A21: z in dom (doms p) by A19, A20, FUNCT_6:22;
(doms p) . z = dom t by A19, A20, FUNCT_6:22;
then dom t in rng (doms p) by A21, FUNCT_1:def_3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then height (dom t) <= h by A15, A17, NAT_1:13;
then consider i being Nat such that
A22: h = (height (dom t)) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
Following (q,h) = Following ((Following (q,(height (dom t)))),i) by A22, FACIRC_1:13;
hence Following (q,h) is_stable_at x by A7, A13, A18, FACIRC_1:17; ::_thesis: verum
end;
then Following (Following (q,h)) is_stable_at [o, the carrier of S] -tree p by A11, FACIRC_1:19;
hence Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at [o, the carrier of S] -tree p by A17, FACIRC_1:12; ::_thesis: (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A)
reconsider t = (Sym (o,V)) -tree p as c-Term of A,V by MSATERM:27;
A23: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9;
A24: Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9;
A25: t = [o, the carrier of S] -tree p by MSAFREE:def_9;
deffunc H1( set ) -> set = (Following (q,h)) . (p . $1);
consider vp being FinSequence such that
A26: len vp = len p and
A27: for i being Nat st i in dom vp holds
vp . i = H1(i) from FINSEQ_1:sch_2();
A28: dom vp = Seg (len p) by A26, FINSEQ_1:def_3;
A29: dom p = Seg (len p) by FINSEQ_1:def_3;
A30: dom p = dom (the_arity_of o) by MSATERM:22;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
ex_t9_being_c-Term_of_A,V_st_
(_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_)
let i be Nat; ::_thesis: ( i in dom p implies ex t9 being c-Term of A,V st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) )
assume A31: i in dom p ; ::_thesis: ex t9 being c-Term of A,V st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,V by MSATERM:22;
reconsider t9 = t as c-Term of A,V by MSATERM:27;
take t9 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
the_sort_of t = the_sort_of t9 by Th1;
hence ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) by A31, MSATERM:23; ::_thesis: verum
end;
then reconsider p9 = p as ArgumentSeq of o,A,V by A30, MSATERM:24;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
for_t_being_c-Term_of_A,V_st_t_=_p_._i_holds_
vp_._i_=_t_@_f
let i be Nat; ::_thesis: ( i in dom p implies for t being c-Term of A,V st t = p . i holds
vp . i = t @ f )
assume A32: i in dom p ; ::_thesis: for t being c-Term of A,V st t = p . i holds
vp . i = t @ f
let t be c-Term of A,V; ::_thesis: ( t = p . i implies vp . i = t @ f )
assume A33: t = p . i ; ::_thesis: vp . i = t @ f
then A34: t in rng p by A32, FUNCT_1:def_3;
then reconsider tt = t as Element of Subtrees X by A13, A14;
reconsider tt = tt as Term of S,V by A2, Th4;
A35: Following (q,(height (dom t))) is_stable_at tt by A7, A34;
A36: (Following (q,(height (dom t)))) . tt = tt @ (f,A) by A7, A34;
A37: vp . i = (Following (q,h)) . t by A27, A28, A29, A32, A33;
A38: i in dom (doms p) by A32, A33, FUNCT_6:22;
(doms p) . i = dom t by A32, A33, FUNCT_6:22;
then dom t in rng (doms p) by A38, FUNCT_1:def_3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then height (dom t) <= h by A15, A17, NAT_1:13;
then consider j being Nat such that
A39: h = (height (dom t)) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
Following (q,h) = Following ((Following (q,(height (dom t)))),j) by A39, FACIRC_1:13;
then (Following (q,h)) . t = (Following (q,(height (dom t)))) . t by A35, FACIRC_1:def_9;
hence vp . i = t @ f by A36, A37, Def7; ::_thesis: verum
end;
then A40: ((Sym (o,( the Sorts of A \/ V))) -tree p9) @ f = (Den (o,A)) . vp by A26, MSATERM:43;
now__::_thesis:_(_dom_((Following_(q,h))_*_p)_=_dom_p_&_(_for_z_being_set_st_z_in_Seg_(len_p)_holds_
vp_._z_=_((Following_(q,h))_*_p)_._z_)_)
A41: rng p c= the carrier of (X -CircuitStr) by A13, FINSEQ_1:def_4;
dom (Following (q,h)) = the carrier of (X -CircuitStr) by CIRCUIT1:3;
hence dom ((Following (q,h)) * p) = dom p by A41, RELAT_1:27; ::_thesis: for z being set st z in Seg (len p) holds
vp . z = ((Following (q,h)) * p) . z
let z be set ; ::_thesis: ( z in Seg (len p) implies vp . z = ((Following (q,h)) * p) . z )
assume A42: z in Seg (len p) ; ::_thesis: vp . z = ((Following (q,h)) * p) . z
then reconsider i = z as Element of NAT ;
vp . i = (Following (q,h)) . (p . i) by A27, A28, A42;
hence vp . z = ((Following (q,h)) * p) . z by A29, A42, FUNCT_1:13; ::_thesis: verum
end;
then A43: vp = (Following (q,h)) * (the_arity_of g) by A13, A28, A29, FUNCT_1:2;
Den (g,(X -Circuit A)) = Den (o,A) by A12, Th16;
then (Den (o,A)) . vp = (Following (Following (q,h))) . t by A11, A25, A43, FACIRC_1:10;
hence (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = t @ f by A17, A23, A24, A40, FACIRC_1:12
.= ([o, the carrier of S] -tree p) @ (f,A) by A24, Def7 ;
::_thesis: verum
end;
thus for t being Term of S,V holds S1[t] from MSATERM:sch_1(A3, A6); ::_thesis: verum
end;
begin
definition
let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
predS1,S2 are_equivalent_wrt f,g means :Def9: :: CIRCTRM1:def 9
( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 );
end;
:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def_9_:_
for S1, S2 being non empty ManySortedSign
for f, g being Function holds
( S1,S2 are_equivalent_wrt f,g iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 ) );
theorem Th23: :: CIRCTRM1:23
for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 )
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 )
let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 ) )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f,g form_morphism_between S1,S2 and
A4: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_9 ::_thesis: ( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 )
thus the carrier of S2 = dom (f ") by A4, PUA2MSS1:def_12
.= rng f by A1, FUNCT_1:33
.= f .: (dom f) by RELAT_1:113
.= f .: the carrier of S1 by A3, PUA2MSS1:def_12 ; ::_thesis: the carrier' of S2 = g .: the carrier' of S1
thus the carrier' of S2 = dom (g ") by A4, PUA2MSS1:def_12
.= rng g by A2, FUNCT_1:33
.= g .: (dom g) by RELAT_1:113
.= g .: the carrier' of S1 by A3, PUA2MSS1:def_12 ; ::_thesis: verum
end;
theorem Th24: :: CIRCTRM1:24
for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( rng f = the carrier of S2 & rng g = the carrier' of S2 )
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( rng f = the carrier of S2 & rng g = the carrier' of S2 )
let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( rng f = the carrier of S2 & rng g = the carrier' of S2 ) )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
f,g form_morphism_between S1,S2 and
A3: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_9 ::_thesis: ( rng f = the carrier of S2 & rng g = the carrier' of S2 )
thus rng f = dom (f ") by A1, FUNCT_1:33
.= the carrier of S2 by A3, PUA2MSS1:def_12 ; ::_thesis: rng g = the carrier' of S2
thus rng g = dom (g ") by A2, FUNCT_1:33
.= the carrier' of S2 by A3, PUA2MSS1:def_12 ; ::_thesis: verum
end;
theorem Th25: :: CIRCTRM1:25
for S being non empty ManySortedSign holds S,S are_equivalent_wrt id the carrier of S, id the carrier' of S
proof
let S be non empty ManySortedSign ; ::_thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S
set f = id the carrier of S;
set g = id the carrier' of S;
thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def_9 ::_thesis: ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S )
A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:45;
(id the carrier' of S) " = id the carrier' of S by FUNCT_1:45;
hence ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S ) by A1, INSTALG1:8; ::_thesis: verum
end;
theorem Th26: :: CIRCTRM1:26
for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
S2,S1 are_equivalent_wrt f " ,g "
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
S2,S1 are_equivalent_wrt f " ,g "
let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies S2,S1 are_equivalent_wrt f " ,g " )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f,g form_morphism_between S1,S2 and
A4: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_9 ::_thesis: S2,S1 are_equivalent_wrt f " ,g "
thus ( f " is one-to-one & g " is one-to-one ) by A1, A2; :: according to CIRCTRM1:def_9 ::_thesis: ( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 )
(f ") " = f by A1, FUNCT_1:43;
hence ( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 ) by A2, A3, A4, FUNCT_1:43; ::_thesis: verum
end;
theorem Th27: :: CIRCTRM1:27
for S1, S2, S3 being non empty ManySortedSign
for f1, g1, f2, g2 being Function st S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 holds
S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for f1, g1, f2, g2 being Function st S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 holds
S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
let f1, g1, f2, g2 be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 implies S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 )
assume that
A1: f1 is one-to-one and
A2: g1 is one-to-one and
A3: f1,g1 form_morphism_between S1,S2 and
A4: f1 " ,g1 " form_morphism_between S2,S1 and
A5: f2 is one-to-one and
A6: g2 is one-to-one and
A7: f2,g2 form_morphism_between S2,S3 and
A8: f2 " ,g2 " form_morphism_between S3,S2 ; :: according to CIRCTRM1:def_9 ::_thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A2, A5, A6; :: according to CIRCTRM1:def_9 ::_thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 )
A9: (f2 * f1) " = (f1 ") * (f2 ") by A1, A5, FUNCT_1:44;
(g2 * g1) " = (g1 ") * (g2 ") by A2, A6, FUNCT_1:44;
hence ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 ) by A3, A4, A7, A8, A9, PUA2MSS1:29; ::_thesis: verum
end;
theorem Th28: :: CIRCTRM1:28
for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )
let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 ) )
assume A1: S1,S2 are_equivalent_wrt f,g ; ::_thesis: ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 )
A2: f is one-to-one by A1, Def9;
A3: f,g form_morphism_between S1,S2 by A1, Def9;
A4: rng g = the carrier' of S2 by A1, Th24;
A5: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def_1;
A6: f .: (rng the ResultSort of S1) = rng (f * the ResultSort of S1) by RELAT_1:127
.= rng ( the ResultSort of S2 * g) by A3, PUA2MSS1:def_12
.= rng the ResultSort of S2 by A4, A5, RELAT_1:28 ;
thus f .: (InputVertices S1) = (f .: the carrier of S1) \ (f .: (rng the ResultSort of S1)) by A2, FUNCT_1:64
.= InputVertices S2 by A1, A6, Th23 ; ::_thesis: f .: (InnerVertices S1) = InnerVertices S2
thus f .: (InnerVertices S1) = InnerVertices S2 by A6; ::_thesis: verum
end;
definition
let S1, S2 be non empty ManySortedSign ;
predS1,S2 are_equivalent means :: CIRCTRM1:def 10
ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g;
reflexivity
for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g
proof
let S be non empty ManySortedSign ; ::_thesis: ex f, g being one-to-one Function st S,S are_equivalent_wrt f,g
take id the carrier of S ; ::_thesis: ex g being one-to-one Function st S,S are_equivalent_wrt id the carrier of S,g
take id the carrier' of S ; ::_thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S
thus S,S are_equivalent_wrt id the carrier of S, id the carrier' of S by Th25; ::_thesis: verum
end;
symmetry
for S1, S2 being non empty ManySortedSign st ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g holds
ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g implies ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g )
given f, g being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f,g ; ::_thesis: ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g
take f " ; ::_thesis: ex g being one-to-one Function st S2,S1 are_equivalent_wrt f " ,g
take g " ; ::_thesis: S2,S1 are_equivalent_wrt f " ,g "
thus S2,S1 are_equivalent_wrt f " ,g " by A1, Th26; ::_thesis: verum
end;
end;
:: deftheorem defines are_equivalent CIRCTRM1:def_10_:_
for S1, S2 being non empty ManySortedSign holds
( S1,S2 are_equivalent iff ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g );
theorem :: CIRCTRM1:29
for S1, S2, S3 being non empty ManySortedSign st S1,S2 are_equivalent & S2,S3 are_equivalent holds
S1,S3 are_equivalent
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: ( S1,S2 are_equivalent & S2,S3 are_equivalent implies S1,S3 are_equivalent )
given f1, g1 being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f1,g1 ; :: according to CIRCTRM1:def_10 ::_thesis: ( not S2,S3 are_equivalent or S1,S3 are_equivalent )
given f2, g2 being one-to-one Function such that A2: S2,S3 are_equivalent_wrt f2,g2 ; :: according to CIRCTRM1:def_10 ::_thesis: S1,S3 are_equivalent
take f2 * f1 ; :: according to CIRCTRM1:def_10 ::_thesis: ex g being one-to-one Function st S1,S3 are_equivalent_wrt f2 * f1,g
take g2 * g1 ; ::_thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
thus S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 by A1, A2, Th27; ::_thesis: verum
end;
definition
let S1, S2 be non empty ManySortedSign ;
let f be Function;
predf preserves_inputs_of S1,S2 means :: CIRCTRM1:def 11
f .: (InputVertices S1) c= InputVertices S2;
end;
:: deftheorem defines preserves_inputs_of CIRCTRM1:def_11_:_
for S1, S2 being non empty ManySortedSign
for f being Function holds
( f preserves_inputs_of S1,S2 iff f .: (InputVertices S1) c= InputVertices S2 );
theorem Th30: :: CIRCTRM1:30
for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Vertex of S1 holds f . v is Vertex of S2
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Vertex of S1 holds f . v is Vertex of S2
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v being Vertex of S1 holds f . v is Vertex of S2 )
assume that
A1: dom f = the carrier of S1 and
dom g = the carrier' of S1 and
A2: rng f c= the carrier of S2 ; :: according to PUA2MSS1:def_12 ::_thesis: ( not proj2 g c= the carrier' of S2 or not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Vertex of S1 holds f . v is Vertex of S2 )
now__::_thesis:_for_v_being_Vertex_of_S1_holds_f_._v_in_the_carrier_of_S2
let v be Vertex of S1; ::_thesis: f . v in the carrier of S2
f . v in rng f by A1, FUNCT_1:def_3;
hence f . v in the carrier of S2 by A2; ::_thesis: verum
end;
hence ( not proj2 g c= the carrier' of S2 or not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Vertex of S1 holds f . v is Vertex of S2 ) ; ::_thesis: verum
end;
theorem Th31: :: CIRCTRM1:31
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Gate of S1 holds g . v is Gate of S2
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Gate of S1 holds g . v is Gate of S2
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v being Gate of S1 holds g . v is Gate of S2 )
assume that
dom f = the carrier of S1 and
A1: dom g = the carrier' of S1 and
rng f c= the carrier of S2 and
A2: rng g c= the carrier' of S2 ; :: according to PUA2MSS1:def_12 ::_thesis: ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Gate of S1 holds g . v is Gate of S2 )
now__::_thesis:_for_v_being_Gate_of_S1_holds_g_._v_in_the_carrier'_of_S2
let v be Gate of S1; ::_thesis: g . v in the carrier' of S2
g . v in rng g by A1, FUNCT_1:def_3;
hence g . v in the carrier' of S2 by A2; ::_thesis: verum
end;
hence ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Gate of S1 holds g . v is Gate of S2 ) ; ::_thesis: verum
end;
theorem Th32: :: CIRCTRM1:32
for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
f .: (InnerVertices S1) c= InnerVertices S2
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
f .: (InnerVertices S1) c= InnerVertices S2
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies f .: (InnerVertices S1) c= InnerVertices S2 )
assume f,g form_morphism_between S1,S2 ; ::_thesis: f .: (InnerVertices S1) c= InnerVertices S2
then f * the ResultSort of S1 = the ResultSort of S2 * g by PUA2MSS1:def_12;
then f .: (InnerVertices S1) = rng ( the ResultSort of S2 * g) by RELAT_1:127;
hence f .: (InnerVertices S1) c= InnerVertices S2 by RELAT_1:26; ::_thesis: verum
end;
theorem Th33: :: CIRCTRM1:33
for S1, S2 being non empty non void Circuit-like ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
proof
let S1, S2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let v1 be Vertex of S1; ::_thesis: ( v1 in InnerVertices S1 implies for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1) )
assume A2: v1 in InnerVertices S1 ; ::_thesis: for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let v2 be Vertex of S2; ::_thesis: ( v2 = f . v1 implies action_at v2 = g . (action_at v1) )
assume A3: v2 = f . v1 ; ::_thesis: action_at v2 = g . (action_at v1)
reconsider g1 = g . (action_at v1) as Gate of S2 by A1, Th31;
A4: dom g = the carrier' of S1 by A1, PUA2MSS1:def_12;
A5: dom f = the carrier of S1 by A1, PUA2MSS1:def_12;
A6: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def_1;
A7: f .: (InnerVertices S1) c= InnerVertices S2 by A1, Th32;
A8: v2 in f .: (InnerVertices S1) by A2, A3, A5, FUNCT_1:def_6;
the_result_sort_of g1 = ( the ResultSort of S2 * g) . (action_at v1) by A4, FUNCT_1:13
.= (f * the ResultSort of S1) . (action_at v1) by A1, PUA2MSS1:def_12
.= f . (the_result_sort_of (action_at v1)) by A6, FUNCT_1:13
.= v2 by A2, A3, MSAFREE2:def_7 ;
hence action_at v2 = g . (action_at v1) by A7, A8, MSAFREE2:def_7; ::_thesis: verum
end;
definition
let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
predf,g form_embedding_of C1,C2 means :Def12: :: CIRCTRM1:def 12
( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g );
end;
:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def_12_:_
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( f,g form_embedding_of C1,C2 iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) );
theorem Th34: :: CIRCTRM1:34
for S being non empty ManySortedSign
for C being non-empty MSAlgebra over S holds id the carrier of S, id the carrier' of S form_embedding_of C,C
proof
let S be non empty ManySortedSign ; ::_thesis: for C being non-empty MSAlgebra over S holds id the carrier of S, id the carrier' of S form_embedding_of C,C
let C be non-empty MSAlgebra over S; ::_thesis: id the carrier of S, id the carrier' of S form_embedding_of C,C
thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def_12 ::_thesis: ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) )
A1: dom the Sorts of C = the carrier of S by PARTFUN1:def_2;
dom the Charact of C = the carrier' of S by PARTFUN1:def_2;
hence ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) ) by A1, INSTALG1:8, RELAT_1:52; ::_thesis: verum
end;
theorem Th35: :: CIRCTRM1:35
for S1, S2, S3 being non empty ManySortedSign
for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let f1, g1, f2, g2 be Function; ::_thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C2 be non-empty MSAlgebra over S2; ::_thesis: for C3 being non-empty MSAlgebra over S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C3 be non-empty MSAlgebra over S3; ::_thesis: ( f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 implies f2 * f1,g2 * g1 form_embedding_of C1,C3 )
assume that
A1: f1 is one-to-one and
A2: g1 is one-to-one and
A3: f1,g1 form_morphism_between S1,S2 and
A4: the Sorts of C1 = the Sorts of C2 * f1 and
A5: the Charact of C1 = the Charact of C2 * g1 and
A6: f2 is one-to-one and
A7: g2 is one-to-one and
A8: f2,g2 form_morphism_between S2,S3 and
A9: the Sorts of C2 = the Sorts of C3 * f2 and
A10: the Charact of C2 = the Charact of C3 * g2 ; :: according to CIRCTRM1:def_12 ::_thesis: f2 * f1,g2 * g1 form_embedding_of C1,C3
thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A2, A6, A7; :: according to CIRCTRM1:def_12 ::_thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) )
thus f2 * f1,g2 * g1 form_morphism_between S1,S3 by A3, A8, PUA2MSS1:29; ::_thesis: ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) )
thus ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) ) by A4, A5, A9, A10, RELAT_1:36; ::_thesis: verum
end;
definition
let S1, S2 be non empty ManySortedSign ;
let f, g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
predC1,C2 are_similar_wrt f,g means :Def13: :: CIRCTRM1:def 13
( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 );
end;
:: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def_13_:_
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar_wrt f,g iff ( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 ) );
theorem Th36: :: CIRCTRM1:36
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let f, g be Function; ::_thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C2 be non-empty MSAlgebra over S2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies S1,S2 are_equivalent_wrt f,g )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f,g form_morphism_between S1,S2 and
the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g and
f " is one-to-one and
g " is one-to-one and
A4: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_12,CIRCTRM1:def_13 ::_thesis: ( not the Sorts of C2 = the Sorts of C1 * (f ") or not the Charact of C2 = the Charact of C1 * (g ") or S1,S2 are_equivalent_wrt f,g )
thus ( not the Sorts of C2 = the Sorts of C1 * (f ") or not the Charact of C2 = the Charact of C1 * (g ") or S1,S2 are_equivalent_wrt f,g ) by A1, A2, A3, A4, Def9; ::_thesis: verum
end;
theorem Th37: :: CIRCTRM1:37
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let f, g be Function; ::_thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let C2 be non-empty MSAlgebra over S2; ::_thesis: ( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
hereby ::_thesis: ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g implies C1,C2 are_similar_wrt f,g )
assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g )
hence S1,S2 are_equivalent_wrt f,g by Th36; ::_thesis: ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g )
f,g form_embedding_of C1,C2 by A1, Def13;
hence ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) by Def12; ::_thesis: verum
end;
assume that
A2: f is one-to-one and
A3: g is one-to-one and
A4: f,g form_morphism_between S1,S2 and
A5: f " ,g " form_morphism_between S2,S1 and
A6: the Sorts of C1 = the Sorts of C2 * f and
A7: the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def_9 ::_thesis: C1,C2 are_similar_wrt f,g
thus ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) by A2, A3, A4, A6, A7; :: according to CIRCTRM1:def_12,CIRCTRM1:def_13 ::_thesis: f " ,g " form_embedding_of C2,C1
thus ( f " is one-to-one & g " is one-to-one ) by A2, A3; :: according to CIRCTRM1:def_12 ::_thesis: ( f " ,g " form_morphism_between S2,S1 & the Sorts of C2 = the Sorts of C1 * (f ") & the Charact of C2 = the Charact of C1 * (g ") )
thus f " ,g " form_morphism_between S2,S1 by A5; ::_thesis: ( the Sorts of C2 = the Sorts of C1 * (f ") & the Charact of C2 = the Charact of C1 * (g ") )
dom (f ") = the carrier of S2 by A5, PUA2MSS1:def_12;
then rng f = the carrier of S2 by A2, FUNCT_1:33;
then f * (f ") = id the carrier of S2 by A2, FUNCT_1:39
.= id (dom the Sorts of C2) by PARTFUN1:def_2 ;
hence the Sorts of C2 = the Sorts of C2 * (f * (f ")) by RELAT_1:52
.= the Sorts of C1 * (f ") by A6, RELAT_1:36 ;
::_thesis: the Charact of C2 = the Charact of C1 * (g ")
dom (g ") = the carrier' of S2 by A5, PUA2MSS1:def_12;
then rng g = the carrier' of S2 by A3, FUNCT_1:33;
then g * (g ") = id the carrier' of S2 by A3, FUNCT_1:39
.= id (dom the Charact of C2) by PARTFUN1:def_2 ;
hence the Charact of C2 = the Charact of C2 * (g * (g ")) by RELAT_1:52
.= the Charact of C1 * (g ") by A7, RELAT_1:36 ;
::_thesis: verum
end;
theorem :: CIRCTRM1:38
for S being non empty ManySortedSign
for C being non-empty MSAlgebra over S holds C,C are_similar_wrt id the carrier of S, id the carrier' of S
proof
let S be non empty ManySortedSign ; ::_thesis: for C being non-empty MSAlgebra over S holds C,C are_similar_wrt id the carrier of S, id the carrier' of S
let C be non-empty MSAlgebra over S; ::_thesis: C,C are_similar_wrt id the carrier of S, id the carrier' of S
set f = id the carrier of S;
set g = id the carrier' of S;
A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:45;
(id the carrier' of S) " = id the carrier' of S by FUNCT_1:45;
hence ( id the carrier of S, id the carrier' of S form_embedding_of C,C & (id the carrier of S) " ,(id the carrier' of S) " form_embedding_of C,C ) by A1, Th34; :: according to CIRCTRM1:def_13 ::_thesis: verum
end;
theorem Th39: :: CIRCTRM1:39
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
C2,C1 are_similar_wrt f " ,g "
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
C2,C1 are_similar_wrt f " ,g "
let f, g be Function; ::_thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
C2,C1 are_similar_wrt f " ,g "
let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
C2,C1 are_similar_wrt f " ,g "
let C2 be non-empty MSAlgebra over S2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies C2,C1 are_similar_wrt f " ,g " )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f " ,g " form_embedding_of C2,C1 ; :: according to CIRCTRM1:def_13 ::_thesis: C2,C1 are_similar_wrt f " ,g "
A3: f is one-to-one by A1, Def12;
A4: g is one-to-one by A1, Def12;
(f ") " = f by A3, FUNCT_1:43;
hence ( f " ,g " form_embedding_of C2,C1 & (f ") " ,(g ") " form_embedding_of C1,C2 ) by A1, A2, A4, FUNCT_1:43; :: according to CIRCTRM1:def_13 ::_thesis: verum
end;
theorem :: CIRCTRM1:40
for S1, S2, S3 being non empty ManySortedSign
for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let f1, g1, f2, g2 be Function; ::_thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C2 be non-empty MSAlgebra over S2; ::_thesis: for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C3 be non-empty MSAlgebra over S3; ::_thesis: ( C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 implies C1,C3 are_similar_wrt f2 * f1,g2 * g1 )
assume that
A1: f1,g1 form_embedding_of C1,C2 and
A2: f1 " ,g1 " form_embedding_of C2,C1 and
A3: f2,g2 form_embedding_of C2,C3 and
A4: f2 " ,g2 " form_embedding_of C3,C2 ; :: according to CIRCTRM1:def_13 ::_thesis: C1,C3 are_similar_wrt f2 * f1,g2 * g1
thus f2 * f1,g2 * g1 form_embedding_of C1,C3 by A1, A3, Th35; :: according to CIRCTRM1:def_13 ::_thesis: (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1
A5: f1 is one-to-one by A1, Def12;
A6: g1 is one-to-one by A1, Def12;
A7: f2 is one-to-one by A3, Def12;
A8: g2 is one-to-one by A3, Def12;
A9: (f2 * f1) " = (f1 ") * (f2 ") by A5, A7, FUNCT_1:44;
(g2 * g1) " = (g1 ") * (g2 ") by A6, A8, FUNCT_1:44;
hence (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 by A2, A4, A9, Th35; ::_thesis: verum
end;
definition
let S1, S2 be non empty ManySortedSign ;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
predC1,C2 are_similar means :: CIRCTRM1:def 14
ex f, g being Function st C1,C2 are_similar_wrt f,g;
end;
:: deftheorem defines are_similar CIRCTRM1:def_14_:_
for S1, S2 being non empty ManySortedSign
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar iff ex f, g being Function st C1,C2 are_similar_wrt f,g );
theorem Th41: :: CIRCTRM1:41
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) )
assume that
f is one-to-one and
g is one-to-one and
A1: dom f = the carrier of G1 and
A2: dom g = the carrier' of G1 and
A3: rng f c= the carrier of G2 and
A4: rng g c= the carrier' of G2 ; :: according to PUA2MSS1:def_12,CIRCTRM1:def_12 ::_thesis: ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of G1 & b2 = the Arity of G1 . b1 & not b2 * f = the Arity of G2 . (g . b1) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) )
thus ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b1 being set ex b2 being set st
( b1 in the carrier' of G1 & b2 = the Arity of G1 . b1 & not b2 * f = the Arity of G2 . (g . b1) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) ) by A1, A2, A3, A4; ::_thesis: verum
end;
theorem Th42: :: CIRCTRM1:42
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1) )
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
the Sorts of C1 = the Sorts of C2 * f and
A2: the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def_12 ::_thesis: for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let o1 be Gate of G1; ::_thesis: for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let o2 be Gate of G2; ::_thesis: ( o2 = g . o1 implies Den (o2,C2) = Den (o1,C1) )
assume A3: o2 = g . o1 ; ::_thesis: Den (o2,C2) = Den (o1,C1)
dom g = the carrier' of G1 by A1, PUA2MSS1:def_12;
hence Den (o2,C2) = Den (o1,C1) by A2, A3, FUNCT_1:13; ::_thesis: verum
end;
theorem Th43: :: CIRCTRM1:43
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def_12 ::_thesis: for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o1 be Gate of G1; ::_thesis: for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o2 be Gate of G2; ::_thesis: ( o2 = g . o1 implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A2: o2 = g . o1 ; ::_thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A3: s1 = s2 * f ; ::_thesis: o2 depends_on_in s2 = o1 depends_on_in s1
thus o2 depends_on_in s2 = s2 * (the_arity_of o2) by CIRCUIT1:def_3
.= s2 * (f * (the_arity_of o1)) by A1, A2, PUA2MSS1:def_12
.= s1 * (the_arity_of o1) by A3, RELAT_1:36
.= o1 depends_on_in s1 by CIRCUIT1:def_3 ; ::_thesis: verum
end;
theorem Th44: :: CIRCTRM1:44
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for s being State of C2 holds s * f is State of C1 )
set S1 = G1;
set S2 = G2;
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
A2: the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def_12 ::_thesis: for s being State of C2 holds s * f is State of C1
let s be State of C2; ::_thesis: s * f is State of C1
A3: dom the Sorts of C2 = the carrier of G2 by PARTFUN1:def_2;
A4: dom the Sorts of C1 = the carrier of G1 by PARTFUN1:def_2;
A5: dom s = dom the Sorts of C2 by CARD_3:9;
A6: rng f c= the carrier of G2 by A1, PUA2MSS1:def_12;
A7: dom f = the carrier of G1 by A1, PUA2MSS1:def_12;
then A8: dom (s * f) = the carrier of G1 by A3, A5, A6, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G1_holds_
(s_*_f)_._x_in_the_Sorts_of_C1_._x
let x be set ; ::_thesis: ( x in the carrier of G1 implies (s * f) . x in the Sorts of C1 . x )
assume A9: x in the carrier of G1 ; ::_thesis: (s * f) . x in the Sorts of C1 . x
then A10: f . x in rng f by A7, FUNCT_1:def_3;
(s * f) . x = s . (f . x) by A7, A9, FUNCT_1:13;
then (s * f) . x in the Sorts of C2 . (f . x) by A3, A6, A10, CARD_3:9;
hence (s * f) . x in the Sorts of C1 . x by A2, A7, A9, FUNCT_1:13; ::_thesis: verum
end;
hence s * f is State of C1 by A4, A8, CARD_3:9; ::_thesis: verum
end;
theorem Th45: :: CIRCTRM1:45
for G2, G1 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
proof
let G2, G1 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f )
assume A1: f,g form_embedding_of C1,C2 ; ::_thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
then A2: f,g form_morphism_between G1,G2 by Def12;
let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let s1 be State of C1; ::_thesis: ( s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) implies Following s1 = (Following s2) * f )
assume that
A3: s1 = s2 * f and
A4: for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ; ::_thesis: Following s1 = (Following s2) * f
reconsider s29 = (Following s2) * f as State of C1 by A1, Th44;
A5: dom f = the carrier of G1 by A2, PUA2MSS1:def_12;
now__::_thesis:_for_v_being_Vertex_of_G1_holds_
(_(_v_in_InputVertices_G1_implies_s29_._v_=_s1_._v_)_&_(_v_in_InnerVertices_G1_implies_s29_._v_=_(Den_((action_at_v),C1))_._((action_at_v)_depends_on_in_s1)_)_)
let v be Vertex of G1; ::_thesis: ( ( v in InputVertices G1 implies s29 . v = s1 . v ) & ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) ) )
A6: s29 . v = (Following s2) . (f . v) by A5, FUNCT_1:13;
reconsider fv = f . v as Vertex of G2 by A2, Th30;
hereby ::_thesis: ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) )
assume v in InputVertices G1 ; ::_thesis: s29 . v = s1 . v
then A7: s2 is_stable_at f . v by A4;
Following (s2,1) = Following s2 by FACIRC_1:14;
hence s29 . v = s2 . (f . v) by A6, A7, FACIRC_1:def_9
.= s1 . v by A3, A5, FUNCT_1:13 ;
::_thesis: verum
end;
A8: f .: (InnerVertices G1) c= InnerVertices G2 by A2, Th32;
assume A9: v in InnerVertices G1 ; ::_thesis: s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1)
then A10: fv in f .: (InnerVertices G1) by A5, FUNCT_1:def_6;
A11: action_at fv = g . (action_at v) by A2, A9, Th33;
thus s29 . v = (Den ((action_at fv),C2)) . ((action_at fv) depends_on_in s2) by A6, A8, A10, CIRCUIT2:def_5
.= (Den ((action_at v),C1)) . ((action_at fv) depends_on_in s2) by A1, A11, Th42
.= (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) by A1, A3, A11, Th43 ; ::_thesis: verum
end;
hence Following s1 = (Following s2) * f by CIRCUIT2:def_5; ::_thesis: verum
end;
theorem Th46: :: CIRCTRM1:46
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f .: (InputVertices G1) c= InputVertices G2 ; :: according to CIRCTRM1:def_11 ::_thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies Following s1 = (Following s2) * f )
assume A3: s1 = s2 * f ; ::_thesis: Following s1 = (Following s2) * f
A4: dom f = the carrier of G1 by A1, Th41;
now__::_thesis:_for_v_being_Vertex_of_G1_st_v_in_InputVertices_G1_holds_
s2_is_stable_at_f_._v
let v be Vertex of G1; ::_thesis: ( v in InputVertices G1 implies s2 is_stable_at f . v )
assume v in InputVertices G1 ; ::_thesis: s2 is_stable_at f . v
then f . v in f .: (InputVertices G1) by A4, FUNCT_1:def_6;
hence s2 is_stable_at f . v by A2, FACIRC_1:18; ::_thesis: verum
end;
hence Following s1 = (Following s2) * f by A1, A3, Th45; ::_thesis: verum
end;
theorem Th47: :: CIRCTRM1:47
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f )
assume A3: s1 = s2 * f ; ::_thesis: for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
defpred S1[ Element of NAT ] means Following (s1,$1) = (Following (s2,$1)) * f;
Following (s1,0) = s1 by FACIRC_1:11;
then A4: S1[ 0 ] by A3, FACIRC_1:11;
A5: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then Following (Following (s1,n)) = (Following (Following (s2,n))) * f by A1, A2, Th46;
then Following (s1,(n + 1)) = (Following (Following (s2,n))) * f by FACIRC_1:12
.= (Following (s2,(n + 1))) * f by FACIRC_1:12 ;
hence S1[n + 1] ; ::_thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A5); ::_thesis: verum
end;
theorem :: CIRCTRM1:48
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let s1 be State of C1; ::_thesis: ( s1 = s2 * f & s2 is stable implies s1 is stable )
assume A3: s1 = s2 * f ; ::_thesis: ( not s2 is stable or s1 is stable )
assume s2 = Following s2 ; :: according to CIRCUIT2:def_6 ::_thesis: s1 is stable
hence s1 = Following s1 by A1, A2, A3, Th46; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;
theorem Th49: :: CIRCTRM1:49
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume A3: s1 = s2 * f ; ::_thesis: for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let v1 be Vertex of G1; ::_thesis: ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
A4: f,g form_morphism_between G1,G2 by A1, Def12;
then A5: dom f = the carrier of G1 by PUA2MSS1:def_12;
reconsider v2 = f . v1 as Vertex of G2 by A4, Th30;
thus ( s1 is_stable_at v1 implies s2 is_stable_at f . v1 ) ::_thesis: ( s2 is_stable_at f . v1 implies s1 is_stable_at v1 )
proof
assume A6: for n being Nat holds (Following (s1,n)) . v1 = s1 . v1 ; :: according to FACIRC_1:def_9 ::_thesis: s2 is_stable_at f . v1
let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s2,n)) . (f . v1) = s2 . (f . v1)
n in NAT by ORDINAL1:def_12;
then Following (s1,n) = (Following (s2,n)) * f by A1, A2, A3, Th47;
hence (Following (s2,n)) . (f . v1) = (Following (s1,n)) . v1 by A5, FUNCT_1:13
.= s1 . v1 by A6
.= s2 . (f . v1) by A3, A5, FUNCT_1:13 ;
::_thesis: verum
end;
assume A7: for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1) ; :: according to FACIRC_1:def_9 ::_thesis: s1 is_stable_at v1
let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s1,n)) . v1 = s1 . v1
n in NAT by ORDINAL1:def_12;
then Following (s1,n) = (Following (s2,n)) * f by A1, A2, A3, Th47;
hence (Following (s1,n)) . v1 = (Following (s2,n)) . v2 by A5, FUNCT_1:13
.= s2 . v2 by A7
.= s1 . v1 by A3, A5, FUNCT_1:13 ;
::_thesis: verum
end;
theorem :: CIRCTRM1:50
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s being State of C2 holds s * f is State of C1
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s being State of C2 holds s * f is State of C1 )
assume f,g form_embedding_of C1,C2 ; :: according to CIRCTRM1:def_13 ::_thesis: ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 )
hence ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 ) by Th44; ::_thesis: verum
end;
theorem Th51: :: CIRCTRM1:51
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") ) )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f " ,g " form_embedding_of C2,C1 ; :: according to CIRCTRM1:def_13 ::_thesis: for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
A3: f is one-to-one by A1, Def12;
let s1 be State of C1; ::_thesis: for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let s2 be State of C2; ::_thesis: ( s1 = s2 * f iff s2 = s1 * (f ") )
f,g form_morphism_between G1,G2 by A1, Def12;
then A4: dom f = the carrier of G1 by PUA2MSS1:def_12;
A5: dom s1 = the carrier of G1 by CIRCUIT1:3;
A6: (s1 * (f ")) * f = s1 * ((f ") * f) by RELAT_1:36
.= s1 * (id (dom f)) by A3, FUNCT_1:39
.= s1 by A4, A5, RELAT_1:52 ;
f " ,g " form_morphism_between G2,G1 by A2, Def12;
then A7: dom (f ") = the carrier of G2 by PUA2MSS1:def_12;
A8: dom s2 = the carrier of G2 by CIRCUIT1:3;
(s2 * f) * (f ") = s2 * (f * (f ")) by RELAT_1:36
.= s2 * (((f ") ") * (f ")) by A3, FUNCT_1:43
.= s2 * (id (dom (f "))) by A3, FUNCT_1:39 ;
hence ( s1 = s2 * f iff s2 = s1 * (f ") ) by A6, A7, A8, RELAT_1:52; ::_thesis: verum
end;
theorem Th52: :: CIRCTRM1:52
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) )
assume C1,C2 are_similar_wrt f,g ; ::_thesis: ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 )
then G1,G2 are_equivalent_wrt f,g by Th36;
hence ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) by Th28; ::_thesis: verum
end;
theorem Th53: :: CIRCTRM1:53
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
f preserves_inputs_of G1,G2
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
f preserves_inputs_of G1,G2
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
f preserves_inputs_of G1,G2
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
f preserves_inputs_of G1,G2
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies f preserves_inputs_of G1,G2 )
assume C1,C2 are_similar_wrt f,g ; ::_thesis: f preserves_inputs_of G1,G2
hence f .: (InputVertices G1) c= InputVertices G2 by Th52; :: according to CIRCTRM1:def_11 ::_thesis: verum
end;
theorem Th54: :: CIRCTRM1:54
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f )
assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f
then f,g form_embedding_of C1,C2 by Def13;
hence for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
Following s1 = (Following s2) * f by A1, Th46, Th53; ::_thesis: verum
end;
theorem Th55: :: CIRCTRM1:55
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f )
assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f
then f,g form_embedding_of C1,C2 by Def13;
hence for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f by A1, Th47, Th53; ::_thesis: verum
end;
theorem :: CIRCTRM1:56
for G1, G2 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
proof
let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable ) )
assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
then A2: C2,C1 are_similar_wrt f " ,g " by Th39;
let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds
( s1 is stable iff s2 is stable )
let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies ( s1 is stable iff s2 is stable ) )
assume A3: s1 = s2 * f ; ::_thesis: ( s1 is stable iff s2 is stable )
A4: s2 = s1 * (f ") by A1, A3, Th51;
thus ( s1 is stable implies s2 is stable ) ::_thesis: ( s2 is stable implies s1 is stable )
proof
assume s1 = Following s1 ; :: according to CIRCUIT2:def_6 ::_thesis: s2 is stable
hence s2 = Following s2 by A2, A4, Th54; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;
assume s2 = Following s2 ; :: according to CIRCUIT2:def_6 ::_thesis: s1 is stable
hence s1 = Following s1 by A1, A3, Th54; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;
theorem :: CIRCTRM1:57
for G2, G1 being non empty non void Circuit-like ManySortedSign
for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
proof
let G2, G1 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
then A2: C2,C1 are_similar_wrt f " ,g " by Th39;
let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume A3: s1 = s2 * f ; ::_thesis: for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let v1 be Vertex of G1; ::_thesis: ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
A4: G1,G2 are_equivalent_wrt f,g by A1, Th37;
then A5: f,g form_morphism_between G1,G2 by Def9;
A6: f " ,g " form_morphism_between G2,G1 by A4, Def9;
A7: dom f = the carrier of G1 by A5, PUA2MSS1:def_12;
A8: dom (f ") = the carrier of G2 by A6, PUA2MSS1:def_12;
reconsider v2 = f . v1 as Vertex of G2 by A5, Th30;
f is one-to-one by A4, Def9;
then A9: v1 = (f ") . v2 by A7, FUNCT_1:34;
thus ( s1 is_stable_at v1 implies s2 is_stable_at f . v1 ) ::_thesis: ( s2 is_stable_at f . v1 implies s1 is_stable_at v1 )
proof
assume A10: for n being Nat holds (Following (s1,n)) . v1 = s1 . v1 ; :: according to FACIRC_1:def_9 ::_thesis: s2 is_stable_at f . v1
let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s2,n)) . (f . v1) = s2 . (f . v1)
n in NAT by ORDINAL1:def_12;
then Following (s1,n) = (Following (s2,n)) * f by A1, A3, Th55;
hence (Following (s2,n)) . (f . v1) = (Following (s1,n)) . v1 by A7, FUNCT_1:13
.= s1 . v1 by A10
.= s2 . (f . v1) by A3, A7, FUNCT_1:13 ;
::_thesis: verum
end;
assume A11: for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1) ; :: according to FACIRC_1:def_9 ::_thesis: s1 is_stable_at v1
let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s1,n)) . v1 = s1 . v1
A12: n in NAT by ORDINAL1:def_12;
s2 = s1 * (f ") by A1, A3, Th51;
then Following (s2,n) = (Following (s1,n)) * (f ") by A2, A12, Th55;
hence (Following (s1,n)) . v1 = (Following (s2,n)) . v2 by A8, A9, FUNCT_1:13
.= s2 . v2 by A11
.= s1 . v1 by A3, A7, FUNCT_1:13 ;
::_thesis: verum
end;
begin
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
let X be non empty Subset of (S -Terms V);
let G be non empty non void Circuit-like ManySortedSign ;
let C be non-empty Circuit of G;
predC calculates X,A means :Def15: :: CIRCTRM1:def 15
ex f, g being Function st
( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G );
predX,A specifies C means :: CIRCTRM1:def 16
C,X -Circuit A are_similar ;
end;
:: deftheorem Def15 defines calculates CIRCTRM1:def_15_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G holds
( C calculates X,A iff ex f, g being Function st
( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G ) );
:: deftheorem defines specifies CIRCTRM1:def_16_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G holds
( X,A specifies C iff C,X -Circuit A are_similar );
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let X be non empty Subset of (S -Terms V);
let G be non empty non void Circuit-like ManySortedSign ;
let C be non-empty Circuit of G;
assume C calculates X,A ;
then consider f, g being Function such that
A1: f,g form_embedding_of X -Circuit A,C and
A2: f preserves_inputs_of X -CircuitStr ,G by Def15;
A3: f is one-to-one by A1, Def12;
mode SortMap of X,A,C -> one-to-one Function means :Def17: :: CIRCTRM1:def 17
( it preserves_inputs_of X -CircuitStr ,G & ex g being Function st it,g form_embedding_of X -Circuit A,C );
existence
ex b1 being one-to-one Function st
( b1 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b1,g form_embedding_of X -Circuit A,C ) by A1, A2, A3;
end;
:: deftheorem Def17 defines SortMap CIRCTRM1:def_17_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for b7 being one-to-one Function holds
( b7 is SortMap of X,A,C iff ( b7 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b7,g form_embedding_of X -Circuit A,C ) );
definition
let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let X be non empty Subset of (S -Terms V);
let G be non empty non void Circuit-like ManySortedSign ;
let C be non-empty Circuit of G;
assume B1: C calculates X,A ;
let f be SortMap of X,A,C;
consider g being Function such that
A1: f,g form_embedding_of X -Circuit A,C by B1, Def17;
A2: g is one-to-one by A1, Def12;
mode OperMap of X,A,C,f -> one-to-one Function means :: CIRCTRM1:def 18
f,it form_embedding_of X -Circuit A,C;
existence
ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C by A1, A2;
end;
:: deftheorem defines OperMap CIRCTRM1:def_18_:_
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for b8 being one-to-one Function holds
( b8 is OperMap of X,A,C,f iff f,b8 form_embedding_of X -Circuit A,C );
theorem Th58: :: CIRCTRM1:58
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A
let C be non-empty Circuit of G; ::_thesis: ( X,A specifies C implies C calculates X,A )
given f, g being Function such that A1: C,X -Circuit A are_similar_wrt f,g ; :: according to CIRCTRM1:def_14,CIRCTRM1:def_16 ::_thesis: C calculates X,A
take f " ; :: according to CIRCTRM1:def_15 ::_thesis: ex g being Function st
( f " ,g form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G )
take g " ; ::_thesis: ( f " ,g " form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G )
thus f " ,g " form_embedding_of X -Circuit A,C by A1, Def13; ::_thesis: f " preserves_inputs_of X -CircuitStr ,G
X -Circuit A,C are_similar_wrt f " ,g " by A1, Th39;
hence f " preserves_inputs_of X -CircuitStr ,G by Th53; ::_thesis: verum
end;
theorem Th59: :: CIRCTRM1:59
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let C be non-empty Circuit of G; ::_thesis: ( C calculates X,A implies for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) )
assume A1: C calculates X,A ; ::_thesis: for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let f be SortMap of X,A,C; ::_thesis: for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
consider g being Function such that
A2: f,g form_embedding_of X -Circuit A,C by A1, Def17;
A3: f preserves_inputs_of X -CircuitStr ,G by A1, Def17;
A4: f,g form_morphism_between X -CircuitStr ,G by A2, Def12;
let t be Term of S,V; ::_thesis: ( t in Subtrees X implies for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) )
assume A5: t in Subtrees X ; ::_thesis: for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let s be State of C; ::_thesis: ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
reconsider s9 = s * f as State of (X -Circuit A) by A2, Th44;
reconsider t9 = t as Vertex of (X -CircuitStr) by A5;
A6: Following (s9,(1 + (height (dom t)))) is_stable_at t9 by Th21;
A7: Following (s9,(1 + (height (dom t)))) = (Following (s,(1 + (height (dom t))))) * f by A2, A3, Th47;
hence Following (s,(1 + (height (dom t)))) is_stable_at f . t by A2, A3, A6, Th49; ::_thesis: for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A)
let s9 be State of (X -Circuit A); ::_thesis: ( s9 = s * f implies for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) )
assume A8: s9 = s * f ; ::_thesis: for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A)
let h be CompatibleValuation of s9; ::_thesis: (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A)
A9: dom f = the carrier of (X -CircuitStr) by A4, PUA2MSS1:def_12;
(Following (s9,(1 + (height (dom t))))) . t9 = t @ (h,A) by Th21;
hence (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) by A7, A8, A9, FUNCT_1:13; ::_thesis: verum
end;
theorem Th60: :: CIRCTRM1:60
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st C calculates X,A holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let C be non-empty Circuit of G; ::_thesis: ( C calculates X,A implies for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) )
assume A1: C calculates X,A ; ::_thesis: for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
then consider f, g being Function such that
A2: f,g form_embedding_of X -Circuit A,C and
A3: f preserves_inputs_of X -CircuitStr ,G by Def15;
f is one-to-one by A2, Def12;
then reconsider f = f as SortMap of X,A,C by A1, A2, A3, Def17;
let t be Term of S,V; ::_thesis: ( t in Subtrees X implies ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) )
assume A4: t in Subtrees X ; ::_thesis: ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
A5: f,g form_morphism_between X -CircuitStr ,G by A2, Def12;
reconsider t9 = t as Vertex of (X -CircuitStr) by A4;
reconsider v = f . t9 as Vertex of G by A5, Th30;
take v ; ::_thesis: for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
let s be State of C; ::_thesis: ( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) )
thus Following (s,(1 + (height (dom t)))) is_stable_at v by A1, Th59; ::_thesis: ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A)
take f ; ::_thesis: for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A)
thus for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) by A1, Th59; ::_thesis: verum
end;
theorem :: CIRCTRM1:61
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
let C be non-empty Circuit of G; ::_thesis: ( X,A specifies C implies for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) )
assume X,A specifies C ; ::_thesis: for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )
then C calculates X,A by Th58;
hence for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) by Th59; ::_thesis: verum
end;
theorem :: CIRCTRM1:62
for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) by Th58, Th60;