:: AMISTD_2 semantic presentation

Lm1: for R being Relation st dom R <> {} holds
R <> {}
by RELAT_1:60;

Lm2: for f, g being Function holds
( dom f, dom g are_equipotent iff f,g are_equipotent )
by PRE_CIRC:26;

Lm3: for f, g being finite Function st dom f misses dom g holds
card (f +* g) = (card f) + (card g)
by PRE_CIRC:27;

registration
let f be Function;
let A be set ;
cluster f \ A -> Relation-like Function-like ;
coherence
( f \ A is Function-like & f \ A is Relation-like ) by GRFUNC_1:38;
end;

theorem :: AMISTD_2:1
canceled;

theorem :: AMISTD_2:2
canceled;

theorem Th3: :: AMISTD_2:3
for x being set
for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
proof end;

Lm4: for F being non empty finite set holds (card F) - 1 = (card F) -' 1
by PRE_CIRC:25;

definition
let S be functional set ;
func PA S -> Function means :Def1: :: AMISTD_2:def 1
( ( for x being set holds
( x in dom it iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom it holds
it . i = pi S,i ) ) if not S is empty
otherwise it = {} ;
existence
( ( not S is empty implies ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b1 holds
b1 . i = pi S,i ) ) ) & ( S is empty implies ex b1 being Function st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Function holds
( ( not S is empty & ( for x being set holds
( x in dom b1 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b1 holds
b1 . i = pi S,i ) & ( for x being set holds
( x in dom b2 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b2 holds
b2 . i = pi S,i ) implies b1 = b2 ) & ( S is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being Function holds verum ;
end;

:: deftheorem Def1 defines PA AMISTD_2:def 1 :
for S being functional set
for b2 being Function holds
( ( not S is empty implies ( b2 = PA S iff ( ( for x being set holds
( x in dom b2 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b2 holds
b2 . i = pi S,i ) ) ) ) & ( S is empty implies ( b2 = PA S iff b2 = {} ) ) );

theorem :: AMISTD_2:4
canceled;

theorem :: AMISTD_2:5
for S being non empty functional set holds dom (PA S) = meet { (dom f) where f is Element of S : verum }
proof end;

theorem :: AMISTD_2:6
for S being non empty functional set
for i being set st i in dom (PA S) holds
(PA S) . i = { (f . i) where f is Element of S : verum }
proof end;

definition
let S be set ;
attr S is product-like means :Def2: :: AMISTD_2:def 2
 ex f being Function st S = product f;
end;

:: deftheorem Def2 defines product-like AMISTD_2:def 2 :
for S being set holds
( S is product-like iff ex f being Function st S = product f );

registration
let f be Function;
cluster product f -> product-like ;
coherence
product f is product-like by Def2;
end;

registration
cluster product-like -> functional with_common_domain set ;
coherence
for b1 being set st b1 is product-like holds
( b1 is functional & b1 is with_common_domain )
proof end;
end;

registration
cluster non empty functional with_common_domain product-like set ;
existence
ex b1 being set st
( b1 is product-like & not b1 is empty )
proof end;
end;

theorem Th7: :: AMISTD_2:7
for S being functional with_common_domain set holds dom (PA S) = DOM S
proof end;

theorem :: AMISTD_2:8
for S being functional set
for i being set st i in dom (PA S) holds
(PA S) . i = pi S,i
proof end;

theorem Th9: :: AMISTD_2:9
for S being functional with_common_domain set holds S c= product (PA S)
proof end;

theorem Th10: :: AMISTD_2:10
for S being non empty product-like set holds S = product (PA S)
proof end;

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

registration
let i be Element of NAT ;
let D be set ;
cluster i -tuples_on D -> functional 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 -> functional with_common_domain product-like ;
coherence
i -tuples_on D is product-like
proof end;
end;

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

Lm6: 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 Th11: :: AMISTD_2:11
for X, N being set
for S being AMI-Struct of N
for F being FinPartState of S holds F \ X is FinPartState of S
proof end;

theorem Th12: :: AMISTD_2:12
for X being set
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for F being programmed FinPartState of S holds F \ X is programmed FinPartState of S
proof end;

definition
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of 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;

registration
let N be with_non-empty_elements set ;
let S be non void halting AMI-Struct of 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 non void IC-Ins-separated definite standard AMI-Struct of 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 non void IC-Ins-separated definite standard AMI-Struct of 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 non void IC-Ins-separated definite standard AMI-Struct of 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 N be set ;
let S be AMI-Struct of 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 N being set
for S being AMI-Struct of N
for I being Element of the Instructions of S holds AddressPart I = I `2 ;

definition
let N be set ;
let S be AMI-Struct of 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 by FINSEQ_1:def 11;
end;

theorem Th16: :: AMISTD_2:16
for N being set
for S being AMI-Struct of 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 N be set ;
let S be AMI-Struct of 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 N being set
for S being AMI-Struct of 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 N be set ;
let S be AMI-Struct of 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 N being set
for S being AMI-Struct of N
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration
let N be set ;
let S be AMI-Struct of N;
let T be InsType of S;
cluster AddressParts T -> functional ;
coherence
AddressParts T is functional
proof end;
end;

definition
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of 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 & (PA (AddressParts (InsCode I))) . k = the Instruction-Locations of S );
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 & (PA (AddressParts (InsCode I))) . k = the Instruction-Locations of S ) holds
f in JUMP I;
end;

:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of 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 & (PA (AddressParts (InsCode I))) . k = the Instruction-Locations of S ) );

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of 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 & (PA (AddressParts (InsCode I))) . k = the Instruction-Locations of S ) holds
f in JUMP I );

definition
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of 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 N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of 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 N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N holds
( S is without_implicit_jumps iff for I being Instruction of S holds I is without_implicit_jumps );

definition
let N be set ;
let S be AMI-Struct of N;
attr S is with-non-trivial-Instruction-Locations means :Def10: :: AMISTD_2:def 10
not the Instruction-Locations of S is trivial;
end;

:: deftheorem Def10 defines with-non-trivial-Instruction-Locations AMISTD_2:def 10 :
for N being set
for S being AMI-Struct of N holds
( S is with-non-trivial-Instruction-Locations iff not the Instruction-Locations of S is trivial );

registration
let N be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated definite standard -> non empty non void IC-Ins-separated definite with-non-trivial-Instruction-Locations AMI-Struct of N;
coherence
for b1 being non empty non void IC-Ins-separated definite AMI-Struct of N st b1 is standard holds
b1 is with-non-trivial-Instruction-Locations
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated definite standard with-non-trivial-Instruction-Locations AMI-Struct of N;
existence
ex b1 being non empty non void IC-Ins-separated definite AMI-Struct of N st b1 is standard
proof end;
end;

registration
let N be with_non-empty_elements set ;
let S be with-non-trivial-Instruction-Locations AMI-Struct of N;
cluster the Instruction-Locations of S -> non trivial ;
coherence
not the Instruction-Locations of S is trivial by Def10;
end;

theorem Th18: :: AMISTD_2:18
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of 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 N be set ;
let S be AMI-Struct of N;
attr S is regular means :Def11: :: AMISTD_2:def 11
for T being InsType of S holds AddressParts T is product-like;
end;

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

registration
let N be set ;
cluster regular -> homogeneous AMI-Struct of N;
coherence
for b1 being AMI-Struct of 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;

registration
let N be with_non-empty_elements set ;
cluster STC N -> homogeneous with_explicit_jumps without_implicit_jumps with-non-trivial-Instruction-Locations 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 non void halting IC-Ins-separated steady-programmed definite realistic programmable standard homogeneous with_explicit_jumps without_implicit_jumps with-non-trivial-Instruction-Locations regular AMI-Struct of N;
existence
ex b1 being non empty non void IC-Ins-separated definite AMI-Struct of 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 N be with_non-empty_elements set ;
let S be regular AMI-Struct of N;
let T be InsType of S;
cluster AddressParts T -> functional with_common_domain product-like ;
coherence
AddressParts T is product-like by Def11;
end;

registration
let N be with_non-empty_elements set ;
let S be homogeneous AMI-Struct of N;
let T be InsType of S;
cluster AddressParts T -> functional with_common_domain ;
coherence
AddressParts T is with_common_domain
proof end;
end;

theorem Th20: :: AMISTD_2:20
for N being with_non-empty_elements set
for S being non empty non void homogeneous AMI-Struct of N
for I being Instruction of S
for x being set st x in dom (AddressPart I) & (PA (AddressParts (InsCode I))) . x = the Instruction-Locations of S holds
(AddressPart I) . x is Instruction-Location of S
proof end;

registration
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite with_explicit_jumps AMI-Struct of 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 N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite without_implicit_jumps AMI-Struct of 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 S being non empty non void IC-Ins-separated definite realistic with-non-trivial-Instruction-Locations AMI-Struct of N
for I being Instruction of S st I is halting holds
JUMP I is empty
proof end;

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

registration
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite with-non-trivial-Instruction-Locations AMI-Struct of N;
cluster non trivial programmed FinPartState 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 non void halting IC-Ins-separated definite standard AMI-Struct of N;
cluster non empty trivial programmed -> non empty programmed unique-halt FinPartState 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 N be set ;
let S be AMI-Struct of 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
(PA (AddressParts (InsCode I))) . x <> the Instruction-Locations of S;
end;

:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :
for N being set
for S being AMI-Struct of 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
(PA (AddressParts (InsCode I))) . x <> the Instruction-Locations of S );

theorem :: AMISTD_2:22
for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic with_explicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of 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 S being non empty non void IC-Ins-separated definite realistic without_implicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of N
for I being Instruction of S st I is halting holds
I is ins-loc-free
proof end;

registration
let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite realistic without_implicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of N;
cluster halting -> without_implicit_jumps 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 non void IC-Ins-separated definite standard without_implicit_jumps AMI-Struct of 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 non void IC-Ins-separated definite standard without_implicit_jumps AMI-Struct of N;
cluster sequential -> without_implicit_jumps 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 non void halting IC-Ins-separated definite standard AMI-Struct of N;
func Stop S -> FinPartState of S equals :: AMISTD_2:def 13
(il. S,0) .--> (halt S);
coherence
(il. S,0) .--> (halt S)</