:: AMISTD_2 semantic presentation

Lemma1: for b₁ being Relation st dom b₁ <> {} holds
b₁ <> {}
by RELAT_1:60;

registration

let c₁ be Function;
let c₂ be non empty Function;
cluster a₁ +* a₂ -> non empty ;
coherence

proof end;

cluster a₂ +* a₁ -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂ be finite Function;
cluster a₁ +* a₂ -> finite ;
coherence

proof end;

end;

theorem Th1: :: AMISTD_2:1

for b₁, b₂ being Function holds
( dom b₁, dom b₂ are_equipotent iff b₁,b₂ are_equipotent )

proof end;

theorem Th2: :: AMISTD_2:2

for b₁, b₂ being finite Function st dom b₁ misses dom b₂ holds
card (b₁ +* b₂) = (card b₁) + (card b₂)

proof end;

registration

let c₁ be Function;
let c₂ be set ;
cluster a₁ \ a₂ -> Relation-like Function-like ;
coherence by GRFUNC_1:38;

end;

theorem Th3: :: AMISTD_2:3

for b₁ being set
for b₂, b₃ being Function st b₁ in (dom b₂) \ (dom b₃) holds
(b₂ \ b₃) . b₁ = b₂ . b₁

proof end;

theorem Th4: :: AMISTD_2:4

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

proof end;

definition

let c₁ be functional set ;
func PA c₁ -> Function means :Def1: :: AMISTD_2:def 1
( ( for b₁ being set holds
( b₁ in dom a₂ iff for b₂ being Function st b₂ in a₁ holds
b₁ in dom b₂ ) ) & ( for b₁ being set st b₁ in dom a₂ holds
a₂ . b₁ = pi a₁,b₁ ) ) if not a₁ is empty
otherwise a₂ = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines PA AMISTD_2:def 1 :

theorem Th5: :: AMISTD_2:5

for b₁ being non empty functional set holds dom (PA b₁) = meet { (dom b₂) where B is Element of b₁ : verum }

proof end;

theorem Th6: :: AMISTD_2:6

for b₁ being non empty functional set
for b₂ being set st b₂ in dom (PA b₁) holds
(PA b₁) . b₂ = { (b₃ . b₂) where B is Element of b₁ : verum }

proof end;

definition

let c₁ be set ;
attr a₁ is product-like means :Def2: :: AMISTD_2:def 2
ex b₁ being Function st a₁ = product b₁;

end;

:: deftheorem Def2 defines product-like AMISTD_2:def 2 :

registration

let c₁ be Function;
cluster product a₁ -> 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 b₁ being functional with_common_domain set holds dom (PA b₁) = DOM b₁

proof end;

theorem Th8: :: AMISTD_2:8

for b₁ being functional set
for b₂ being set st b₂ in dom (PA b₁) holds
(PA b₁) . b₂ = pi b₁,b₂

proof end;

theorem Th9: :: AMISTD_2:9

for b₁ being functional with_common_domain set holds b₁ c= product (PA b₁)

proof end;

theorem Th10: :: AMISTD_2:10

for b₁ being non empty product-like set holds b₁ = product (PA b₁)

proof end;

registration

let c₁ be set ;
cluster -> functional FinSequenceSet of a₁;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be set ;
cluster a₁ -tuples_on a₂ -> functional with_common_domain ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be set ;
cluster a₁ -tuples_on a₂ -> functional with_common_domain product-like ;
coherence

proof end;

end;

Lemma11: for b₁ being natural number holds - 1 < b₁

proof end;

Lemma12: for b₁ being natural number
for b₂, b₃, b₄ being Nat st 1 <= b₂ & 2 <= b₃ & not b₁ < b₂ - 1 & not ( b₂ <= b₁ & b₁ <= (b₂ + b₃) - 3 ) & not b₁ = (b₂ + b₃) - 2 & not (b₂ + b₃) - 2 < b₁ holds
b₁ = b₂ - 1

proof end;

theorem Th11: :: AMISTD_2:11

for b₁, b₂ being set
for b₃ being AMI-Struct of b₂
for b₄ being FinPartState of b₃ holds b₄ \ b₁ is FinPartState of b₃

proof end;

theorem Th12: :: AMISTD_2:12

