let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( S1 tolerates S2 & InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable )
assume A1: ( S1 tolerates S2 & InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 ) ; :: thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let C1 be non-empty Circuit of S1; :: thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let C2 be non-empty Circuit of S2; :: thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let C be non-empty Circuit of S; :: thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable )
assume A2: ( C1 tolerates C2 & C = C1 +* C2 ) ; :: thesis: for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let s1 be State of C1; :: thesis: for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let s2 be State of C2; :: thesis: for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable
let s be State of C; :: thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable implies s is stable )
assume that
A3: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 ) and
A4: ( s1 is stable & s2 is stable ) ; :: thesis: s is stable
( dom s = the carrier of S & the carrier of S = the carrier of S1 \/ the carrier of S2 ) by A1, CIRCCOMB:def 2, CIRCUIT1:4;
then s = s1 +* s2 by A3, FUNCT_4:74;
then s = (Following s1) +* s2 by A4, CIRCUIT2:def 6
.= (Following s1) +* (Following s2) by A4, CIRCUIT2:def 6
.= Following s by A1, A2, A3, CIRCCOMB:39 ;
hence s = Following s ; :: according to CIRCUIT2:def 6 :: thesis: verum