:: AMISTD_1 semantic presentation

theorem Th1: :: AMISTD_1:1

for b₁ being real number holds max {b₁} = b₁

proof end;

theorem Th2: :: AMISTD_1:2

for b₁ being Nat holds max {b₁} = b₁ by Th1;

registration

cluster non trivial set ;
existence

proof end;

end;

theorem Th3: :: AMISTD_1:3

for b₁ being non empty set
for b₂ being trivial FinSequence of b₁ holds
( b₂ is empty or ex b₃ being Element of b₁ st b₂ = <*b₃*> )

proof end;

registration

cluster -> with_non-empty_elements set ;
coherence

proof end;

end;

registration

let c₁ be finite set ;
let c₂ be set ;
cluster K339(a₁,a₂) -> finite ;
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster a₁ .--> a₂ -> trivial with_non-empty_elements ;
coherence

proof end;

end;

registration

let c₁ be non empty FinSequence;
let c₂ be FinSequence;
cluster a₁ ^' a₂ -> non empty with_non-empty_elements ;
coherence

proof end;

end;

theorem Th4: :: AMISTD_1:4

canceled;

theorem Th5: :: AMISTD_1:5

for b₁ being non empty set
for b₂ being non empty FinSequence of b₁
for b₃ being FinSequence of b₁ holds (b₂ ^' b₃) /. 1 = b₂ /. 1

proof end;

theorem Th6: :: AMISTD_1:6

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being non trivial FinSequence of b₁ holds (b₂ ^' b₃) /. (len (b₂ ^' b₃)) = b₃ /. (len b₃)

proof end;

theorem Th7: :: AMISTD_1:7

for b₁ being FinSequence holds b₁ ^' {} = b₁

proof end;

theorem Th8: :: AMISTD_1:8

for b₁ being set
for b₂ being FinSequence holds b₂ ^' <*b₁*> = b₂

proof end;

theorem Th9: :: AMISTD_1:9

