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 s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A1:
( InputVertices S1 misses InnerVertices S2 & 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 s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
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 s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
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 s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A be non-empty Circuit of S; ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A2:
( A1 tolerates A2 & A = A1 +* A2 )
; for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s be State of A; for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s1 be State of A1; ( s1 = s | the carrier of S1 implies for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A3:
s1 = s | the carrier of S1
; for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let n be natural Number ; (Following (s,n)) | the carrier of S1 = Following (s1,n)
A0:
n is Nat
by TARSKI:1;
defpred S3[ Nat] means (Following (s,$1)) | the carrier of S1 = Following (s1,$1);
A4:
now for n being Nat st S3[n] holds
S3[n + 1]end;
(Following (s,0)) | the carrier of S1 =
s1
by A3, FACIRC_1:11
.=
Following (s1,0)
by FACIRC_1:11
;
then A6:
S3[ 0 ]
;
for n being Nat holds S3[n]
from NAT_1:sch 2(A6, A4);
hence
(Following (s,n)) | the carrier of S1 = Following (s1,n)
by A0; verum