:: AMISTD_1 semantic presentation

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 Th11: :: AMISTD_1:11
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program definite AMI-Struct of IL,N
for I being Element of the Instructions of S
for s being State of S holds s +* (IL --> I) is State of S
proof end;

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty -> programmed Element of sproduct the Object-Kind of S;
coherence
for b1 being FinPartState of S st b1 is empty holds
b1 is programmed
proof end;
end;

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st b1 is empty
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
cluster non empty trivial programmed Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st
( not b1 is empty & b1 is trivial & b1 is programmed )
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of IL,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;

Lm1: for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
proof end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N;
cluster non empty trivial autonomic programmed Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st
( not b1 is empty & b1 is trivial & b1 is autonomic & b1 is programmed )
proof end;
end;

theorem :: AMISTD_1:12
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S holds il .--> I is autonomic by Lm1;

theorem Th13: :: AMISTD_1:13
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N holds S is programmable
proof end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated steady-programmed definite -> non empty stored-program IC-Ins-separated definite programmable AMI-Struct of IL,N;
coherence
for b1 being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N st b1 is steady-programmed holds
b1 is programmable by Th13;
end;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
mode IL-Subset of S -> Subset of IL means :Def1: :: AMISTD_1:def 1
verum;
existence
ex b1 being Subset of IL st verum ;
end;

:: deftheorem Def1 defines IL-Subset AMISTD_1:def 1 :
for IL, N being set
for S being AMI-Struct of IL,N
for b4 being Subset of IL holds
( b4 is IL-Subset of S iff verum );

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty IL-Subset of S;
existence
ex b1 being IL-Subset of S st b1 is empty
proof end;
end;

registration
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
cluster non empty IL-Subset of S;
existence
not for b1 being IL-Subset of S holds b1 is empty
proof end;
end;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of IL,N;
let T be InsType of S;
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 <> IC S holds
(Exec I,s) . o = s . o;
end;

:: deftheorem AMISTD_1:def 2 :
canceled;

:: deftheorem defines jump-only AMISTD_1:def 3 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of IL,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 <> IC S holds
(Exec I,s) . o = s . o );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is jump-only iff InsCode I is jump-only );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l be Instruction-Location of S;
let i be Element of the Instructions of S;
func NIC i,l -> IL-Subset of S equals :: AMISTD_1:def 5
{ (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } ;
coherence
{ (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } is IL-Subset of S
proof end;
end;

:: deftheorem defines NIC AMISTD_1:def 5 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l being Instruction-Location of S
for i being Element of the Instructions of S holds NIC i,l = { (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } ;

Lm2: now
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N;
let i be Element of the Instructions of S;
let l be Instruction-Location of S;
let s be State of S;
let f be FinPartState of S;
assume A1: f = (IC S),l --> l,i ;
set t = s +* f;
A2: IC S <> l by AMI_1:48;
A3: dom f = {(IC S),l} by A1, FUNCT_4:65;
then IC S in dom f by TARSKI:def 2;
then A4: IC (s +* f) = f . (IC S) by FUNCT_4:14
.= l by A1, A2, FUNCT_4:66 ;
l in dom f by A3, TARSKI:def 2;
then (s +* f) . l = f . l by FUNCT_4:14
.= i by A1, FUNCT_4:66 ;
hence IC (Following (s +* f)) in NIC i,l by A4;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N;
let i be Element of the Instructions of S;
let l be Instruction-Location of S;
cluster NIC i,l -> non empty ;
coherence
not NIC i,l is empty
proof end;
end;

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

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

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l be Instruction-Location of S;
func SUCC l -> Subset of IL 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 IL
proof end;
end;

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

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

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

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l1, l2 be Instruction-Location of S;
pred l1 <= l2 means :Def8: :: AMISTD_1:def 8
 ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) );
reflexivity
for l1 being Instruction-Location of S ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l1 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) )
proof end;
end;

:: deftheorem Def8 defines <= AMISTD_1:def 8 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l1, l2 being Instruction-Location of S holds
( l1 <= l2 iff ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) ) );

theorem :: AMISTD_1:16
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l1, l2, l3 being Instruction-Location of S st l1 <= l2 & l2 <= l3 holds
l1 <= l3
proof end;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
attr S is InsLoc-antisymmetric means :: AMISTD_1:def 9
for l1, l2 being Instruction-Location of S st l1 <= l2 & l2 <= l1 holds
l1 = l2;
end;

:: deftheorem defines InsLoc-antisymmetric AMISTD_1:def 9 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( S is InsLoc-antisymmetric iff for l1, l2 being Instruction-Location of S st l1 <= l2 & l2 <= l1 holds
l1 = l2 );

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

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

theorem Th17: :: AMISTD_1:17
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for f1, f2 being IL-Function of NAT ,S st f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) ) & f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n ) ) holds
f1 = f2
proof end;

theorem Th18: :: AMISTD_1:18
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for f being IL-Function of NAT ,S st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) )
proof end;

theorem Th19: :: AMISTD_1:19
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( S is standard iff ex f being IL-Function of NAT ,S st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) 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 ]};

definition
let N be with_non-empty_elements set ;
func STC N -> strict AMI-Struct of NAT ,N means :Def11: :: AMISTD_1:def 11
( the carrier of it = NAT \/ {NAT } & the Instruction-Counter of it = NAT & the Instructions of it = {[0 ,0 ],[1,0 ]} & the Object-Kind of it = (NAT --> {[1,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 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of it))) ) );
existence
ex b1 being strict AMI-Struct of NAT ,N st
( the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b1 = (NAT --> {[1,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 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b1))) ) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of NAT ,N st the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b1 = (NAT --> {[1,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 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b1))) ) & the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b2 = (NAT --> {[1,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 ] .--> f) +* ([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 NAT ,N holds
( b2 = STC N iff ( the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b2 = (NAT --> {[1,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 ] .--> f) +* ([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