let i1, i2 be Integer; :: thesis: for s being State-consisting of 0 , 0 , 0 ,<%(Divide (dl. 0 ),(dl. 1))%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*> holds
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = 1 & (Result (ProgramPart s),s) . (dl. 0 ) = i1 div i2 & (Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
let s be State-consisting of 0 , 0 , 0 ,<%(Divide (dl. 0 ),(dl. 1))%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*>; :: thesis: ( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = 1 & (Result (ProgramPart s),s) . (dl. 0 ) = i1 div i2 & (Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
set s1 = Comput (ProgramPart s),s,(0 + 1);
A1: dl. 0 <> dl. 1 by AMI_3:52;
A2: ( IC s = 0 & s . 0 = Divide (dl. 0 ),(dl. 1) ) by Th15;
A3: ( s . (dl. 0 ) = i1 & s . (dl. 1) = i2 ) by Th15;
A4: s = Comput (ProgramPart s),s,0 by AMI_1:13;
s . 1 = halt SCM by Th15;
then A5: s . (IC (Comput (ProgramPart s),s,(0 + 1))) = halt SCM by A2, A1, A4, Th22;
hence ProgramPart s halts_on s by Th3; :: thesis: ( LifeSpan (ProgramPart s),s = 1 & (Result (ProgramPart s),s) . (dl. 0 ) = i1 div i2 & (Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
Divide (dl. 0 ),(dl. 1) <> halt SCM by Th26;
hence LifeSpan (ProgramPart s),s = 1 by A2, A4, A5, Th16; :: thesis: ( (Result (ProgramPart s),s) . (dl. 0 ) = i1 div i2 & (Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
thus (Result (ProgramPart s),s) . (dl. 0 ) = (Comput (ProgramPart s),s,(0 + 1)) . (dl. 0 ) by A5, Th4
.= i1 div i2 by A2, A3, A1, A4, Th22 ; :: thesis: ( (Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
thus (Result (ProgramPart s),s) . (dl. 1) = (Comput (ProgramPart s),s,(0 + 1)) . (dl. 1) by A5, Th4
.= i1 mod i2 by A2, A3, A1, A4, Th22 ; :: thesis: for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d
let d be Data-Location ; :: thesis: ( d <> dl. 0 & d <> dl. 1 implies (Result (ProgramPart s),s) . d = s . d )
assume A6: ( d <> dl. 0 & d <> dl. 1 ) ; :: thesis: (Result (ProgramPart s),s) . d = s . d
thus (Result (ProgramPart s),s) . d = (Comput (ProgramPart s),s,(0 + 1)) . d by A5, Th4
.= s . d by A2, A1, A4, A6, Th22 ; :: thesis: verum