let x be FinPartState of SCM; :: thesis: ( x in dom powerSCMFunction implies Initialize x is Autonomy of IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) )
assume A1: x in dom powerSCMFunction ; :: thesis: Initialize x is Autonomy of IterativeAlgorithm (MultBy ((dl. 2),(dl. 1)))
set I = MultBy ((dl. 2),(dl. 1));
A2: ( MultBy ((dl. 2),(dl. 1)) = AddTo ((dl. 2),(dl. 1)) or MultBy ((dl. 2),(dl. 1)) = SubFrom ((dl. 2),(dl. 1)) or MultBy ((dl. 2),(dl. 1)) = MultBy ((dl. 2),(dl. 1)) ) ;
deffunc H₃( Nat) -> Element of omega = 1;
A3: for x being object st x in dom powerSCMFunction holds
ex n being Nat st x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,H₃(n)) by Th33;
A4: for P, Q being Instruction-Sequence of SCM st IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P & IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= Q holds
for x being FinPartState of SCM st x in dom powerSCMFunction 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)

proof

let P, Q be Instruction-Sequence of SCM; :: thesis: ( IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P & IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= Q implies for x being FinPartState of SCM st x in dom powerSCMFunction 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) )
assume that
A5: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P and
A6: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= Q ; :: thesis: for x being FinPartState of SCM st x in dom powerSCMFunction 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)
let x be FinPartState of SCM; :: thesis: ( x in dom powerSCMFunction implies 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) )
assume A7: x in dom powerSCMFunction ; :: thesis: 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)
let s1, s2 be State of SCM; :: thesis: ( Initialize x c= s1 & Initialize x c= s2 implies for k being Nat holds (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2) )
assume that
A8: Initialize x c= s1 and
A9: Initialize x c= s2 ; :: thesis: for k being Nat holds (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2)
consider n being Nat such that
A10: x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,H₃(n)) by A7, Th33;
let k be Nat; :: thesis: (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2)
reconsider P = P as IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM by A5, PROOFS_1:def 12;
reconsider Q = Q as IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM by A6, PROOFS_1:def 12;
reconsider s1 = s1 as 0 -started State-consisting of <%1,n,H₃(n)%> by A10, A8, Th15, MEMSTR_0:17;
reconsider s2 = s2 as 0 -started State-consisting of <%1,n,H₃(n)%> by A10, A9, Th15, MEMSTR_0:17;
defpred S₁[ Nat] means (Comput (P,s1,$1)) . (dl. 2) = (Comput (Q,s2,$1)) . (dl. 2);
(Comput (P,s1,0)) . (dl. 2) = H₃(n) by Th14
.= (Comput (Q,s2,0)) . (dl. 2) by Th14 ;
then A11: S₁[ 0 ] ;
A12: 4 > 0 ;
A13: for i, j being Nat st S₁[4 * i] & j <> 0 & j <= 4 holds
S₁[(4 * i) + j]

proof

let i, j be Nat; :: thesis: ( S₁[4 * i] & j <> 0 & j <= 4 implies S₁[(4 * i) + j] )
assume that
S₁[4 * i] and
A14: j <> 0 and
A15: j <= 4 ; :: thesis: S₁[(4 * i) + j]
reconsider j1 = j - 1 as Nat by A14;

per cases ( i >= n or i < n ) ;

suppose A16: i >= n ; :: thesis: S₁[(4 * i) + j]

(Comput (P,s1,((4 * i) + j))) . (dl. 2) = (Comput (P,s1,(((4 * i) + 1) + j1))) . (dl. 2)
.= n ! by A16, Th32
.= (Comput (Q,s2,(((4 * i) + 1) + j1))) . (dl. 2) by A16, Th32
.= (Comput (Q,s2,((4 * i) + j))) . (dl. 2) ;
hence S₁[(4 * i) + j] ; :: thesis: verum

end;

suppose A17: i < n ; :: thesis: S₁[(4 * i) + j]

(Comput (P,s1,((4 * i) + 2))) . (dl. 1) = n - i by A5, A17, Th29
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) by A6, A17, Th29 ;
then A18: (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) = (n !) / ((((Comput (P,s1,((4 * i) + 2))) . (dl. 1)) -' 1) !) by A17, Th32
.= (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A17, Th32 ;
A19: (Comput (Q,s2,((4 * i) + 3))) . (dl. 2) = (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) by A17, Th32
.= (Comput (P,s1,((4 * i) + 3))) . (dl. 2) by A17, A18, Th32 ;
not not j = 0 & ... & not j = 4 by A15;

per cases then ( j = 1 or j = 2 or j = 3 or j = 4 ) by A14;

suppose A20: j = 1 ; :: thesis: S₁[(4 * i) + j]

(Comput (P,s1,((4 * i) + 1))) . (dl. 1) = n - i by A5, A17, Th29
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) by A6, A17, Th29 ;
then (Comput (Q,s2,((4 * i) + 1))) . (dl. 2) = (n !) / (((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) !) by A17, Th32
.= (Comput (P,s1,((4 * i) + 1))) . (dl. 2) by A17, Th32 ;
hence S₁[(4 * i) + j] by A20; :: thesis: verum

end;

suppose j = 2 ; :: thesis: S₁[(4 * i) + j]

hence S₁[(4 * i) + j] by A18; :: thesis: verum

end;

suppose j = 3 ; :: thesis: S₁[(4 * i) + j]

hence S₁[(4 * i) + j] by A19; :: thesis: verum

end;

suppose A21: j = 4 ; :: thesis: S₁[(4 * i) + j]

(Comput (Q,s2,((4 * i) + 4))) . (dl. 2) = (Comput (Q,s2,((4 * i) + 3))) . (dl. 2) by A17, Th32
.= (Comput (P,s1,((4 * i) + 4))) . (dl. 2) by A17, A19, Th32 ;
hence S₁[(4 * i) + j] by A21; :: thesis: verum

end;

end;

end;

end;

end;

reconsider k = k as Element of NAT by ORDINAL1:def 12;
S₁[k] from NAT_D:sch 2(A11, A12, A13);
hence (Comput (P,s1,k)) . (dl. 2) = (Comput (Q,s2,k)) . (dl. 2) ; :: thesis: verum

end;

for x being FinPartState of SCM st x in dom powerSCMFunction holds
Initialize x is Autonomy of IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) from AMI_8:sch 7(A2, A3, A4);
hence Initialize x is Autonomy of IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) by A1; :: thesis: verum