:: AMISTD_2 semantic presentation

registration
let D be set ;
cluster -> functional FinSequenceSet of D;
coherence
for b1 being FinSequenceSet of D holds b1 is functional ;
end;

registration
let i be Element of NAT ;
let D be set ;
cluster i -tuples_on D -> with_common_domain ;
coherence
i -tuples_on D is with_common_domain
proof end;
end;

registration
let i be Element of NAT ;
let D be set ;
cluster i -tuples_on D -> product-like ;
coherence
i -tuples_on D is product-like
proof end;
end;

Lm1: for k being natural number holds - 1 < k
proof end;

Lm2: for k being natural number
for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
proof end;

theorem :: AMISTD_2:1
canceled;

theorem :: AMISTD_2:2
canceled;

theorem :: AMISTD_2:3
canceled;

theorem :: AMISTD_2:4
canceled;

theorem :: AMISTD_2:5
canceled;

theorem :: AMISTD_2:6
canceled;

theorem :: AMISTD_2:7
canceled;

theorem :: AMISTD_2:8
canceled;

theorem :: AMISTD_2:9
canceled;

theorem :: AMISTD_2:10
canceled;

theorem :: AMISTD_2:11
for X, IL, N being set
for S being AMI-Struct of IL,N
for F being FinPartState of S holds F \ X is FinPartState of S by CARD_3:80;

theorem Th12: :: AMISTD_2:12
for X being set
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 programmed FinPartState of S holds F \ X is programmed FinPartState of S
proof end;

definition
let IL be non empty set ;
canceled;
canceled;
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 i1, i2 be Instruction-Location of S;
let I1, I2 be Element of the Instructions of S;
:: original: -->
redefine func i1,i2 --> I1,I2 -> FinPartState of S;
coherence
i1,i2 --> I1,I2 is FinPartState of S
proof end;
end;

:: deftheorem AMISTD_2:def 1 :
canceled;

:: deftheorem AMISTD_2:def 2 :
canceled;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be stored-program halting AMI-Struct of IL,N;
cluster halting Element of the Instructions of S;
existence
ex b1 being Instruction of S st b1 is halting
proof end;
end;

theorem Th13: :: AMISTD_2:13
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S
for G being programmed FinPartState of S st dom F = dom G holds
G is lower
proof end;

theorem Th14: :: AMISTD_2:14
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S
for f being Instruction-Location of S st f in dom F holds
locnum f < card F
proof end;

theorem Th15: :: AMISTD_2:15
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S holds dom F = { (il. S,k) where k is Element of NAT : k < card F }
proof end;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
let I be Element of the Instructions of S;
func AddressPart I -> set equals :: AMISTD_2:def 3
I `2 ;
coherence
I `2 is set ;
end;

