let F be NAT -defined the InstructionsF of SCM -valued total Function; ( <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies for i1, i2 being Integer
for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) ) )
assume A1:
<%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F
; for i1, i2 being Integer
for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
let i1, i2 be Integer; for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
let s be 0 -started State-consisting of <%i1,i2%>; ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
set s1 = Comput (F,s,(0 + 1));
A2:
dl. 0 <> dl. 1
by AMI_3:10;
A3:
( IC s = 0 & F . 0 = Divide ((dl. 0),(dl. 1)) )
by A1, Th3, MEMSTR_0:def 11;
A4:
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
by Th2;
A5:
s = Comput (F,s,0)
by EXTPRO_1:2;
F . 1 = halt SCM
by A1, Th3;
then A6:
F . (IC (Comput (F,s,(0 + 1)))) = halt SCM
by A3, A2, A5, Th8;
hence
F halts_on s
by EXTPRO_1:30; ( LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
Divide ((dl. 0),(dl. 1)) <> halt SCM
by Th12;
hence
LifeSpan (F,s) = 1
by A3, A5, A6, EXTPRO_1:32; ( (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
thus (Result (F,s)) . (dl. 0) =
(Comput (F,s,(0 + 1))) . (dl. 0)
by A6, EXTPRO_1:7
.=
i1 div i2
by A3, A4, A2, A5, Th8
; ( (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
thus (Result (F,s)) . (dl. 1) =
(Comput (F,s,(0 + 1))) . (dl. 1)
by A6, EXTPRO_1:7
.=
i1 mod i2
by A3, A4, A2, A5, Th8
; for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ( d <> dl. 0 & d <> dl. 1 implies (Result (F,s)) . d = s . d )
assume A7:
( d <> dl. 0 & d <> dl. 1 )
; (Result (F,s)) . d = s . d
thus (Result (F,s)) . d =
(Comput (F,s,(0 + 1))) . d
by A6, EXTPRO_1:7
.=
s . d
by A3, A2, A5, A7, Th8
; verum