:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, SETFAM_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1,
AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1,
FUNCT_1, CARD_3, FRECHET, STRUCT_0, FSM_1, FUNCT_4, TURING_1, CIRCUIT2,
AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, XXREAL_0, COMPOS_1, QUANTAL1,
GOBRD13, MEMSTR_0;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D, FUNCT_7,
VALUED_0, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1,
MEASURE6, EXTPRO_1, AMISTD_1;
constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY,
AFINSQ_1, ORDINAL4, VALUED_1, NAT_1, FUNCT_7, PBOOLE, FUNCT_4, MEMSTR_0,
RELSET_1, MEASURE6, XTUPLE_0;
registrations RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED,
CARD_3, STRUCT_0, AMISTD_1, FUNCT_4, EXTPRO_1, MEMSTR_0, MEASURE6,
COMPOS_0, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions AMISTD_1, XBOOLE_0, TARSKI, COMPOS_0;
equalities COMPOS_1, EXTPRO_1, AMISTD_1, XBOOLE_0, FUNCOP_1, VALUED_1,
MEMSTR_0, COMPOS_0, XTUPLE_0;
expansions AMISTD_1, XBOOLE_0;
theorems AMISTD_1, FUNCOP_1, FUNCT_1, FUNCT_4, GRFUNC_1, MCART_1, SETFAM_1,
TARSKI, CARD_3, XBOOLE_0, PARTFUN1, VALUED_1, COMPOS_1, EXTPRO_1,
ORDINAL1, NAT_1, MEMSTR_0, COMPOS_0;
schemes NAT_1;
begin :: Properties of AMI-Struct
reserve k, m for Nat,
x, x1, x2, x3, y, y1, y2, y3, X,Y,Z for set,
N for with_zero set;
theorem
for I being Instruction of STC N holds JumpPart I = 0;
definition
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I be Instruction of S;
attr I is with_explicit_jumps means
:Def1: JUMP I = rng JumpPart I;
end;
definition
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is with_explicit_jumps means
:Def2: for I being Instruction of S holds I is with_explicit_jumps;
end;
registration
let N be with_zero set;
cluster standard for IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
theorem Th2:
for S being standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I being Instruction of S
st for f being Element of NAT holds NIC(I,f)={f+1}
holds JUMP I is empty
proof
let S be standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I be Instruction of S;
assume
A1: for f being Element of NAT holds NIC(I,f)={f+1};
set p=1, q=2;
reconsider p,q as Element of NAT;
set X = the set of all NIC(I,f) where f is Nat;
assume not thesis;
then consider x being object such that
A2: x in meet X;
A3: NIC(I,p) = {p+1} by A1;
A4: NIC(I,q) = {q+1} by A1;
A5: {succ p} in X by A3;
A6: {succ q} in X by A4;
A7: x in {succ p} by A2,A5,SETFAM_1:def 1;
A8: x in {succ q} by A2,A6,SETFAM_1:def 1;
x = succ p by A7,TARSKI:def 1;
hence contradiction by A8,TARSKI:def 1;
end;
registration
let N be with_zero set,
I be Instruction of STC N;
cluster JUMP I -> empty;
coherence
proof
per cases by AMISTD_1:6;
suppose InsCode I = 0;
then for f being Nat holds NIC(I,f)={f} by AMISTD_1:2,4;
hence thesis by AMISTD_1:1;
end;
suppose InsCode I = 1;
then for f being Element of NAT holds NIC(I,f)={f+1} by AMISTD_1:10;
hence thesis by Th2;
end;
end;
end;
theorem
for T being InsType of the InstructionsF of STC N holds JumpParts T = {0}
proof
let T be InsType of the InstructionsF of STC N;
set A = { JumpPart I where I is Instruction of STC N: InsCode I = T };
{0} = A
proof
hereby
let a be object;
assume a in {0};
then
A1: a = 0 by TARSKI:def 1;
A2: the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then
A3: InsCodes the InstructionsF of STC N = {0,1} by MCART_1:91;
per cases by A3,TARSKI:def 2;
suppose
A4: T = 0;
reconsider I = [0,0,0] as Instruction of STC N by A2,TARSKI:def 2;
A5: JumpPart I = 0;
InsCode I = 0;
hence a in A by A1,A4,A5;
end;
suppose
A6: T = 1;
reconsider I = [1,0,0] as Instruction of STC N by A2,TARSKI:def 2;
A7: JumpPart I = 0;
InsCode I = 1;
hence a in A by A1,A6,A7;
end;
end;
let a be object;
assume a in A;
then ex I being Instruction of STC N st a = JumpPart I & InsCode I = T;
then a = 0;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
Lm1: for I being Instruction of Trivial-AMI N holds JumpPart I = 0
proof
let I be Instruction of Trivial-AMI N;
the InstructionsF of Trivial-AMI N = {[0,0,{}]} by EXTPRO_1:def 1;
then I = [0,0,0] by TARSKI:def 1;
hence thesis;
end;
Lm2: for T being InsType of the InstructionsF of Trivial-AMI N
holds JumpParts T = {0}
proof
let T be InsType of the InstructionsF of Trivial-AMI N;
set A =
{ JumpPart I where I is Instruction of Trivial-AMI N: InsCode I = T };
{0} = A
proof
hereby
let a be object;
assume a in {0};
then
A1: a = 0 by TARSKI:def 1;
A2: the InstructionsF of Trivial-AMI N = {[0,0,{}]} by EXTPRO_1:def 1;
then InsCodes the InstructionsF of Trivial-AMI N = {0} by MCART_1:92;
then
A3: T = 0 by TARSKI:def 1;
reconsider I = [0,0,0] as Instruction of Trivial-AMI N
by A2,TARSKI:def 1;
A4: JumpPart I = 0;
InsCode I = 0;
hence a in A by A1,A3,A4;
end;
let a be object;
assume a in A;
then ex I being Instruction of Trivial-AMI N
st a = JumpPart I & InsCode I = T;
then a = 0 by Lm1;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
registration
let N be with_zero set;
cluster STC N -> with_explicit_jumps;
coherence
proof
let I be Instruction of STC N;
thus JUMP I = rng JumpPart I;
end;
end;
registration
let N be with_zero set;
cluster standard
halting with_explicit_jumps for IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_zero set,
I be Instruction of Trivial-AMI N;
cluster JUMP I -> empty;
coherence
proof
for f being Nat holds NIC(I,f)={f} by AMISTD_1:2,17;
hence thesis by AMISTD_1:1;
end;
end;
registration
let N be with_zero set;
cluster Trivial-AMI N -> with_explicit_jumps;
coherence
proof
thus Trivial-AMI N is with_explicit_jumps
proof
let I be Instruction of Trivial-AMI N;
the InstructionsF of Trivial-AMI N = {[0,0,{}]} by EXTPRO_1:def 1;
then I = [0,0,0] by TARSKI:def 1;
hence JUMP I = rng JumpPart I;
end;
end;
end;
registration
let N be with_zero set;
cluster with_explicit_jumps halting
for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
registration
let N be with_zero set;
let S be with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster -> with_explicit_jumps for Instruction of S;
coherence by Def2;
end;
theorem Th4:
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
I being Instruction of S st I is halting holds JUMP I is empty
proof
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I be Instruction of S;
assume I is halting;
then for l being Nat holds NIC(I,l)={l} by AMISTD_1:2;
hence thesis by AMISTD_1:1;
end;
registration
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
I be halting Instruction of S;
cluster JUMP I -> empty;
coherence by Th4;
end;
theorem
for S being halting with_explicit_jumps
IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
I being Instruction of S st I is ins-loc-free holds JUMP I is empty
proof
let S be halting with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I be Instruction of S such that
A1: JumpPart I is empty;
A2: rng JumpPart I = {} by A1;
JUMP I c= rng JumpPart I by Def1;
hence thesis by A2;
end;
registration
let N be with_zero set,
S be with_explicit_jumps
IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster halting -> ins-loc-free for Instruction of S;
coherence
proof
let I be Instruction of S;
assume I is halting;
then
A1: JUMP I is empty by Th4;
rng JumpPart I = JUMP I by Def1;
hence JumpPart I is empty by A1;
end;
end;
registration
let N be with_zero set,
S be with_explicit_jumps
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> ins-loc-free for Instruction of S;
coherence
proof
let I be Instruction of S;
assume I is sequential;
then
A1: JUMP I is empty by AMISTD_1:13;
rng JumpPart I = JUMP I by Def1;
hence JumpPart I is empty by A1;
end;
end;
begin :: On the composition of macro instructions
registration
let N be with_zero set,
S be halting with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I be halting Instruction of S, k be Nat;
cluster IncAddr(I,k) -> halting;
coherence by COMPOS_0:4;
end;
theorem
for S being standard halting
with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I being Instruction of S st I is sequential
holds IncAddr(I,k) is sequential by COMPOS_0:4;
definition
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
I be Instruction of S;
attr I is IC-relocable means
:Def3:
for j,k being Nat, s being State of S
holds IC Exec(IncAddr(I,j),s) + k = IC Exec(IncAddr(I,j+k),IncIC(s,k));
end;
definition
let N be with_zero set,
S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is IC-relocable means
:Def4:
for I being Instruction of S holds I is IC-relocable;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> IC-relocable for Instruction of S;
coherence
proof
let I be Instruction of S such that
A1: I is sequential;
let j,k be Nat, s1 be State of S;
set s2 = IncIC(s1,k);
IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
then
A2: IC s2 = (IC S .--> (IC s1 + k)).IC S by FUNCT_4:13
.= IC s1 + k by FUNCOP_1:72;
A3: IC Exec(I, s2) = IC s2 + 1 by A1
.= IC s1 + 1 + k by A2;
A4: IncAddr(I,j) = I by A1,COMPOS_0:4;
IC Exec(I,s1) = IC s1 + 1 by A1;
hence IC Exec(IncAddr(I,j),s1) + k
= IC Exec(IncAddr(I,j+k), s2) by A1,A3,A4,COMPOS_0:4;
end;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster halting -> IC-relocable for Instruction of S;
coherence
proof
let I be Instruction of S such that
A1: I is halting;
let j,k be Nat, s1 be State of S;
set s2 = IncIC(s1,k);
A2: IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
thus IC Exec(IncAddr(I,j),s1) + k = IC s1 + k by A1,EXTPRO_1:def 3
.= (IC S .--> (IC s1 + k)).IC S by FUNCOP_1:72
.= IC s2 by A2,FUNCT_4:13
.= IC Exec(IncAddr(I,j+k), s2) by A1,EXTPRO_1:def 3;
end;
end;
registration
let N be with_zero set;
cluster STC N -> IC-relocable;
coherence
proof
thus STC N is IC-relocable
proof
let I be Instruction of STC N, j,k be Nat,
s1 be State of STC N;
set s2 = IncIC(s1,k);
IC STC N in dom (IC STC N .--> (IC s1 + k)) by TARSKI:def 1;
then
A1: IC s2 = (IC STC N .--> (IC s1 + k)).IC STC N by FUNCT_4:13
.= IC s1 + k by FUNCOP_1:72;
per cases by AMISTD_1:6;
suppose
A2: InsCode I = 1;
then
A3: InsCode IncAddr(I,k) = 1 by COMPOS_0:def 9;
A4: IncAddr(I,j) = I by COMPOS_0:4;
IC Exec(I,s1) = IC s1 + 1 by A2,AMISTD_1:9;
hence IC Exec(IncAddr(I,j),s1) + k = IC s2 + 1 by A1,A4
.= IC Exec(IncAddr(IncAddr(I,j),k), s2) by A4,A3,AMISTD_1:9
.= IC Exec(IncAddr(I,j+k), s2) by COMPOS_0:7;
end;
suppose InsCode I = 0;
then
A5: I is halting by AMISTD_1:4;
hence IC Exec(IncAddr(I,j),s1) + k = IC s1 + k by EXTPRO_1:def 3
.= IC Exec(IncAddr(I,j+k), s2) by A1,A5,EXTPRO_1:def 3;
end;
end;
end;
end;
registration
let N be with_zero set;
cluster halting with_explicit_jumps
for standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_zero set;
cluster IC-relocable for
with_explicit_jumps halting
standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_zero set,
S be IC-relocable IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster -> IC-relocable for Instruction of S;
coherence by Def4;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster IC-relocable for Instruction of S;
existence
proof
take the halting Instruction of S;
thus thesis;
end;
end;
theorem Th7:
for S be halting
with_explicit_jumps
IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
I being IC-relocable Instruction of S
for k being Nat, s being State of S
holds IC Exec(I,s) + k = IC Exec(IncAddr(I,k),IncIC(s,k))
proof
let S be halting
with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I being IC-relocable Instruction of S;
let k being Nat, s being State of S;
A1: k+(0 qua Nat)=k;
thus IC Exec(I,s) + k
= IC Exec(IncAddr(I,0),s) + k by COMPOS_0:3
.= IC Exec(IncAddr(I,k),IncIC(s,k)) by Def3,A1;
end;
registration
let N be with_zero set,
S be IC-relocable standard with_explicit_jumps
halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
F, G be really-closed Program of S;
cluster F ';' G -> really-closed;
coherence
proof
set P = F ';' G, k = card F -' 1;
let f be Nat such that
A1: f in dom P;
A2: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A3: dom CutLastLoc F c= dom F by GRFUNC_1:2;
A4: dom Reloc(G,k) =
{(m+k) where m is Nat: m in dom IncAddr(G,k)}
by VALUED_1:def 12;
let x be object;
assume x in NIC(P/.f,f);
then consider s2 being Element of product the_Values_of S
such that
A5: x = IC Exec(P/.f,s2) and
A6: IC s2 = f;
A7: P/.f = P.f by A1,PARTFUN1:def 6;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
A8: f in dom CutLastLoc F;
then
A9: NIC(F/.f,f) c= dom F by A3,AMISTD_1:def 9;
dom CutLastLoc F = dom F \ {LastLoc F} by VALUED_1:36;
then
A10: f in dom F by A8;
dom CutLastLoc F misses dom Reloc(G,card F -' 1)
by COMPOS_1:18;
then
A11: not f in dom Reloc(G,card F -' 1)
by A8,XBOOLE_0:3;
A12: P/.f = P.f by A1,PARTFUN1:def 6
.= (CutLastLoc F).f by A11,FUNCT_4:11
.= F.f by A8,GRFUNC_1:2
.= F/.f by A10,PARTFUN1:def 6;
IC Exec(F/.f,s2) in NIC(F/.f,f) by A6;
then
A13: x in dom F by A5,A9,A12;
dom F c= dom P by COMPOS_1:21;
hence thesis by A13;
end;
suppose
A14: f in dom Reloc(G,k);
then consider m being Nat such that
A15: f = m+k and
A16: m in dom IncAddr(G,k) by A4;
A17: m in dom G by A16,COMPOS_1:def 21;
then
A18: NIC(G/.m,m) c= dom G by AMISTD_1:def 9;
A19: Values IC S = NAT by MEMSTR_0:def 6;
reconsider m as Element of NAT by ORDINAL1:def 12;
reconsider v = IC S .--> m as FinPartState of S by A19;
set s1 = s2 +* v;
A20: P/.f = Reloc(G,k).f by A7,A14,FUNCT_4:13
.= IncAddr(G,k).m by A15,A16,VALUED_1:def 12;
A21: (IC S .--> m).IC S = m by FUNCOP_1:72;
A22: IC S in {IC S} by TARSKI:def 1;
A23: dom (IC S .--> m) = {IC S};
reconsider w = IC S .--> (IC s1 + k) as FinPartState of S by A19;
A24: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by PARTFUN1:def 2;
A25: dom s2 = the carrier of S by PARTFUN1:def 2;
for a being object st a in dom s2 holds
s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
proof
let a be object such that a in dom s2;
A26: dom (IC S .--> (IC s1 + k)) = {IC S};
per cases;
suppose
A27: a = IC S;
hence s2.a = IC s1 + k by A6,A15,A23,A21,A22,FUNCT_4:13
.= (IC S .--> (IC s1 + k)).a by A27,FUNCOP_1:72
.= (s1 +* (IC S .--> (IC s1 + k))).a by A22,A26,A27,FUNCT_4:13;
end;
suppose
A28: a <> IC S;
then
A29: not a in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
not a in dom (IC S .--> m) by A28,TARSKI:def 1;
then s1.a = s2.a by FUNCT_4:11;
hence thesis by A29,FUNCT_4:11;
end;
end;
then
A30: s2 = IncIC(s1,k) by A24,A25,FUNCT_1:2;
set s3 = s1;
A31: IC s3 = m by A21,A22,A23,FUNCT_4:13;
reconsider s3 as Element of product the_Values_of S by CARD_3:107;
reconsider k,m as Element of NAT;
A32: x = IC Exec(IncAddr(G/.m,k),s2) by A5,A17,A20,COMPOS_1:def 21
.= IC Exec(G/.m, s3) + k by A30,Th7;
IC Exec(G/.m, s3) in NIC(G/.m,m) by A31;
then IC Exec(G/.m, s3) in dom G by A18;
then IC Exec(G/.m, s3) in dom IncAddr(G,k) by COMPOS_1:def 21;
then x in dom Reloc(G,k) by A4,A32;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
end;
theorem
for I being Instruction of Trivial-AMI N holds JumpPart I = 0 by Lm1;
theorem
for T being InsType of the InstructionsF of Trivial-AMI N
holds JumpParts T = {0} by Lm2;
reserve n,m for Nat;
theorem
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for s being State of S, I being Program of S
for P1,P2 being Instruction-Sequence of S
st I c= P1 & I c= P2 &
for m st m < n holds IC Comput(P2,s,m) in dom I
for m st m <= n holds Comput(P1,s,m) = Comput(P2,s,m)
proof
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
let s be State of S, I be Program of S;
let P1,P2 be Instruction-Sequence of S
such that
A1: I c= P1 & I c= P2;
assume that
A2: for m st m < n holds IC Comput(P2,s,m) in dom I;
defpred X[Nat] means $1 <= n implies
Comput(P1,s,$1) = Comput(P2,s,$1);
A3: for m st X[m] holds X[m+1]
proof
let m such that
A4: X[m];
A5: Comput(P2,s,m+1) = Following(P2,Comput(P2,s,m)) by EXTPRO_1:3
.= Exec(CurInstr(P2,Comput(P2,s,m)),Comput(P2,s,m));
A6: Comput(P1,s,m+1) = Following(P1,Comput(P1,s,m)) by EXTPRO_1:3
.= Exec(CurInstr(P1,Comput(P1,s,m)),Comput(P1,s,m));
assume
A7: m+1 <= n;
then m < n by NAT_1:13;
then
A8: IC Comput(P1,s,m) = IC Comput(P2,s,m) by A4;
m < n by A7,NAT_1:13;
then
A9: IC Comput(P2,s,m) in dom I by A2;
dom P2 = NAT by PARTFUN1:def 2;
then
A10: IC Comput(P2,s,m) in dom P2;
dom P1 = NAT by PARTFUN1:def 2;
then IC Comput(P1,s,m) in dom P1;
then CurInstr(P1,Comput(P1,s,m))
= P1.IC( Comput(P1,s,m)) by PARTFUN1:def 6
.= I.IC( Comput(P1,s,m)) by A9,A8,A1,GRFUNC_1:2
.= P2.IC Comput(P2,s,m) by A9,A8,A1,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s,m)) by A10,PARTFUN1:def 6;
hence thesis by A4,A6,A5,A7,NAT_1:13;
end;
A11: X[0];
thus for m holds X[m] from NAT_1:sch 2(A11,A3);
end;
theorem
for S being IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N,
P being Instruction-Sequence of S,
s being State of S st s = Following(P,s)
holds for n holds Comput(P,s,n) = s
proof
let S be IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N,
P be Instruction-Sequence of S,
s be State of S;
defpred X[Nat] means Comput(P,s,$1) = s;
assume
A1: s = Following(P,s);
A2: for n st X[n] holds X[n+1] by A1,EXTPRO_1:3;
A3: X[ 0];
thus for n holds X[n] from NAT_1:sch 2(A3, A2);
end;