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