for b₁ being non empty set
for b₂ being Nat
for b₃, b₄ being FinSequence of b₁ st 1 <= b₂ & b₂ <= len b₃ holds
(b₃ ^' b₄) /. b₂ = b₃ /. b₂

proof end;

theorem Th10: :: AMISTD_1:10

for b₁ being non empty set
for b₂ being Nat
for b₃, b₄ being FinSequence of b₁ st 1 <= b₂ & b₂ < len b₄ holds
(b₃ ^' b₄) /. ((len b₃) + b₂) = b₄ /. (b₂ + 1)

proof end;

theorem Th11: :: AMISTD_1:11

for b₁ being with_non-empty_elements set
for b₂ being non empty non void definite AMI-Struct of b₁
for b₃ being Element of the Instructions of b₂
for b₄ being State of b₂ holds b₄ +* (the Instruction-Locations of b₂ --> b₃) is State of b₂

proof end;

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
cluster empty -> with_non-empty_elements programmed FinPartState of a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
cluster empty with_non-empty_elements programmed FinPartState of a₂;
existence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
let c₄ be State of c₂;
cluster (the Execution of a₂ . a₃) . a₄ -> Relation-like Function-like with_non-empty_elements ;
coherence

proof end;

end;

Lemma10: for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Element of the Instructions of b₂
for b₅ being FinPartState of b₂ st b₅ = b₃ .--> b₄ holds
b₅ is autonomic

proof end;

registration

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

proof end;

end;

theorem Th12: :: AMISTD_1:12

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Element of the Instructions of b₂ holds b₃ .--> b₄ is autonomic by Lemma10;

theorem Th13: :: AMISTD_1:13

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁ holds b₂ is programmable

proof end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated steady-programmed definite -> non empty non void IC-Ins-separated definite programmable AMI-Struct of a₁;
coherence by Th13;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void AMI-Struct of c₁;
let c₃ be InsType of c₂;
canceled;
canceled;
attr a₃ is jump-only means :: AMISTD_1:def 3
for b₁ being State of a₂
for b₂ being Object of a₂
for b₃ being Instruction of a₂ st InsCode b₃ = a₃ & b₂ <> IC a₂ holds
(Exec b₃,b₁) . b₂ = b₁ . b₂;

end;

:: deftheorem Def1 AMISTD_1:def 1 :

:: deftheorem Def2 AMISTD_1:def 2 :

:: deftheorem Def3 defines jump-only AMISTD_1:def 3 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is jump-only means :: AMISTD_1:def 4
InsCode a₃ is jump-only;

end;

:: deftheorem Def4 defines jump-only AMISTD_1:def 4 :

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-Location of c₂;
let c₄ be Element of the Instructions of c₂;
func NIC c₄,c₃ -> Subset of the Instruction-Locations of a₂ equals :: AMISTD_1:def 5
{ (IC (Following b₁)) where B is State of a₂ : ( IC b₁ = a₃ & b₁ . a₃ = a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def5 defines NIC AMISTD_1:def 5 :

E12: now

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite realistic AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
let c₄ be Instruction-Location of c₂;
let c₅ be State of c₂;
let c₆ be FinPartState of c₂;
assume E13: c₆ = (IC c₂),c₄ --> c₄,c₃ ;
set c₇ = c₅ +* c₆;
E14: IC c₂ <> c₄ by AMI_1:48;
E15: dom c₆ = {(IC c₂),c₄} by E13, FUNCT_4:65;
then E16: IC c₂ in dom c₆ by TARSKI:def 2;
E17: IC (c₅ +* c₆) = (c₅ +* c₆) . (IC c₂)
.= c₆ . (IC c₂) by E16, FUNCT_4:14
.= c₄ by E13, E14, FUNCT_4:66 ;
c₄ in dom c₆ by E15, TARSKI:def 2;
then (c₅ +* c₆) . c₄ = c₆ . c₄ by FUNCT_4:14
.= c₃ by E13, E14, FUNCT_4:66 ;
hence IC (Following (c₅ +* c₆)) in NIC c₃,c₄ by E17;

end;

registration

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 Element of the Instructions of c₂;
func JUMP c₃ -> Subset of the Instruction-Locations of a₂ equals :: AMISTD_1:def 6
meet { (NIC a₃,b₁) where B is Instruction-Location of a₂ : verum } ;
coherence

proof end;

end;

:: deftheorem Def6 defines JUMP AMISTD_1:def 6 :

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-Location of c₂;
func SUCC c₃ -> Subset of the Instruction-Locations of a₂ equals :: AMISTD_1:def 7
union { ((NIC b₁,a₃) \ (JUMP b₁)) where B is Element of the Instructions of a₂ : verum } ;
coherence

proof end;

end;

:: deftheorem Def7 defines SUCC AMISTD_1:def 7 :

theorem Th14: :: AMISTD_1:14

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 Element of the Instructions of b₂ st not the Instruction-Locations of b₂ is trivial & ( for b₄ being Instruction-Location of b₂ holds NIC b₃,b₄ = {b₄} ) holds
JUMP b₃ is empty

proof end;

theorem Th15: :: AMISTD_1:15

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Instruction of b₂ st b₄ is halting holds
NIC 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 AMI-Struct of c₁;
let c₃, c₄ be Instruction-Location of c₂;
pred c₃ <= c₄ means :Def8: :: AMISTD_1:def 8
ex b₁ being non empty FinSequence of the Instruction-Locations of a₂ st
( b₁ /. 1 = a₃ & b₁ /. (len b₁) = a₄ & ( for b₂ being Nat st 1 <= b₂ & b₂ < len b₁ holds
b₁ /. (b₂ + 1) in SUCC (b₁ /. b₂) ) );
reflexivity

proof end;

end;

:: deftheorem Def8 defines <= AMISTD_1:def 8 :

theorem Th16: :: AMISTD_1:16

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₃, b₄, b₅ being Instruction-Location of b₂ st b₃ <= b₄ & b₄ <= b₅ holds
b₃ <= 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₁;
attr a₂ is InsLoc-antisymmetric means :: AMISTD_1:def 9
for b₁, b₂ being Instruction-Location of a₂ st b₁ <= b₂ & b₂ <= b₁ holds
b₁ = b₂;

end;

:: deftheorem Def9 defines InsLoc-antisymmetric AMISTD_1:def 9 :

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 standard means :Def10: :: AMISTD_1:def 10
ex b₁ being Function of NAT ,the Instruction-Locations of a₂ st
( b₁ is bijective & ( for b₂, b₃ being Nat holds
( b₂ <= b₃ iff b₁ . b₂ <= b₁ . b₃ ) ) );

end;

:: deftheorem Def10 defines standard AMISTD_1:def 10 :

theorem Th17: :: AMISTD_1:17

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₃, b₄ being Function of NAT ,the Instruction-Locations of b₂ st b₃ is bijective & ( for b₅, b₆ being Nat holds
( b₅ <= b₆ iff b₃ . b₅ <= b₃ . b₆ ) ) & b₄ is bijective & ( for b₅, b₆ being Nat holds
( b₅ <= b₆ iff b₄ . b₅ <= b₄ . b₆ ) ) holds
b₃ = b₄

proof end;

theorem Th18: :: AMISTD_1:18

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 Function of NAT ,the Instruction-Locations of b₂ st b₃ is bijective holds
( ( for b₄, b₅ being Nat holds
( b₄ <= b₅ iff b₃ . b₄ <= b₃ . b₅ ) ) iff for b₄ being Nat holds
( b₃ . (b₄ + 1) in SUCC (b₃ . b₄) & ( for b₅ being Nat st b₃ . b₅ in SUCC (b₃ . b₄) holds
b₄ <= b₅ ) ) )

proof end;

theorem Th19: :: AMISTD_1:19

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁ holds
( b₂ is standard iff ex b₃ being Function of NAT ,the Instruction-Locations of b₂ st
( b₃ is bijective & ( for b₄ being Nat holds
( b₃ . (b₄ + 1) in SUCC (b₃ . b₄) & ( for b₅ being Nat st b₃ . b₅ in SUCC (b₃ . b₄) holds
b₄ <= b₅ ) ) ) ) )

proof end;

Lemma20: for b₁, b₂ being set holds dom ((NAT --> b₁) +* (NAT .--> b₂)) = NAT \/ {NAT }

proof end;

set c₁ = {[1,0],[0,0]};

definition

let c₂ be with_non-empty_elements set ;
func STC c₁ -> strict AMI-Struct of a₁ means :Def11: :: AMISTD_1:def 11
( the carrier of a₂ = NAT \/ {NAT } & the Instruction-Counter of a₂ = NAT & the Instruction-Locations of a₂ = NAT & the Instruction-Codes of a₂ = {0,1} & the Instructions of a₂ = {[0,0],[1,0]} & the Object-Kind of a₂ = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b₁ being Function of product the Object-Kind of a₂, product the Object-Kind of a₂ st
( ( for b₂ being Element of product the Object-Kind of a₂ holds b₁ . b₂ = b₂ +* (NAT .--> (succ (b₂ . NAT ))) ) & the Execution of a₂ = ([1,0] .--> b₁) +* ([0,0] .--> (id (product the Object-Kind of a₂))) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines STC AMISTD_1:def 11 :

registration

let c₂ be with_non-empty_elements set ;
cluster the Instruction-Locations of (STC a₁) -> infinite ;
coherence by Def11, CARD_4:15;

end;

registration

let c₂ be with_non-empty_elements set ;
cluster STC a₁ -> non empty strict non void ;
coherence

proof end;

end;

registration

let c₂ be with_non-empty_elements set ;
cluster STC a₁ -> non empty strict non void IC-Ins-separated data-oriented steady-programmed definite realistic programmable ;
coherence

proof end;

end;

Lemma22: for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁)
for b₃ being State of (STC b₁) st InsCode b₂ = 1 holds
(Exec b₂,b₃) . (IC (STC b₁)) = succ (IC b₃)

proof end;

theorem Th20: :: AMISTD_1:20

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁) st InsCode b₂ = 0 holds
b₂ is halting

proof end;

theorem Th21: :: AMISTD_1:21

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁) st InsCode b₂ = 1 holds
not b₂ is halting

proof end;

theorem Th22: :: AMISTD_1:22

for b₁ being with_non-empty_elements set
for b₂ being Element of the Instructions of (STC b₁) holds
( InsCode b₂ = 1 or InsCode b₂ = 0 )

proof end;

theorem Th23: :: AMISTD_1:23

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁) holds b₂ is jump-only

proof end;

Lemma26: for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being Instruction-Location of (STC b₂)
for b₄ being Element of the Instructions of (STC b₂) st b₃ = b₁ & InsCode b₄ = 1 holds
NIC b₄,b₃ = {(b₁ + 1)}

proof end;

Lemma27: for b₁ being with_non-empty_elements set
for b₂ being Element of the Instructions of (STC b₁) holds JUMP b₂ is empty

proof end;

theorem Th24: :: AMISTD_1:24

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being Instruction-Location of (STC b₂) st b₃ = b₁ holds
SUCC b₃ = {b₁,(b₁ + 1)}

proof end;

registration

let c₂ be with_non-empty_elements set ;
cluster STC a₁ -> non empty strict non void IC-Ins-separated data-oriented steady-programmed definite realistic programmable standard ;
coherence

proof end;

end;

registration

let c₂ be with_non-empty_elements set ;
cluster STC a₁ -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic programmable standard ;
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 AMI-Struct of a₁;
existence

proof end;

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 natural number ;
func il. c₂,c₃ -> Instruction-Location of a₂ means :Def12: :: AMISTD_1:def 12
ex b₁ being Function of NAT ,the Instruction-Locations of a₂ st
( b₁ is bijective & ( for b₂, b₃ being Nat holds
( b₂ <= b₃ iff b₁ . b₂ <= b₁ . b₃ ) ) & a₄ = b₁ . a₃ );
existence

proof end;

uniqueness by Th17;

end;

:: deftheorem Def12 defines il. AMISTD_1:def 12 :

theorem Th25: :: AMISTD_1:25

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₃, b₄ being natural number st il. b₂,b₃ = il. b₂,b₄ holds
b₃ = b₄

proof end;

theorem Th26: :: AMISTD_1:26

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-Location of b₂ ex b₄ being natural number st b₃ = il. 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 Instruction-Location of c₃;
func locnum c₃ -> natural number means :Def13: :: AMISTD_1:def 13
il. a₂,a₄ = a₃;
existence by Th26;
uniqueness by Th25;

end;

:: deftheorem Def13 defines locnum AMISTD_1:def 13 :

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 Instruction-Location of c₃;
redefine func locnum as locnum c₃ -> Nat;
coherence by ORDINAL2:def 21;

end;

theorem Th27: :: AMISTD_1:27

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₃, b₄ being Instruction-Location of b₂ st locnum b₃ = locnum b₄ holds
b₃ = b₄

proof end;

theorem Th28: :: AMISTD_1:28

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₃, b₄ being natural number holds
( il. b₂,b₃ <= il. b₂,b₄ iff b₃ <= b₄ )

proof end;

theorem Th29: :: AMISTD_1:29

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₃, b₄ being Instruction-Location of b₂ holds
( locnum b₃ <= locnum b₄ iff b₃ <= b₄ )

proof end;

theorem Th30: :: AMISTD_1:30

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁ st b₂ is standard holds
b₂ is InsLoc-antisymmetric

proof end;

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 InsLoc-antisymmetric AMI-Struct of a₁;
coherence by Th30;

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 Instruction-Location of c₃;
let c₅ be natural number ;
func c₃ + c₄ -> Instruction-Location of a₂ equals :: AMISTD_1:def 14
il. a₂,((locnum a₃) + a₄);
coherence ;

end;

:: deftheorem Def14 defines + AMISTD_1:def 14 :

theorem Th31: :: AMISTD_1:31

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-Location of b₂ holds b₃ + 0 = b₃ by Def13;

theorem Th32: :: AMISTD_1:32

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₄, b₅ being Instruction-Location of b₃ st b₄ + b₁ = b₅ + b₁ holds
b₄ = b₅

proof end;

theorem Th33: :: AMISTD_1:33

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 Instruction-Location of b₃ holds (locnum b₄) + b₁ = locnum (b₄ + b₁) by Def13;

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 Instruction-Location of c₃;
func NextLoc c₃ -> Instruction-Location of a₂ equals :: AMISTD_1:def 15
a₃ + 1;
coherence ;

end;

:: deftheorem Def15 defines NextLoc AMISTD_1:def 15 :

theorem Th34: :: AMISTD_1:34

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-Location of b₂ holds NextLoc b₃ = il. b₂,((locnum b₃) + 1) ;

theorem Th35: :: AMISTD_1:35

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-Location of b₂ holds b₃ <> NextLoc b₃

proof end;

theorem Th36: :: AMISTD_1:36

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₃, b₄ being Instruction-Location of b₂ st NextLoc b₃ = NextLoc b₄ holds
b₃ = b₄

proof end;

theorem Th37: :: AMISTD_1:37

for b₁ being natural number
for b₂ being with_non-empty_elements set holds il. (STC b₂),b₁ = b₁

proof end;

theorem Th38: :: AMISTD_1:38

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁)
for b₃ being State of (STC b₁) st InsCode b₂ = 1 holds
(Exec b₂,b₃) . (IC (STC b₁)) = NextLoc (IC b₃)

proof end;

theorem Th39: :: AMISTD_1:39

for b₁ being with_non-empty_elements set
for b₂ being Instruction-Location of (STC b₁)
for b₃ being Element of the Instructions of (STC b₁) st InsCode b₃ = 1 holds
NIC b₃,b₂ = {(NextLoc b₂)}

proof end;

theorem Th40: :: AMISTD_1:40

for b₁ being with_non-empty_elements set
for b₂ being Instruction-Location of (STC b₁) holds SUCC b₂ = {b₂,(NextLoc 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 Instruction of c₃;
attr a₃ is sequential means :: AMISTD_1:def 16
for b₁ being State of a₂ holds (Exec a₃,b₁) . (IC a₂) = NextLoc (IC b₁);

end;

:: deftheorem Def16 defines sequential AMISTD_1:def 16 :

theorem Th41: :: AMISTD_1:41

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

proof end;

theorem Th42: :: AMISTD_1:42

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

proof end;

registration

let c₂ be with_non-empty_elements set ;
let c₃ be non empty non void IC-Ins-separated definite realistic standard AMI-Struct of c₂;
cluster sequential -> non halting Element of the Instructions of a₂;
coherence by Th42;
cluster halting -> non sequential Element of the Instructions of a₂;
coherence by Th42;

end;

theorem Th43: :: AMISTD_1:43

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 not JUMP b₃ is empty holds
not b₃ is sequential

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₄ be FinPartState of c₃;
attr a₃ is closed means :Def17: :: AMISTD_1:def 17
for b₁ being Instruction-Location of a₂ st b₁ in dom a₃ holds
NIC (pi a₃,b₁),b₁ c= dom a₃;
attr a₃ is really-closed means :: AMISTD_1:def 18
for b₁ being State of a₂ st a₃ c= b₁ & IC b₁ in dom a₃ holds
for b₂ being Nat holds IC ((Computation b₁) . b₂) in dom a₃;

end;

:: deftheorem Def17 defines closed AMISTD_1:def 17 :

:: deftheorem Def18 defines really-closed AMISTD_1:def 18 :

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₃;
attr a₃ is para-closed means :: AMISTD_1:def 19
for b₁ being State of a₂ st a₃ c= b₁ & IC b₁ = il. a₂,0 holds
for b₂ being Nat holds IC ((Computation b₁) . b₂) in dom a₃;

end;

:: deftheorem Def19 defines para-closed AMISTD_1:def 19 :

theorem Th44: :: AMISTD_1:44

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of b₁
for b₃ being FinPartState of b₂ st b₃ is really-closed & il. b₂,0 in dom b₃ holds
b₃ is para-closed

proof end;

theorem Th45: :: AMISTD_1:45

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

proof end;

registration

let c₂ be with_non-empty_elements set ;
let c₃ be non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of c₂;
cluster closed -> with_non-empty_elements really-closed FinPartState of a₂;
coherence by Th45;

end;

theorem Th46: :: AMISTD_1:46

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of b₁ holds (il. b₂,0) .--> (halt b₂) is closed

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₄ be FinPartState of c₃;
attr a₃ is lower means :Def20: :: AMISTD_1:def 20
for b₁ being Instruction-Location of a₂ st b₁ in dom a₃ holds
for b₂ being Instruction-Location of a₂ st b₂ <= b₁ holds
b₂ in dom a₃;

end;

:: deftheorem Def20 defines lower AMISTD_1:def 20 :

theorem Th47: :: AMISTD_1:47

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 empty FinPartState of b₂ holds b₃ is lower

proof end;

registration

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

end;

theorem Th48: :: AMISTD_1:48

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 Element of the Instructions of b₂ holds (il. b₂,0) .--> b₃ is lower

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₂;
cluster non empty trivial with_non-empty_elements programmed lower FinPartState of a₂;
existence

proof end;

end;

theorem Th49: :: AMISTD_1:49

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 lower FinPartState of b₂ holds il. b₂,0 in dom b₃

proof end;

theorem Th50: :: AMISTD_1:50

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 lower FinPartState of b₃ holds
( b₁ < card b₄ iff il. b₃,b₁ in dom 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 non empty programmed FinPartState of c₃;
func LastLoc c₃ -> Instruction-Location of a₂ means :Def21: :: AMISTD_1:def 21
ex b₁ being non empty finite natural-membered set st
( b₁ = { (locnum b₂) where B is Element of the Instruction-Locations of a₂ : b₂ in dom a₃ } & a₄ = il. a₂,(max b₁) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :

theorem Th51: :: AMISTD_1:51

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 LastLoc b₃ in dom b₃

proof end;

theorem Th52: :: AMISTD_1:52

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₃, b₄ being non empty programmed FinPartState of b₂ st b₃ c= b₄ holds
LastLoc b₃ <= LastLoc b₄

proof end;

theorem Th53: :: AMISTD_1:53

proof end;

theorem Th54: :: AMISTD_1:54

proof end;

theorem Th55: :: AMISTD_1:55

proof end;

registration

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

proof end;

end;

E54: 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₂;
set c₄ = (il. c₃,0) .--> (halt c₃);
E55: dom ((il. c₃,0) .--> (halt c₃)) = {(il. c₃,0)} by CQC_LANG:5;
then E56: card (dom ((il. c₃,0) .--> (halt c₃))) = 1 by CARD_1:79;
(il. c₃,0) .--> (halt c₃) is lower FinPartState of c₃ by Th48;
then E57: LastLoc ((il. c₃,0) .--> (halt c₃)) = il. c₃,((card ((il. c₃,0) .--> (halt c₃))) -' 1) by Th55
.= il. c₃,((card (dom ((il. c₃,0) .--> (halt c₃)))) -' 1) by PRE_CIRC:21
.= il. c₃,0 by E56, BINARITH:51 ;
hence ((il. c₃,0) .--> (halt c₃)) . (LastLoc ((il. c₃,0) .--> (halt c₃))) = halt c₃ by CQC_LANG:6;
let c₅ be Instruction-Location of c₃;
assume ((il. c₃,0) .--> (halt c₃)) . c₅ = halt c₃ ;
assume c₅ in dom ((il. c₃,0) .--> (halt c₃)) ;
hence c₅ = LastLoc ((il. c₃,0) .--> (halt c₃)) by E55, E57, TARSKI:def 1;

end;

definition