:: deftheorem defines succ AOFA_A00:def 26 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for C being image of A
for G being GeneratorSystem over S,X,A st G is C -supported holds
for s being Element of C -States the generators of G
for r being SortSymbol of S
for v being Element of C,r
for t being Element of G,r
for b₁₀ being Element of C -States the generators of G holds
( b₁₀ = succ (s,t,v) iff ( (b₁₀ . r) . t = v & ( for p being SortSymbol of S
for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (b₁₀ . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(supp-var t),v) & x in (vf t) . p holds
for q being Element of A,p st q = ((supp-term t) . p) . x holds
(b₁₀ . p) . x = q value_at (C,u) ) ) ) ) );