:: deftheorem defines AddressPart AMISTD_2:def 3 :
for IL, N being set
for S being AMI-Struct of IL,N
for I being Element of the Instructions of S holds AddressPart I = I `2 ;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let I be Element of the Instructions of S;
:: original: AddressPart
redefine func AddressPart I -> FinSequence of (union N) \/ the carrier of S;
coherence
AddressPart I is FinSequence of (union N) \/ the carrier of S
proof end;
end;

theorem Th16: :: AMISTD_2:16
for IL being non empty set
for N being set
for S being standard-ins AMI-Struct of IL,N
for I, J being Element of the Instructions of S st InsCode I = InsCode J & AddressPart I = AddressPart J holds
I = J
proof end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
attr S is homogeneous means :Def4: :: AMISTD_2:def 4
for I, J being Instruction of S st InsCode I = InsCode J holds
dom (AddressPart I) = dom (AddressPart J);
end;

:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :
for IL, N being set
for S being standard-ins AMI-Struct of IL,N holds
( S is homogeneous iff for I, J being Instruction of S st InsCode I = InsCode J holds
dom (AddressPart I) = dom (AddressPart J) );

theorem Th17: :: AMISTD_2:17
for N being with_non-empty_elements set
for I being Instruction of (STC N) holds AddressPart I = 0
proof end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let T be InsType of S;
func AddressParts T -> set equals :: AMISTD_2:def 5
{ (AddressPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (AddressPart I) where I is Instruction of S : InsCode I = T } is set ;
end;

:: deftheorem defines AddressParts AMISTD_2:def 5 :
for IL, N being set
for S being standard-ins AMI-Struct of IL,N
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let T be InsType of S;
cluster AddressParts T -> functional ;
coherence
AddressParts T is functional
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 standard-ins AMI-Struct of IL,N;
let I be Instruction of S;
attr I is with_explicit_jumps means :Def6: :: AMISTD_2:def 6
for f being set st f in JUMP I holds
ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL );
attr I is without_implicit_jumps means :Def7: :: AMISTD_2:def 7
for f being set st ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) holds
f in JUMP I;
end;

:: deftheorem Def6 defines with_explicit_jumps AMISTD_2: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 standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is with_explicit_jumps iff for f being set st f in JUMP I holds
ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) );

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2: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 standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is without_implicit_jumps iff for f being set st ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) holds
f in JUMP I );

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 standard-ins AMI-Struct of IL,N;
attr S is with_explicit_jumps means :Def8: :: AMISTD_2:def 8
for I being Instruction of S holds I is with_explicit_jumps;
attr S is without_implicit_jumps means :Def9: :: AMISTD_2:def 9
for I being Instruction of S holds I is without_implicit_jumps;
end;

:: deftheorem Def8 defines with_explicit_jumps AMISTD_2: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 standard-ins AMI-Struct of IL,N holds
( S is with_explicit_jumps iff for I being Instruction of S holds I is with_explicit_jumps );

:: deftheorem Def9 defines without_implicit_jumps AMISTD_2: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 standard-ins AMI-Struct of IL,N holds
( S is without_implicit_jumps iff for I being Instruction of S holds I is without_implicit_jumps );

registration
let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard -> non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N;
coherence
for b1 being non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N st b1 is standard holds
verum ;
end;

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

theorem Th18: :: AMISTD_2:18
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for I being Instruction of S st ( for f being Instruction-Location of S holds NIC I,f = {(NextLoc f)} ) holds
JUMP I is empty
proof end;

registration
let N be with_non-empty_elements set ;
let I be Instruction of (STC N);
cluster JUMP I -> empty ;
coherence
JUMP I is empty
proof end;
end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
canceled;
attr S is regular means :Def11: :: AMISTD_2:def 11
for T being InsType of S holds AddressParts T is product-like;
end;

:: deftheorem AMISTD_2:def 10 :
canceled;

:: deftheorem Def11 defines regular AMISTD_2:def 11 :
for IL, N being set
for S being standard-ins AMI-Struct of IL,N holds
( S is regular iff for T being InsType of S holds AddressParts T is product-like );

registration
let IL, N be set ;
cluster standard-ins regular -> standard-ins homogeneous AMI-Struct of IL,N;
coherence
for b1 being standard-ins AMI-Struct of IL,N st b1 is regular holds
b1 is homogeneous
proof end;
end;

theorem Th19: :: AMISTD_2:19
for N being with_non-empty_elements set
for T being InsType of (STC N) holds AddressParts T = {0 }
proof end;

Lm3: for N being with_non-empty_elements set
for IL being non empty set
for I being Instruction of (Trivial-AMI IL,N) holds AddressPart I = 0
proof end;

Lm4: for N being with_non-empty_elements set
for IL being non empty set
for T being InsType of (Trivial-AMI IL,N) holds AddressParts T = {0 }
proof end;

registration
let N be with_non-empty_elements set ;
cluster STC N -> with_explicit_jumps without_implicit_jumps regular ;
coherence
( STC N is with_explicit_jumps & STC N is without_implicit_jumps & STC N is regular )
proof end;
end;

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

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> regular ;
coherence
Trivial-AMI IL,N is regular
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster standard-ins regular AMI-Struct of IL,N;
existence
ex b1 being standard-ins AMI-Struct of IL,N st b1 is regular
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be standard-ins regular AMI-Struct of IL,N;
let T be InsType of S;
cluster AddressParts T -> product-like ;
coherence
AddressParts T is product-like by Def11;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be standard-ins homogeneous AMI-Struct of IL,N;
let T be InsType of S;
cluster AddressParts T -> with_common_domain ;
coherence
AddressParts T is with_common_domain
proof end;
end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
let I be Instruction of (Trivial-AMI IL,N);
cluster JUMP I -> empty ;
coherence
JUMP I is empty
proof end;
end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> with_explicit_jumps without_implicit_jumps regular ;
coherence
( Trivial-AMI IL,N is with_explicit_jumps & Trivial-AMI IL,N is without_implicit_jumps & Trivial-AMI IL,N is regular )
proof end;
end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
cluster non empty stored-program standard-ins regular AMI-Struct of IL,N;
existence
ex b1 being non empty stored-program standard-ins AMI-Struct of IL,N st b1 is regular
proof end;
end;

theorem Th20: :: AMISTD_2:20
for N being with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program standard-ins homogeneous AMI-Struct of IL,N
for I being Instruction of S
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S
proof end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> halting ;
coherence
Trivial-AMI IL,N is halting ;
end;

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

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins with_explicit_jumps AMI-Struct of IL,N;
cluster -> with_explicit_jumps Element of the Instructions of S;
coherence
for b1 being Instruction of S holds b1 is with_explicit_jumps by Def8;
end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins without_implicit_jumps AMI-Struct of IL,N;
cluster -> without_implicit_jumps Element of the Instructions of S;
coherence
for b1 being Instruction of S holds b1 is without_implicit_jumps by Def9;
end;

theorem Th21: :: AMISTD_2:21
for N being with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
JUMP I is empty
proof end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N;
let I be halting Instruction of S;
cluster JUMP I -> empty ;
coherence
JUMP I is empty by Th21;
end;

registration
let IL be non trivial 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 trivial programmed Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st
( not b1 is trivial & b1 is programmed )
proof end;
end;

registration
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster non empty trivial programmed -> non empty programmed unique-halt Element of sproduct the Object-Kind of S;
coherence
for b1 being non empty programmed FinPartState of S st b1 is trivial holds
b1 is unique-halt
proof end;
end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let I be Instruction of S;
attr I is ins-loc-free means :Def12: :: AMISTD_2:def 12
for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> IL;
end;

:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :
for IL, N being set
for S being standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is ins-loc-free iff for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> IL );

theorem :: AMISTD_2:22
for N being with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins with_explicit_jumps AMI-Struct of IL,N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
proof end;

theorem Th23: :: AMISTD_2:23
for N being with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
I is ins-loc-free
proof end;

registration
let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,N;
cluster halting -> ins-loc-free Element of the Instructions of S;
coherence
for b1 being Instruction of S st b1 is halting holds
b1 is ins-loc-free by Th23;
end;

theorem Th24: :: AMISTD_2:24
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of NAT ,N
for I being Instruction of S st I is sequential holds
I is ins-loc-free
proof end;

registration
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of NAT ,N;
cluster sequential -> ins-loc-free Element of the Instructions of S;
coherence
for b1 being Instruction of S st b1 is sequential holds
b1 is ins-loc-free by Th24;
end;

definition
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
func Stop S -> FinPartState of S equals :: AMISTD_2:def 13
(il. S,0 ) .--> (halt S);
coherence
(il. S,0 ) .--> (halt S) is FinPartState of S ;
end;

:: deftheorem defines Stop AMISTD_2:def 13 :
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds Stop S = (il. S,0 ) .--> (halt S);

Lm5: now
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
thus dom (Stop S) = {(il. S,0 )} by FUNCOP_1:19;
hence il. S,0 in dom (Stop S) by TARSKI:def 1;
end;

registration
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster Stop S -> non empty trivial programmed lower ;
coherence
( Stop S is lower & not Stop S is empty & Stop S is programmed & Stop S is trivial ) by AMISTD_1:48;
end;

registration
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N;
cluster Stop S -> closed ;
coherence
Stop S is closed by AMISTD_1:46;
end;

registration
let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite standard AMI-Struct of NAT ,N;
cluster Stop S -> autonomic ;
coherence
Stop S is autonomic by AMISTD_1:12;
end;

theorem Th25: :: AMISTD_2:25
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds card (Stop S) = 1
proof <