:: AMISTD_2 semantic presentation

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

registration

let f be Function;
let g be non empty Function;
cluster f +* g -> non empty ;
coherence

proof end;

cluster g +* f -> non empty ;
coherence

proof end;

end;

registration

let f, g be finite Function;
cluster f +* g -> finite ;
coherence

proof end;

end;

theorem Th1: :: AMISTD_2:1

for f, g being Function holds
( dom f, dom g are_equipotent iff f,g are_equipotent )

proof end;

theorem Th2: :: AMISTD_2:2

for f, g being finite Function st dom f misses dom g holds
card (f +* g) = (card f) + (card g)

proof end;

registration

let f be Function;
let A be set ;
cluster f \ A -> Relation-like Function-like ;
coherence by GRFUNC_1:38;

end;

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;

theorem Th4: :: AMISTD_2:4

for F being non empty finite set holds (card F) - 1 = (card F) -' 1

proof end;

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

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines PA AMISTD_2:def 1 :

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 :

registration

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

end;

registration

cluster product-like -> functional with_common_domain set ;
coherence

proof end;

end;

registration

cluster non empty functional with_common_domain product-like set ;
existence

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

proof end;

end;

registration

let i be Nat;
let D be set ;
cluster i -tuples_on D -> functional with_common_domain ;
coherence

proof end;

end;

registration

let i be Nat;
let D be set ;
cluster i -tuples_on D -> functional with_common_domain product-like ;
coherence

proof end;

end;

Lm2: for k being natural number holds - 1 < k

proof end;

Lm3: for k being natural number
for a, b, c being 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

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

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 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 ;

end;

:: deftheorem defines AddressPart AMISTD_2:def 3 :

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 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 :

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 ;

end;

:: deftheorem defines AddressParts AMISTD_2:def 5 :

registration

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

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 :

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :

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 :

:: deftheorem Def9 defines without_implicit_jumps AMISTD_2:def 9 :

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 :

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

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

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 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

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 :

registration

let N be set ;
cluster regular -> homogeneous AMI-Struct of N;
coherence

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

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

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 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

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 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 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 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 programmed non trivial FinPartState of S;
existence

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 programmed trivial -> non empty programmed unique-halt FinPartState of S;
coherence

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 :

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 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 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 ;

end;

:: deftheorem defines Stop AMISTD_2:def 13 :

Lm4: now

let N be with_non-empty_elements set ; :: thesis:
let S be non empty non void halting IC-Ins-separated definite standard AMI-Struct of N; :: thesis:
thus dom (Stop S) = dom ((il. S,0) .--> (halt S))
.= {(il. S,0)} by CQC_LANG:5 ; :: thesis:
hence il. S,0 in dom (Stop S) by TARSKI:def 1; :: thesis:

end;

Lm5: for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N holds (Stop S) . (il. S,0) = halt S
by CQC_LANG:6;

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 Stop S -> non empty programmed lower unique-halt trivial ;
coherence by AMISTD_1:48;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of N;
cluster Stop S -> non empty programmed closed lower unique-halt trivial ;
coherence by AMISTD_1:46;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated steady-programmed definite standard AMI-Struct of N;
cluster Stop S -> non empty autonomic programmed lower unique-halt trivial ;
coherence by AMISTD_1:12;

end;

theorem Th25: :: AMISTD_2:25

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N holds card (Stop S) = 1

proof end;

theorem Th26: :: AMISTD_2:26

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N
for F being pre-Macro of S st card F = 1 holds
F = Stop S

proof end;

Lm6: for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N holds (card (Stop S)) -' 1 = 0

proof end;

theorem Th27: :: AMISTD_2:27

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N holds LastLoc (Stop S) = il. S,0

proof end;

registration

