:: Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users


begin

registration
let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of N;
let i be Element of the Instructions of S;
let s be State of S;
cluster ( the Execution of S . i) . s -> Relation-like Function-like ;
coherence
( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like )
proof end;
end;

theorem :: AMISTD_1:1
canceled;

theorem :: AMISTD_1:2
canceled;

theorem :: AMISTD_1:3
canceled;

theorem :: AMISTD_1:4
canceled;

theorem :: AMISTD_1:5
canceled;

theorem :: AMISTD_1:6
canceled;

theorem :: AMISTD_1:7
canceled;

theorem :: AMISTD_1:8
canceled;

theorem :: AMISTD_1:9
canceled;

theorem :: AMISTD_1:10
canceled;

theorem :: AMISTD_1:11
canceled;

theorem :: AMISTD_1:12
canceled;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of N;
let T be InsType of S;
canceled;
canceled;
attr T is jump-only means :: AMISTD_1:def 3
 for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o in Data-Locations S holds
(Exec (I,s)) . o = s . o;
end;

:: deftheorem AMISTD_1:def 1 :
canceled;

:: deftheorem AMISTD_1:def 2 :
canceled;

:: deftheorem defines jump-only AMISTD_1:def 3 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of N
for T being InsType of S holds
( T is jump-only iff for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o in Data-Locations S holds
(Exec (I,s)) . o = s . o );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of N;
let I be Instruction of S;
attr I is jump-only means :: AMISTD_1:def 4
 InsCode I is jump-only ;
end;

:: deftheorem defines jump-only AMISTD_1:def 4 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of N
for I being Instruction of S holds
( I is jump-only iff InsCode I is jump-only );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let l be Nat;
let i be Element of the Instructions of S;
func NIC (i,l) -> Subset of NAT equals :: AMISTD_1:def 5
 { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = l } ;
coherence
{ (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = l } is Subset of NAT
proof end;
end;

:: deftheorem defines NIC AMISTD_1:def 5 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for l being Nat
for i being Element of the Instructions of S holds NIC (i,l) = { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = l } ;

Lm1: now
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for i being Element of the Instructions of S
for l being Element of NAT
for s being State of S
for P being the Instructions of b1 -valued ManySortedSet of NAT holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for i being Element of the Instructions of S
for l being Element of NAT
for s being State of S
for P being the Instructions of S -valued ManySortedSet of NAT holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let i be Element of the Instructions of S; :: thesis: for l being Element of NAT
for s being State of S
for P being the Instructions of S -valued ManySortedSet of NAT holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let l be Element of NAT ; :: thesis: for s being State of S
for P being the Instructions of S -valued ManySortedSet of NAT holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let s be State of S; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
reconsider t = s +* ((IC ),l) as Element of product the Object-Kind of S by PBOOLE:155;
l in NAT ;
then A1: l in dom P by PARTFUN1:def 4;
IC in dom s by COMPOS_1:9;
then A4: IC t = l by FUNCT_7:33;
then CurInstr ((P +* (l,i)),t) = (P +* (l,i)) . l by PBOOLE:158
.= i by A1, FUNCT_7:33 ;
hence IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) by A4; :: thesis: verum
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N;
let i be Element of the Instructions of S;
let l be Element of NAT ;
cluster NIC (i,l) -> non empty ;
coherence
not NIC (i,l) is empty by Lm1;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let i be Element of the Instructions of S;
func JUMP i -> Subset of NAT equals :: AMISTD_1:def 6
 meet { (NIC (i,l)) where l is Element of NAT : verum } ;
coherence
meet { (NIC (i,l)) where l is Element of NAT : verum } is Subset of NAT
proof end;
end;

:: deftheorem defines JUMP AMISTD_1:def 6 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Element of the Instructions of S holds JUMP i = meet { (NIC (i,l)) where l is Element of NAT : verum } ;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let l be Nat;
func SUCC (l,S) -> Subset of NAT equals :: AMISTD_1:def 7
 union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the Instructions of S : verum } ;
coherence
union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the Instructions of S : verum } is Subset of NAT
proof end;
end;

