let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( InputVertices S1 misses InnerVertices 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 that
A1: InputVertices S1 misses InnerVertices S2 and
A2: 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 A3: ( 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
A4: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 ) and
A5: s1 is stable and
A6: 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 A2, CIRCCOMB:def 2, CIRCUIT1:3;
then s = s2 +* s1 by A4, FUNCT_4:70;
then s = (Following s2) +* s1 by A6, CIRCUIT2:def 6
.= (Following s2) +* (Following s1) by A5, CIRCUIT2:def 6
.= Following s by A1, A2, A3, A4, CIRCCOMB:33 ;
hence s = Following s ; :: according to CIRCUIT2:def 6 :: thesis: verum