let S be non empty non void Circuit-like ManySortedSign ; :: thesis: for A being non-empty Circuit of S

for s being State of A

for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let A be non-empty Circuit of S; :: thesis: for s being State of A

for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let s be State of A; :: thesis: for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let n1, n2 be natural Number ; :: thesis: ( Following (s,n1) is stable & n1 <= n2 implies Following (s,n2) = Following (s,n1) )

assume that

A1: Following (s,n1) is stable and

A2: n1 <= n2 ; :: thesis: Following (s,n2) = Following (s,n1)

consider k being Nat such that

A3: n2 = n1 + k by A2, NAT_1:10;

reconsider k = k as Nat ;

( n1 is Nat & n2 is Nat ) by TARSKI:1;

then Following (s,n2) = Following ((Following (s,n1)),k) by A3, FACIRC_1:13;

hence Following (s,n2) = Following (s,n1) by A1, Th3; :: thesis: verum

for s being State of A

for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let A be non-empty Circuit of S; :: thesis: for s being State of A

for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let s be State of A; :: thesis: for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds

Following (s,n2) = Following (s,n1)

let n1, n2 be natural Number ; :: thesis: ( Following (s,n1) is stable & n1 <= n2 implies Following (s,n2) = Following (s,n1) )

assume that

A1: Following (s,n1) is stable and

A2: n1 <= n2 ; :: thesis: Following (s,n2) = Following (s,n1)

consider k being Nat such that

A3: n2 = n1 + k by A2, NAT_1:10;

reconsider k = k as Nat ;

( n1 is Nat & n2 is Nat ) by TARSKI:1;

then Following (s,n2) = Following ((Following (s,n1)),k) by A3, FACIRC_1:13;

hence Following (s,n2) = Following (s,n1) by A1, Th3; :: thesis: verum