let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable )
assume that
A1:
InputVertices S1 misses InnerVertices S2
and
A2:
S = S1 +* S2
; for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let A1 be non-empty Circuit of S1; for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let A2 be non-empty Circuit of S2; for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let A be non-empty Circuit of S; ( A1 tolerates A2 & A = A1 +* A2 implies for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable )
assume that
A3:
A1 tolerates A2
and
A4:
A = A1 +* A2
; for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let n1, n2 be Nat; for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let s be State of A; for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & Following (s1,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let s9 be State of A1; for s2 being State of A2 st s9 = s | the carrier of S1 & Following (s9,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let s99 be State of A2; ( s9 = s | the carrier of S1 & Following (s9,n1) is stable & s99 = (Following (s,n1)) | the carrier of S2 & Following (s99,n2) is stable implies Following (s,(n1 + n2)) is stable )
assume that
A5:
( s9 = s | the carrier of S1 & Following (s9,n1) is stable )
and
A6:
( s99 = (Following (s,n1)) | the carrier of S2 & Following (s99,n2) is stable )
; Following (s,(n1 + n2)) is stable
A7:
the Sorts of A1 tolerates the Sorts of A2
by A3, CIRCCOMB:def 3;
then reconsider s1 = (Following (s,n1)) | the carrier of S1, s0 = s | the carrier of S1 as State of A1 by A4, CIRCCOMB:26;
A8:
Following ((Following (s,n1)),n2) = Following (s,(n1 + n2))
by FACIRC_1:13;
then A9:
(Following (s,(n1 + n2))) | the carrier of S1 = Following (s1,n2)
by A1, A2, A3, A4, Th13;
reconsider s2 = (Following (s,n1)) | the carrier of S2 as State of A2 by A4, A7, CIRCCOMB:26;
A10:
dom (Following (s,(n1 + n2))) = the carrier of S
by CIRCUIT1:3;
A11:
the carrier of S = the carrier of S1 \/ the carrier of S2
by A2, CIRCCOMB:def 2;
A12:
s1 = Following (s0,n1)
by A1, A2, A3, A4, Th13;
then A13:
(Following (s,(n1 + n2))) | the carrier of S2 = Following (s2,n2)
by A1, A2, A3, A4, A5, A8, Th18;
then Following (Following (s,(n1 + n2))) =
(Following (Following (s2,n2))) +* (Following (Following (s1,n2)))
by A1, A2, A3, A4, A9, CIRCCOMB:33
.=
(Following (s2,n2)) +* (Following (Following (s1,n2)))
by A6
.=
(Following (s2,n2)) +* (Following (s1,(n2 + 1)))
by FACIRC_1:12
.=
(Following (s2,n2)) +* s1
by A5, A12, Th3
.=
(Following (s2,n2)) +* (Following (s1,n2))
by A5, A12, Th3
.=
Following (s,(n1 + n2))
by A11, A10, A9, A13, FUNCT_4:70
;
hence
Following (s,(n1 + n2)) is stable
; verum