:: deftheorem defines SUCC AMISTD_1:def 7 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for l being Nat holds SUCC (l,S) = union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the Instructions of S : verum } ;

theorem :: AMISTD_1:13
canceled;

theorem Th14: :: AMISTD_1:14
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Element of the Instructions of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds
JUMP i is empty
proof end;

theorem Th15: :: AMISTD_1:15
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is halting holds
NIC (i,il) = {il}
proof end;

begin

definition
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
attr S is standard means :Def10: :: AMISTD_1:def 10
 for m, n being Element of NAT holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) );
end;

:: deftheorem AMISTD_1:def 8 :
canceled;

:: deftheorem AMISTD_1:def 9 :
canceled;

:: deftheorem Def10 defines standard AMISTD_1:def 10 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is standard iff for m, n being Element of NAT holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) ) );

Lm2: for k being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
proof end;

theorem :: AMISTD_1:16
canceled;

theorem :: AMISTD_1:17
canceled;

theorem :: AMISTD_1:18
canceled;

theorem Th19: :: AMISTD_1:19
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is standard iff for k being Element of NAT holds
( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds
k <= j ) ) )
proof end;

Lm3: for a, b being set holds dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT}
proof end;

set III = {[1,0,0],[0,0,0]};

begin

definition
let N be with_non-empty_elements set ;
func STC N -> strict AMI-Struct of N means :Def11: :: AMISTD_1:def 11
( the carrier of it = NAT \/ {NAT} & the ZeroF of it = NAT & the Instructions of it = {[0,0,0],[1,0,0]} & the haltF of it = [0,0,0] & the Object-Kind of it = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) & ex f being Function of (product the Object-Kind of it),(product the Object-Kind of it) st
( ( for s being Element of product the Object-Kind of it holds f . s = s +* (NAT .--> (succ (s . NAT))) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it))) ) );
existence
ex b1 being strict AMI-Struct of N st
( the carrier of b1 = NAT \/ {NAT} & the ZeroF of b1 = NAT & the Instructions of b1 = {[0,0,0],[1,0,0]} & the haltF of b1 = [0,0,0] & the Object-Kind of b1 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) & ex f being Function of (product the Object-Kind of b1),(product the Object-Kind of b1) st
( ( for s being Element of product the Object-Kind of b1 holds f . s = s +* (NAT .--> (succ (s . NAT))) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of b1))) ) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of N st the carrier of b1 = NAT \/ {NAT} & the ZeroF of b1 = NAT & the Instructions of b1 = {[0,0,0],[1,0,0]} & the haltF of b1 = [0,0,0] & the Object-Kind of b1 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) & ex f being Function of (product the Object-Kind of b1),(product the Object-Kind of b1) st
( ( for s being Element of product the Object-Kind of b1 holds f . s = s +* (NAT .--> (succ (s . NAT))) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of b1))) ) & the carrier of b2 = NAT \/ {NAT} & the ZeroF of b2 = NAT & the Instructions of b2 = {[0,0,0],[1,0,0]} & the haltF of b2 = [0,0,0] & the Object-Kind of b2 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) & ex f being Function of (product the Object-Kind of b2),(product the Object-Kind of b2) st
( ( for s being Element of product the Object-Kind of b2 holds f . s = s +* (NAT .--> (succ (s . NAT))) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of b2))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines STC AMISTD_1:def 11 :
for N being with_non-empty_elements set
for b2 being strict AMI-Struct of N holds
( b2 = STC N iff ( the carrier of b2 = NAT \/ {NAT} & the ZeroF of b2 = NAT & the Instructions of b2 = {[0,0,0],[1,0,0]} & the haltF of b2 = [0,0,0] & the Object-Kind of b2 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) & ex f being Function of (product the Object-Kind of b2),(product the Object-Kind of b2) st
( ( for s being Element of product the Object-Kind of b2 holds f . s = s +* (NAT .--> (succ (s . NAT))) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of b2))) ) ) );