proof end;

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;
:: original: Stop
redefine func Stop S -> pre-Macro of S;
coherence ;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let I be Element of the Instructions of S;
let k be natural number ;
func IncAddr I,k -> Instruction of S means :Def14: :: AMISTD_2:def 14
( InsCode it = InsCode I & dom (AddressPart it) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (PA (AddressParts (InsCode I))) . n = the Instruction-Locations of S implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart it) . n = il. S,(k + (locnum f)) ) ) & ( (PA (AddressParts (InsCode I))) . n <> the Instruction-Locations of S implies (AddressPart it) . n = (AddressPart I) . n ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :

theorem Th28: :: AMISTD_2:28

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I being Element of the Instructions of S holds IncAddr I,0 = I

proof end;

theorem Th29: :: AMISTD_2:29

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I

proof end;

theorem :: AMISTD_2:30

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of N holds IncAddr (halt S),k = halt S by Th29;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of N;
let I be halting Instruction of S;
let k be natural number ;
cluster IncAddr I,k -> halting without_implicit_jumps ins-loc-free ;
coherence by Th29;

end;

theorem Th31: :: AMISTD_2:31

proof end;

theorem Th32: :: AMISTD_2:32

for x being set
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k & (PA (AddressParts (InsCode I))) . x = the Instruction-Locations of S holds
(PA (AddressParts (InsCode J))) . x = the Instruction-Locations of S

proof end;

theorem Th33: :: AMISTD_2:33

for x being set
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k & (PA (AddressParts (InsCode I))) . x <> the Instruction-Locations of S holds
(PA (AddressParts (InsCode J))) . x <> the Instruction-Locations of S

proof end;

theorem Th34: :: AMISTD_2:34

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J

proof end;

theorem Th35: :: AMISTD_2:35

proof end;

theorem :: AMISTD_2:36

proof end;

theorem Th37: :: AMISTD_2:37

for k, m being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for I being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let p be programmed FinPartState of S;
let k be natural number ;
A1: dom p c= the Instruction-Locations of S by AMI_3:def 13;
func IncAddr p,k -> FinPartState of S means :Def15: :: AMISTD_2:def 15
( dom it = dom p & ( for m being natural number st il. S,m in dom p holds
it . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines IncAddr AMISTD_2:def 15 :

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F be programmed FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> programmed ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F be empty programmed FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> empty programmed ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F be non empty programmed FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> non empty programmed ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F be programmed lower FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> programmed lower ;
coherence

proof end;

end;

theorem Th38: :: AMISTD_2:38

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F being programmed FinPartState of S holds IncAddr F,0 = F

proof end;

theorem :: AMISTD_2:39

for k, m being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F being programmed lower FinPartState of S holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let p be FinPartState of S;
let k be natural number ;
func Shift p,k -> FinPartState of S means :Def16: :: AMISTD_2:def 16
( dom it = { (il. S,(m + k)) where m is Nat : il. S,m in dom p } & ( for m being Nat st il. S,m in dom p holds
it . (il. S,(m + k)) = p . (il. S,m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Shift AMISTD_2:def 16 :

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be FinPartState of S;
let k be natural number ;
cluster Shift F,k -> programmed ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be empty FinPartState of S;
let k be natural number ;
cluster Shift F,k -> empty programmed ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty programmed FinPartState of S;
let k be natural number ;
cluster Shift F,k -> non empty programmed ;
coherence

proof end;

end;

theorem Th40: :: AMISTD_2:40

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 FinPartState of S holds Shift F,0 = F

proof end;

theorem Th41: :: AMISTD_2:41

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 FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)

proof end;

theorem :: AMISTD_2:42

for m, k being natural number
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 FinPartState of S holds Shift (Shift F,m),k = Shift F,(m + k)

proof end;

theorem Th43: :: AMISTD_2:43

for k being natural number
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 FinPartState of S holds dom F, dom (Shift F,k) are_equipotent

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let I be Instruction of S;
attr I is IC-good means :Def17: :: AMISTD_2:def 17
for k being natural number
for s1, s2 being State of S st s2 = s1 +* ((IC S) .--> ((IC s1) + k)) holds
(IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2);

end;

:: deftheorem Def17 defines IC-good AMISTD_2:def 17 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
attr S is IC-good means :Def18: :: AMISTD_2:def 18
for I being Instruction of S holds I is IC-good;

end;

:: deftheorem Def18 defines IC-good AMISTD_2:def 18 :

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
let I be Instruction of S;
attr I is Exec-preserving means :Def19: :: AMISTD_2:def 19
for s1, s2 being State of S st s1,s2 equal_outside the Instruction-Locations of S holds
Exec I,s1, Exec I,s2 equal_outside the Instruction-Locations of S;

end;

:: deftheorem Def19 defines Exec-preserving AMISTD_2:def 19 :

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
attr S is Exec-preserving means :Def20: :: AMISTD_2:def 20
for I being Instruction of S holds I is Exec-preserving;

end;

:: deftheorem Def20 defines Exec-preserving AMISTD_2:def 20 :

theorem Th44: :: AMISTD_2:44

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard without_implicit_jumps regular AMI-Struct of N
for I being Instruction of S st I is sequential holds
I is IC-good

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 regular AMI-Struct of N;
cluster sequential -> without_implicit_jumps IC-good Element of the Instructions of S;
coherence by Th44;

end;

theorem Th45: :: AMISTD_2:45

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of N
for I being Instruction of S st I is halting holds
I is IC-good

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of N;
cluster halting -> without_implicit_jumps IC-good Element of the Instructions of S;
coherence by Th45;

end;

theorem Th46: :: AMISTD_2:46

for N being with_non-empty_elements set
for S being non void AMI-Struct of N
for I being Instruction of S st I is halting holds
I is Exec-preserving

proof end;

registration

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
cluster halting -> Exec-preserving Element of the Instructions of S;
coherence by Th46;

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 IC-good Exec-preserving ;
coherence

proof end;

end;

registration

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular IC-good AMI-Struct of N;
cluster -> IC-good Element of the Instructions of S;
coherence by Def18;

end;

registration

let N be with_non-empty_elements set ;
let S be non void Exec-preserving AMI-Struct of N;
cluster -> Exec-preserving Element of the Instructions of S;
coherence by Def20;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty programmed FinPartState of S;
func CutLastLoc F -> FinPartState of S equals :: AMISTD_2:def 21
F \ ((LastLoc F) .--> (F . (LastLoc F)));
coherence by Th11;

end;

:: deftheorem defines CutLastLoc AMISTD_2:def 21 :

Lm7: 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 non empty programmed FinPartState of S holds CutLastLoc F c= F
by XBOOLE_1:36;

theorem Th47: :: AMISTD_2:47

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 non empty programmed FinPartState of S holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}

proof end;

theorem Th48: :: AMISTD_2:48

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty programmed trivial FinPartState of S;
cluster CutLastLoc F -> empty ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty programmed FinPartState of S;
cluster CutLastLoc F -> programmed ;
coherence by Th12;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty programmed lower FinPartState of S;
cluster CutLastLoc F -> programmed lower ;
coherence

proof end;

end;

theorem Th49: :: AMISTD_2:49

proof end;

theorem Th50: :: AMISTD_2:50

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F being non empty programmed lower FinPartState of S
for G being non empty programmed FinPartState of S holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))

proof end;

theorem Th51: :: AMISTD_2:51

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N
for F being non empty programmed lower unique-halt FinPartState of S
for I being Instruction-Location of S st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F, G be non empty programmed FinPartState of S;
func F ';' G -> FinPartState of S equals :: AMISTD_2:def 22
(CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1));
coherence ;

end;

:: deftheorem defines ';' AMISTD_2:def 22 :

Lm8: for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F, G being non empty programmed FinPartState of S holds dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)))
by FUNCT_4:def 1;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F, G be non empty programmed FinPartState of S;
cluster F ';' G -> non empty programmed ;
coherence ;

