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