let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%(SCM-goto 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 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) ) )

assume A1: <%(SCM-goto 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 & ( for d being Data-Location 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 & ( for d being Data-Location 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 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

set s1 = Comput (F,s,(0 + 1));

A2: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def 11;

A3: F . 0 = SCM-goto 1 by A1, Th3;

then A4: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, Th9;

A5: F . 1 = halt SCM by A1, Th3;

hence F halts_on s by A4, EXTPRO_1:30; :: thesis: ( LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

thus LifeSpan (F,s) = 1 by A5, A2, A4, EXTPRO_1:33; :: thesis: for d being Data-Location holds (Result (F,s)) . d = s . d

let d be Data-Location; :: thesis: (Result (F,s)) . d = s . d

thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A5, A4, EXTPRO_1:7

.= s . d by A3, A2, Th9 ; :: thesis: verum

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) ) )

assume A1: <%(SCM-goto 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 & ( for d being Data-Location 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 & ( for d being Data-Location 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 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

set s1 = Comput (F,s,(0 + 1));

A2: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def 11;

A3: F . 0 = SCM-goto 1 by A1, Th3;

then A4: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, Th9;

A5: F . 1 = halt SCM by A1, Th3;

hence F halts_on s by A4, EXTPRO_1:30; :: thesis: ( LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

thus LifeSpan (F,s) = 1 by A5, A2, A4, EXTPRO_1:33; :: thesis: for d being Data-Location holds (Result (F,s)) . d = s . d

let d be Data-Location; :: thesis: (Result (F,s)) . d = s . d

thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A5, A4, EXTPRO_1:7

.= s . d by A3, A2, Th9 ; :: thesis: verum