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 Nat 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 Nat 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 Nat st Following s,n1 is stable & n1 <= n2 holds
Following s,n2 = Following s,n1
let n1, n2 be Nat; :: thesis: ( Following s,n1 is stable & n1 <= n2 implies Following s,n2 = Following s,n1 )
assume A1: ( Following s,n1 is stable & n1 <= n2 ) ; :: thesis: Following s,n2 = Following s,n1
consider k being Nat such that
A2: n2 = n1 + k by A1, NAT_1:10;
reconsider k = k as Nat ;
Following s,n2 = Following (Following s,n1),k by A2, FACIRC_1:13;
hence Following s,n2 = Following s,n1 by A1, Th3; :: thesis: verum