let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%(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 ; :: thesis: 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; :: thesis: 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%>; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds

(Result (F,s)) . d = s . d

let d be Data-Location; :: thesis: ( d <> dl. 0 & d <> dl. 1 implies (Result (F,s)) . d = s . d )

assume A7: ( d <> dl. 0 & d <> dl. 1 ) ; :: thesis: (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 ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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%>; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds

(Result (F,s)) . d = s . d

let d be Data-Location; :: thesis: ( d <> dl. 0 & d <> dl. 1 implies (Result (F,s)) . d = s . d )

assume A7: ( d <> dl. 0 & d <> dl. 1 ) ; :: thesis: (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 ; :: thesis: verum