for b₁ being set
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃ holds b₄ \ b₁ is programmed FinPartState of b₃

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃, c₄ be Instruction-Location of c₂;
let c₅, c₆ be Element of the Instructions of c₂;
redefine func --> as c₃,c₄ --> c₅,c₆ -> FinPartState of a₂;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halting Element of the Instructions of a₂;
existence

proof end;

end;

theorem Th13: :: AMISTD_2:13

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂
for b₄ being programmed FinPartState of b₂ st dom b₃ = dom b₄ holds
b₄ is lower

proof end;

theorem Th14: :: AMISTD_2:14

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂
for b₄ being Instruction-Location of b₂ st b₄ in dom b₃ holds
locnum b₄ < card b₃

proof end;

theorem Th15: :: AMISTD_2:15

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂ holds dom b₃ = { (il. b₂,b₄) where B is Nat : b₄ < card b₃ }

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
func AddressPart c₃ -> set equals :: AMISTD_2:def 3
a₃ `2 ;
coherence ;

end;

:: deftheorem Def3 defines AddressPart AMISTD_2:def 3 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
redefine func AddressPart as AddressPart c₃ -> FinSequence of (union a₁) \/ the carrier of a₂;
coherence by FINSEQ_1:def 11;

end;

theorem Th16: :: AMISTD_2:16

for b₁ being set
for b₂ being AMI-Struct of b₁
for b₃, b₄ being Element of the Instructions of b₂ st InsCode b₃ = InsCode b₄ & AddressPart b₃ = AddressPart b₄ holds
b₃ = b₄

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is homogeneous means :Def4: :: AMISTD_2:def 4
for b₁, b₂ being Instruction of a₂ st InsCode b₁ = InsCode b₂ holds
dom (AddressPart b₁) = dom (AddressPart b₂);

end;

:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :

theorem Th17: :: AMISTD_2:17

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁) holds AddressPart b₂ = 0

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be InsType of c₂;
func AddressParts c₃ -> set equals :: AMISTD_2:def 5
{ (AddressPart b₁) where B is Instruction of a₂ : InsCode b₁ = a₃ } ;
coherence ;

end;

:: deftheorem Def5 defines AddressParts AMISTD_2:def 5 :

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be InsType of c₂;
cluster AddressParts a₃ -> functional ;
coherence

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is with_explicit_jumps means :Def6: :: AMISTD_2:def 6
for b₁ being set st b₁ in JUMP a₃ holds
ex b₂ being set st
( b₂ in dom (AddressPart a₃) & b₁ = (AddressPart a₃) . b₂ & (PA (AddressParts (InsCode a₃))) . b₂ = the Instruction-Locations of a₂ );
attr a₃ is without_implicit_jumps means :Def7: :: AMISTD_2:def 7
for b₁ being set st ex b₂ being set st
( b₂ in dom (AddressPart a₃) & b₁ = (AddressPart a₃) . b₂ & (PA (AddressParts (InsCode a₃))) . b₂ = the Instruction-Locations of a₂ ) holds
b₁ in JUMP a₃;

end;

:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
attr a₂ is with_explicit_jumps means :Def8: :: AMISTD_2:def 8
for b₁ being Instruction of a₂ holds b₁ is with_explicit_jumps;
attr a₂ is without_implicit_jumps means :Def9: :: AMISTD_2:def 9
for b₁ being Instruction of a₂ holds b₁ 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 c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is with-non-trivial-Instruction-Locations means :Def10: :: AMISTD_2:def 10
not the Instruction-Locations of a₂ is trivial;

end;

:: deftheorem Def10 defines with-non-trivial-Instruction-Locations AMISTD_2:def 10 :

registration

let c₁ 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 a₁;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated definite standard with-non-trivial-Instruction-Locations AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be with-non-trivial-Instruction-Locations AMI-Struct of c₁;
cluster the Instruction-Locations of a₂ -> non trivial ;
coherence by Def10;

end;

theorem Th18: :: AMISTD_2:18

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction of b₂ st ( for b₄ being Instruction-Location of b₂ holds NIC b₃,b₄ = {(NextLoc b₄)} ) holds
JUMP b₃ is empty

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be Instruction of (STC c₁);
cluster JUMP a₂ -> empty ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is regular means :Def11: :: AMISTD_2:def 11
for b₁ being InsType of a₂ holds AddressParts b₁ is product-like;

end;

:: deftheorem Def11 defines regular AMISTD_2:def 11 :

registration

let c₁ be set ;
cluster regular -> homogeneous AMI-Struct of a₁;
coherence

proof end;

end;

theorem Th19: :: AMISTD_2:19

for b₁ being with_non-empty_elements set
for b₂ being InsType of (STC b₁) holds AddressParts b₂ = {0}

proof end;

registration

let c₁ be with_non-empty_elements set ;
cluster STC a₁ -> homogeneous with_explicit_jumps without_implicit_jumps with-non-trivial-Instruction-Locations regular ;
coherence

proof end;

end;

registration

let c₁ 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 a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be regular AMI-Struct of c₁;
let c₃ be InsType of c₂;
cluster AddressParts a₃ -> functional with_common_domain product-like ;
coherence by Def11;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be homogeneous AMI-Struct of c₁;
let c₃ be InsType of c₂;
cluster AddressParts a₃ -> functional with_common_domain ;
coherence

proof end;

end;

theorem Th20: :: AMISTD_2:20

for b₁ being with_non-empty_elements set
for b₂ being non empty non void homogeneous AMI-Struct of b₁
for b₃ being Instruction of b₂
for b₄ being set st b₄ in dom (AddressPart b₃) & (PA (AddressParts (InsCode b₃))) . b₄ = the Instruction-Locations of b₂ holds
(AddressPart b₃) . b₄ is Instruction-Location of b₂

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite with_explicit_jumps AMI-Struct of c₁;
cluster -> with_explicit_jumps Element of the Instructions of a₂;
coherence by Def8;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite without_implicit_jumps AMI-Struct of c₁;
cluster -> without_implicit_jumps Element of the Instructions of a₂;
coherence by Def9;

end;

theorem Th21: :: AMISTD_2:21

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic with-non-trivial-Instruction-Locations AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is halting holds
JUMP b₃ is empty

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic with-non-trivial-Instruction-Locations AMI-Struct of c₁;
let c₃ be halting Instruction of c₂;
cluster JUMP a₃ -> empty ;
coherence by Th21;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite with-non-trivial-Instruction-Locations AMI-Struct of c₁;
cluster programmed non trivial FinPartState of a₂;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c₁;
cluster non empty programmed trivial -> non empty programmed unique-halt FinPartState of a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is ins-loc-free means :Def12: :: AMISTD_2:def 12
for b₁ being set st b₁ in dom (AddressPart a₃) holds
(PA (AddressParts (InsCode a₃))) . b₁ <> the Instruction-Locations of a₂;

end;

:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :

theorem Th22: :: AMISTD_2:22

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic with_explicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is ins-loc-free holds
JUMP b₃ is empty

proof end;

theorem Th23: :: AMISTD_2:23

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic without_implicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is halting holds
b₃ is ins-loc-free

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite realistic without_implicit_jumps with-non-trivial-Instruction-Locations AMI-Struct of c₁;
cluster halting -> without_implicit_jumps ins-loc-free Element of the Instructions of a₂;
coherence by Th23;

end;

theorem Th24: :: AMISTD_2:24

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard without_implicit_jumps AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is sequential holds
b₃ is ins-loc-free

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard without_implicit_jumps AMI-Struct of c₁;
cluster sequential -> without_implicit_jumps ins-loc-free Element of the Instructions of a₂;
coherence by Th24;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c₁;
func Stop c₂ -> FinPartState of a₂ equals :: AMISTD_2:def 13
(il. a₂,0) .--> (halt a₂);
coherence ;

end;

:: deftheorem Def13 defines Stop AMISTD_2:def 13 :

E34: now

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

end;

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

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c₁;
cluster Stop a₂ -> non empty programmed lower unique-halt trivial ;
coherence by AMISTD_1:48;

end;

registration

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

end;

registration

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

end;

theorem Th25: :: AMISTD_2:25

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

proof end;

theorem Th26: :: AMISTD_2:26

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being pre-Macro of b₂ st card b₃ = 1 holds
b₃ = Stop b₂

proof end;

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

proof end;

theorem Th27: :: AMISTD_2:27

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

proof end;

registration

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c₁;
redefine func Stop as Stop c₂ -> pre-Macro of a₂;
coherence ;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
let c₄ be natural number ;
func IncAddr c₃,c₄ -> Instruction of a₂ means :Def14: :: AMISTD_2:def 14
( InsCode a₅ = InsCode a₃ & dom (AddressPart a₅) = dom (AddressPart a₃) & ( for b₁ being set st b₁ in dom (AddressPart a₃) holds
( ( (PA (AddressParts (InsCode a₃))) . b₁ = the Instruction-Locations of a₂ implies ex b₂ being Instruction-Location of a₂ st
( b₂ = (AddressPart a₃) . b₁ & (AddressPart a₅) . b₁ = il. a₂,(a₄ + (locnum b₂)) ) ) & ( (PA (AddressParts (InsCode a₃))) . b₁ <> the Instruction-Locations of a₂ implies (AddressPart a₅) . b₁ = (AddressPart a₃) . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :

theorem Th28: :: AMISTD_2:28

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃ being Element of the Instructions of b₂ holds IncAddr b₃,0 = b₃

proof end;

theorem Th29: :: AMISTD_2:29

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being Instruction of b₃ st b₄ is ins-loc-free holds
IncAddr b₄,b₁ = b₄

proof end;

theorem Th30: :: AMISTD_2:30

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

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of c₁;
let c₃ be halting Instruction of c₂;
let c₄ be natural number ;
cluster IncAddr a₃,a₄ -> halting without_implicit_jumps ins-loc-free ;
coherence by Th29;

end;

theorem Th31: :: AMISTD_2:31

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being Instruction of b₃ holds AddressParts (InsCode b₄) = AddressParts (InsCode (IncAddr b₄,b₁))

proof end;

theorem Th32: :: AMISTD_2:32

for b₁ being set
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄, b₅ being Instruction of b₃ st ex b₆ being natural number st IncAddr b₄,b₆ = IncAddr b₅,b₆ & (PA (AddressParts (InsCode b₄))) . b₁ = the Instruction-Locations of b₃ holds
(PA (AddressParts (InsCode b₅))) . b₁ = the Instruction-Locations of b₃

proof end;

theorem Th33: :: AMISTD_2:33

for b₁ being set
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄, b₅ being Instruction of b₃ st ex b₆ being natural number st IncAddr b₄,b₆ = IncAddr b₅,b₆ & (PA (AddressParts (InsCode b₄))) . b₁ <> the Instruction-Locations of b₃ holds
(PA (AddressParts (InsCode b₅))) . b₁ <> the Instruction-Locations of b₃

proof end;

theorem Th34: :: AMISTD_2:34

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃, b₄ being Instruction of b₂ st ex b₅ being natural number st IncAddr b₃,b₅ = IncAddr b₄,b₅ holds
b₃ = b₄

proof end;

theorem Th35: :: AMISTD_2:35

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of b₂
for b₄ being Instruction of b₃ st IncAddr b₄,b₁ = halt b₃ holds
b₄ = halt b₃

proof end;

theorem Th36: :: AMISTD_2:36

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void halting IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of b₂
for b₄ being Instruction of b₃ st b₄ is sequential holds
IncAddr b₄,b₁ is sequential

proof end;

theorem Th37: :: AMISTD_2:37

for b₁, b₂ being natural number
for b₃ being with_non-empty_elements set
for b₄ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₃
for b₅ being Instruction of b₄ holds IncAddr (IncAddr b₅,b₁),b₂ = IncAddr b₅,(b₁ + b₂)

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be programmed FinPartState of c₂;
let c₄ be natural number ;
E49: dom c₃ c= the Instruction-Locations of c₂ by AMI_3:def 13;
func IncAddr c₃,c₄ -> FinPartState of a₂ means :Def15: :: AMISTD_2:def 15
( dom a₅ = dom a₃ & ( for b₁ being natural number st il. a₂,b₁ in dom a₃ holds
a₅ . (il. a₂,b₁) = IncAddr (pi a₃,(il. a₂,b₁)),a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines IncAddr AMISTD_2:def 15 :

registration

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be empty programmed FinPartState of c₂;
let c₄ be natural number ;
cluster IncAddr a₃,a₄ -> empty programmed ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be non empty programmed FinPartState of c₂;
let c₄ be natural number ;
cluster IncAddr a₃,a₄ -> non empty programmed ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be programmed lower FinPartState of c₂;
let c₄ be natural number ;
cluster IncAddr a₃,a₄ -> programmed lower ;
coherence

proof end;

end;

theorem Th38: :: AMISTD_2:38

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃ being programmed FinPartState of b₂ holds IncAddr b₃,0 = b₃

proof end;

theorem Th39: :: AMISTD_2:39

for b₁, b₂ being natural number
for b₃ being with_non-empty_elements set
for b₄ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₃
for b₅ being programmed lower FinPartState of b₄ holds IncAddr (IncAddr b₅,b₁),b₂ = IncAddr b₅,(b₁ + b₂)

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
let c₄ be natural number ;
func Shift c₃,c₄ -> FinPartState of a₂ means :Def16: :: AMISTD_2:def 16
( dom a₅ = { (il. a₂,(b₁ + a₄)) where B is Nat : il. a₂,b₁ in dom a₃ } & ( for b₁ being Nat st il. a₂,b₁ in dom a₃ holds
a₅ . (il. a₂,(b₁ + a₄)) = a₃ . (il. a₂,b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Shift AMISTD_2:def 16 :

registration

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be empty FinPartState of c₂;
let c₄ be natural number ;
cluster Shift a₃,a₄ -> empty programmed ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be non empty programmed FinPartState of c₂;
let c₄ be natural number ;
cluster Shift a₃,a₄ -> non empty programmed ;
coherence

proof end;

end;

theorem Th40: :: AMISTD_2:40

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed FinPartState of b₂ holds Shift b₃,0 = b₃

proof end;

theorem Th41: :: AMISTD_2:41

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being FinPartState of b₂
for b₄ being natural number st b₄ > 0 holds
not il. b₂,0 in dom (Shift b₃,b₄)

proof end;

theorem Th42: :: AMISTD_2:42

for b₁, b₂ being natural number
for b₃ being with_non-empty_elements set
for b₄ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₃
for b₅ being FinPartState of b₄ holds Shift (Shift b₅,b₁),b₂ = Shift b₅,(b₁ + b₂)

proof end;

theorem Th43: :: AMISTD_2:43

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃ holds dom b₄, dom (Shift b₄,b₁) are_equipotent

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is IC-good means :Def17: :: AMISTD_2:def 17
for b₁ being natural number
for b₂, b₃ being State of a₂ st b₃ = b₂ +* ((IC a₂) .--> ((IC b₂) + b₁)) holds
(IC (Exec a₃,b₂)) + b₁ = IC (Exec (IncAddr a₃,b₁),b₃);

end;

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

definition

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

end;

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

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is Exec-preserving means :Def19: :: AMISTD_2:def 19
for b₁, b₂ being State of a₂ st b₁,b₂ equal_outside the Instruction-Locations of a₂ holds
Exec a₃,b₁, Exec a₃,b₂ equal_outside the Instruction-Locations of a₂;

end;

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

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
attr a₂ is Exec-preserving means :Def20: :: AMISTD_2:def 20
for b₁ being Instruction of a₂ holds b₁ is Exec-preserving;

end;

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

theorem Th44: :: AMISTD_2:44

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard without_implicit_jumps regular AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is sequential holds
b₃ is IC-good

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard without_implicit_jumps regular AMI-Struct of c₁;
cluster sequential -> without_implicit_jumps IC-good Element of the Instructions of a₂;
coherence by Th44;

end;

theorem Th45: :: AMISTD_2:45

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic standard without_implicit_jumps regular AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is halting holds
b₃ is IC-good

proof end;

registration

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

end;

theorem Th46: :: AMISTD_2:46

for b₁ being with_non-empty_elements set
for b₂ being non void AMI-Struct of b₁
for b₃ being Instruction of b₂ st b₃ is halting holds
b₃ is Exec-preserving

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
cluster halting -> Exec-preserving Element of the Instructions of a₂;
coherence by Th46;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster STC a₁ -> 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 c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular IC-good AMI-Struct of c₁;
cluster -> IC-good Element of the Instructions of a₂;
coherence by Def18;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void Exec-preserving AMI-Struct of c₁;
cluster -> Exec-preserving Element of the Instructions of a₂;
coherence by Def20;

end;

definition

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

end;

:: deftheorem Def21 defines CutLastLoc AMISTD_2:def 21 :

Lemma62: for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being non empty programmed FinPartState of b₂ holds CutLastLoc b₃ c= b₃
by XBOOLE_1:36;

theorem Th47: :: AMISTD_2:47

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being non empty programmed FinPartState of b₂ holds dom (CutLastLoc b₃) = (dom b₃) \ {(LastLoc b₃)}

proof end;

theorem Th48: :: AMISTD_2:48

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be non empty programmed trivial FinPartState of c₂;
cluster CutLastLoc a₃ -> empty ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be non empty programmed FinPartState of c₂;
cluster CutLastLoc a₃ -> programmed ;
coherence by Th12;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be non empty programmed lower FinPartState of c₂;
cluster CutLastLoc a₃ -> programmed lower ;
coherence

proof end;

end;

theorem Th49: :: AMISTD_2:49

proof end;

theorem Th50: :: AMISTD_2:50

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃ being non empty programmed lower FinPartState of b₂
for b₄ being non empty programmed FinPartState of b₂ holds dom (CutLastLoc b₃) misses dom (Shift (IncAddr b₄,((card b₃) -' 1)),((card b₃) -' 1))

proof end;

theorem Th51: :: AMISTD_2:51

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being non empty programmed lower unique-halt FinPartState of b₂
for b₄ being Instruction-Location of b₂ st b₄ in dom (CutLastLoc b₃) holds
(CutLastLoc b₃) . b₄ <> halt b₂

proof end;

definition

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

end;

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

Lemma68: for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃, b₄ being non empty programmed FinPartState of b₂ holds dom (b₃ ';' b₄) = (dom (CutLastLoc b₃)) \/ (dom (Shift (IncAddr b₄,((card b₃) -' 1)),((card b₃) -' 1)))
by FUNCT_4:def 1;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃, c₄ be non empty programmed FinPartState of c₂;
cluster a₃ ';' a₄ -> non empty programmed ;
coherence ;

end;

theorem Th52: :: AMISTD_2:52

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃ being non empty programmed lower FinPartState of b₂
for b₄ being non empty programmed FinPartState of b₂ holds
( card (b₃ ';' b₄) = ((card b₃) + (card b₄)) - 1 & card (b₃ ';' b₄) = ((card b₃) + (card b₄)) -' 1 )

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard regular AMI-Struct of c₁;
let c₃, c₄ be non empty programmed lower FinPartState of c₂;
cluster a₃ ';' a₄ -> 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 b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃, b₄ being non empty programmed lower FinPartState of b₂ holds (b₃ ';' b₄) . (LastLoc b₃) = (IncAddr b₄,((card b₃) -' 1)) . (il. b₂,0)

proof end;

theorem Th56: :: AMISTD_2:56

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₁
for b₃, b₄ being non empty programmed lower FinPartState of b₂
for b₅ being Instruction-Location of b₂ st locnum b₅ < (card b₃) - 1 holds
(IncAddr b₃,((card b₃) -' 1)) . b₅ = (IncAddr (b₃ ';' b₄),((card b₃) -' 1)) . b₅

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of c₁;
let c₃ be non empty programmed lower FinPartState of c₂;
let c₄ be non empty programmed lower halt-ending FinPartState of c₂;
cluster a₃ ';' a₄ -> non empty programmed lower halt-ending ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of c₁;
let c₃, c₄ be non empty programmed lower halt-ending unique-halt FinPartState of c₂;
cluster a₃ ';' a₄ -> non empty programmed lower halt-ending unique-halt ;
coherence

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of c₁;
let c₃, c₄ be pre-Macro of c₂;
redefine func ';' as c₃ ';' c₄ -> pre-Macro of a₂;
coherence ;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard regular IC-good Exec-preserving AMI-Struct of c₁;
let c₃, c₄ be non empty programmed closed lower FinPartState of c₂;
cluster a₃ ';' a₄ -> non empty programmed closed lower ;
coherence

proof end;

end;

theorem Th57: :: AMISTD_2:57

proof end;

theorem Th58: :: AMISTD_2:58

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

proof end;

theorem Th59: :: AMISTD_2:59

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

proof end;

theorem Th60: :: AMISTD_2:60

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

proof end;

theorem Th61: :: AMISTD_2:61

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated steady-programmed definite realistic standard without_implicit_jumps regular AMI-Struct of b₁
for b₃, b₄, b₅ being pre-Macro of b₂ holds (b₃ ';' b₄) ';' b₅ = b₃ ';' (b₄ ';' b₅)

proof end;