end;

theorem Th52: :: AMISTD_2:52

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F being non empty programmed lower FinPartState of S
for G being non empty programmed FinPartState of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let F, G be non empty programmed lower FinPartState of S;
cluster F ';' G -> non empty programmed lower ;
coherence

proof end;

end;

theorem Th53: :: AMISTD_2:53

proof end;

theorem Th54: :: AMISTD_2:54

proof end;

theorem Th55: :: AMISTD_2:55

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F, G being non empty programmed lower FinPartState of S holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . (il. S,0)

proof end;

theorem :: AMISTD_2:56

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for F, G being non empty programmed lower FinPartState of S
for f being Instruction-Location of S st locnum f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of N;
let F be non empty programmed lower FinPartState of S;
let G be non empty programmed lower halt-ending FinPartState of S;
cluster F ';' G -> non empty programmed lower halt-ending ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of N;
let F, G be non empty programmed lower halt-ending unique-halt FinPartState of S;
cluster F ';' G -> non empty programmed lower halt-ending unique-halt ;
coherence

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of N;
let F, G be pre-Macro of S;
:: original: ';'
redefine func F ';' G -> pre-Macro of S;
coherence ;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard regular IC-good Exec-preserving AMI-Struct of N;
let F, G be non empty programmed closed lower FinPartState of S;
cluster F ';' G -> non empty programmed closed lower ;
coherence

proof end;

end;

theorem Th57: :: AMISTD_2:57

proof end;

theorem Th58: :: AMISTD_2:58

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard AMI-Struct of N holds Shift (Stop S),k = (il. S,k) .--> (halt S)

proof end;

theorem Th59: :: AMISTD_2:59

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of N
for F being pre-Macro of S holds F ';' (Stop S) = F

proof end;

theorem Th60: :: AMISTD_2:60

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite standard regular AMI-Struct of N
for F being pre-Macro of S holds (Stop S) ';' F = F

proof end;

theorem :: AMISTD_2:61

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of N
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)

proof end;