scheme :: AMI_8:sch 7
AutonomySch{ F₁() -> PartFunc of (FinPartSt SCM),(FinPartSt SCM), F₂() -> Instruction of SCM, F₃( object ) -> Nat } :

for x being FinPartState of SCM st x in dom F₁() holds
Initialize x is Autonomy of IterativeAlgorithm F₂()

provided

A1: ( F₂() = AddTo ((dl. 2),(dl. 1)) or F₂() = SubFrom ((dl. 2),(dl. 1)) or F₂() = MultBy ((dl. 2),(dl. 1)) ) and
A2: for x being object st x in dom F₁() holds
ex n being Nat st x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,F₃(n)) and
A3: for P, Q being Instruction-Sequence of SCM st IterativeAlgorithm F₂() c= P & IterativeAlgorithm F₂() c= Q holds
for x being FinPartState of SCM st x in dom F₁() holds
for s1, s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2 holds
for k being Nat holds (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2)