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 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 ;
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