registration
let N be with_non-empty_elements set ;
cluster STC N -> infinite strict ;
coherence
not STC N is finite
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster STC N -> non empty stored-program standard-ins strict ;
coherence
( not STC N is empty & STC N is stored-program & STC N is standard-ins )
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster STC N -> IC-Ins-separated definite realistic strict ;
coherence
( STC N is IC-Ins-separated & STC N is definite & STC N is realistic )
proof end;
end;

Lm4: for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = succ (IC s)
proof end;

theorem Th20: :: AMISTD_1:20
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N) st InsCode i = 0 holds
i is halting
proof end;

theorem :: AMISTD_1:21
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N) st InsCode i = 1 holds
not i is halting
proof end;

theorem Th22: :: AMISTD_1:22
for N being non empty with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )
proof end;

theorem :: AMISTD_1:23
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N) holds i is jump-only
proof end;

registration
let N be non empty with_non-empty_elements set ;
cluster -> ins-loc-free Element of the Instructions of (STC N);
coherence
for b1 being Instruction of (STC N) holds b1 is ins-loc-free
proof end;
end;

Lm5: for z being natural number
for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
proof end;

Lm6: for N being non empty with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds JUMP i is empty
proof end;

theorem Th24: :: AMISTD_1:24
for z being natural number
for N being non empty with_non-empty_elements set
for l being Element of NAT st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}
proof end;

registration
let N be non empty with_non-empty_elements set ;
cluster STC N -> strict standard ;
coherence
STC N is standard
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster STC N -> strict halting ;
coherence
STC N is halting
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard AMI-Struct of N;
existence
ex b1 being non empty stored-program IC-Ins-separated definite AMI-Struct of N st
( b1 is standard & b1 is halting & b1 is realistic & b1 is standard-ins )
proof end;
end;

theorem :: AMISTD_1:25
canceled;

theorem :: AMISTD_1:26
canceled;

theorem :: AMISTD_1:27
canceled;

theorem :: AMISTD_1:28
canceled;

theorem :: AMISTD_1:29
canceled;

theorem :: AMISTD_1:30
canceled;

theorem :: AMISTD_1:31
canceled;

theorem :: AMISTD_1:32
canceled;

theorem :: AMISTD_1:33
canceled;

theorem :: AMISTD_1:34
canceled;

theorem :: AMISTD_1:35
canceled;

theorem :: AMISTD_1:36
canceled;

theorem :: AMISTD_1:37
canceled;

theorem :: AMISTD_1:38
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = succ (IC s) by Lm4;

theorem :: AMISTD_1:39
for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(succ l)} by Lm5;

theorem :: AMISTD_1:40
for N being non empty with_non-empty_elements set
for l being Element of NAT holds SUCC (l,(STC N)) = {l,(succ l)} by Th24;

definition
canceled;
canceled;
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let i be Instruction of S;
attr i is sequential means :: AMISTD_1:def 16
 for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s);
end;

:: deftheorem AMISTD_1:def 12 :
canceled;

:: deftheorem AMISTD_1:def 13 :
canceled;

:: deftheorem AMISTD_1:def 14 :
canceled;

:: deftheorem AMISTD_1:def 15 :
canceled;

:: deftheorem defines sequential AMISTD_1:def 16 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Instruction of S holds
( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) );

theorem Th41: :: AMISTD_1:41
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(succ il)}
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N;
cluster sequential -> non halting Element of the Instructions of S;
coherence
for b1 being Instruction of S st b1 is sequential holds
not b1 is halting
proof end;
cluster halting -> non sequential Element of the Instructions of S;
coherence
for b1 being Instruction of S st b1 is halting holds
not b1 is sequential ;
end;

theorem :: AMISTD_1:42
canceled;

theorem :: AMISTD_1:43
for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Instruction of T st not JUMP i is empty holds
not i is sequential
proof end;

begin

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued FinPartState of ;
attr F is closed means :Def17: :: AMISTD_1:def 17
 for l being Element of NAT st l in dom F holds
NIC ((F /. l),l) c= dom F;
attr F is really-closed means :: AMISTD_1:def 18
 for s being State of S st IC s in dom F holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F;
