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