end;

:: deftheorem Def17 defines closed AMISTD_1:def 17 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued FinPartState of holds
( F is closed iff for l being Element of NAT st l in dom F holds
NIC ((F /. l),l) c= dom F );

:: deftheorem defines really-closed AMISTD_1:def 18 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued FinPartState of holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued Function;
attr F is para-closed means :: AMISTD_1:def 19
 for s being State of S st IC s = 0 holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F;
end;

:: deftheorem defines para-closed AMISTD_1:def 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued Function holds
( F is para-closed iff for s being State of S st IC s = 0 holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F );

theorem Th44: :: AMISTD_1:44
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued FinPartState of st F is really-closed & 0 in dom F holds
F is para-closed
proof end;

theorem Th45: :: AMISTD_1:45
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued FinPartState of st F is closed holds
F is really-closed
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite closed -> NAT -defined the Instructions of S -valued really-closed set ;
coherence
for b1 being NAT -defined the Instructions of S -valued FinPartState of st b1 is closed holds
b1 is really-closed by Th45;
end;

theorem Th46: :: AMISTD_1:46
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N holds 0 .--> (halt S) is closed
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued non empty Function-like the Object-Kind of S -compatible finite initial really-closed -> NAT -defined the Instructions of S -valued para-closed set ;
coherence
for b1 being NAT -defined the Instructions of S -valued FinPartState of st b1 is really-closed & b1 is initial & not b1 is empty holds
b1 is para-closed
proof end;
end;

Lm7: now
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds
( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
let S be non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N; :: thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
set F = <%(halt S)%>;
A1: dom <%(halt S)%> = {0} by FUNCOP_1:19;
then A2: card (dom <%(halt S)%>) = 1 by CARD_1:50;
A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:74
.= 0 by A2, XREAL_1:234 ;
hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:87; :: thesis: for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%>
let l be Element of NAT ; :: thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume <%(halt S)%> . l = halt S ; :: thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume l in dom <%(halt S)%> ; :: thesis: l = LastLoc <%(halt S)%>
hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis: verum
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued non empty trivial Function-like the Object-Kind of S -compatible finite countable initial V137() closed set ;
existence
ex b1 being NAT -defined the Instructions of S -valued FinPartState of st
( b1 is trivial & b1 is closed & b1 is initial & not b1 is empty )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued T-Sequence-like non empty trivial Function-like the Object-Kind of S -compatible finite countable initial halt-ending unique-halt V137() closed set ;
existence
ex b1 being NAT -defined the Instructions of S -valued non empty initial FinPartState of st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial & b1 is closed )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued T-Sequence-like non empty Function-like the Object-Kind of S -compatible finite countable initial halt-ending unique-halt V137() closed set ;
existence
ex b1 being pre-Macro of S st b1 is closed
proof end;
end;

theorem :: AMISTD_1:47
canceled;

theorem :: AMISTD_1:48
canceled;

theorem :: AMISTD_1:49
canceled;

theorem :: AMISTD_1:50
canceled;

theorem :: AMISTD_1:51
canceled;

theorem :: AMISTD_1:52
canceled;

theorem :: AMISTD_1:53
canceled;

theorem :: AMISTD_1:54
canceled;

theorem :: AMISTD_1:55
canceled;

theorem :: AMISTD_1:56
for N being non empty with_non-empty_elements set
for i being Instruction of (Trivial-AMI N) holds i is halting
proof end;

theorem :: AMISTD_1:57
for N being non empty with_non-empty_elements set
for i being Element of the Instructions of (Trivial-AMI N) holds InsCode i = 0
proof end;

begin

theorem :: AMISTD_1:58
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Instruction of S
for l being Element of NAT holds JUMP i c= NIC (i,l)
proof end;

theorem :: AMISTD_1:59
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
Exec (i,s) = IncIC (s,1)
proof end;

registration
let N be non empty with_non-empty_elements set ;
let p be PartState of (STC N);
cluster DataPart p -> empty ;
coherence
DataPart p is empty
proof end;
end;