:: AMI_7 semantic presentation

theorem Th1: :: AMI_7:1

for b₁, b₂, b₃ being set st b₁ <> b₂ & b₁ <> b₃ holds
{b₁,b₂,b₃} \ {b₁} = {b₂,b₃}

proof end;

theorem Th2: :: AMI_7:2

for b₁ being with_non-empty_elements set
for b₂ being non empty non void AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Object of b₂ holds b₃ . b₄ in ObjectKind b₄

proof end;

theorem Th3: :: AMI_7:3

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 State of b₂
for b₄ being Instruction-Location of b₂
for b₅ being Element of ObjectKind (IC b₂) holds (b₃ +* (IC b₂),b₅) . 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₃ be State of c₂;
let c₄ be Object of c₂;
let c₅ be Element of ObjectKind c₄;
redefine func +* as c₃ +* c₄,c₅ -> State of a₂;
coherence

proof end;

end;

theorem Th4: :: AMI_7:4

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 State of b₂
for b₄ being Object of b₂
for b₅ being Instruction-Location of b₂
for b₆ being Instruction of b₂
for b₇ being Element of ObjectKind b₄ st b₅ <> b₄ holds
(Exec b₆,b₃) . b₅ = (Exec b₆,(b₃ +* b₄,b₇)) . b₅

proof end;

theorem Th5: :: AMI_7:5

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 State of b₂
for b₄ being Object of b₂
for b₅ being Element of ObjectKind b₄ st b₄ <> IC b₂ holds
IC b₃ = IC (b₃ +* b₄,b₅) by FUNCT_7:34;

theorem Th6: :: AMI_7:6

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₂
for b₄ being State of b₂
for b₅ being Object of b₂
for b₆ being Element of ObjectKind b₅ st b₃ is sequential & b₅ <> IC b₂ holds
IC (Exec b₃,b₄) = IC (Exec b₃,(b₄ +* b₅,b₆))

proof end;

theorem Th7: :: AMI_7:7

proof end;

theorem Th8: :: AMI_7:8

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 Instruction of b₂
for b₄ being State of b₂
for b₅ being Object of b₂
for b₆ being Element of ObjectKind b₅
for b₇ being Instruction-Location of b₂ holds (Exec b₃,(b₄ +* b₅,b₆)) . b₇ = ((Exec b₃,b₄) +* b₅,b₆) . b₇

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is with_non_trivial_Instructions means :Def1: :: AMI_7:def 1
not the Instructions of a₂ is trivial;

end;

:: deftheorem Def1 defines with_non_trivial_Instructions AMI_7:def 1 :

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
attr a₂ is with_non_trivial_ObjectKinds means :Def2: :: AMI_7:def 2
for b₁ being Object of a₂ holds not ObjectKind b₁ is trivial;

end;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMI_7:def 2 :

registration

let c₁ be with_non-empty_elements set ;
cluster STC a₁ -> with_non_trivial_ObjectKinds ;
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 with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving with_non_trivial_Instructions with_non_trivial_ObjectKinds AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty non void definite with_non_trivial_ObjectKinds -> non empty non void definite with_non_trivial_Instructions AMI-Struct of a₁;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty IC-Ins-separated with_non_trivial_ObjectKinds -> non empty IC-Ins-separated with-non-trivial-Instruction-Locations AMI-Struct of a₁;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty with_non_trivial_ObjectKinds AMI-Struct of c₁;
let c₃ be Object of c₂;
cluster ObjectKind a₃ -> non trivial ;
coherence by Def2;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be with_non_trivial_Instructions AMI-Struct of c₁;
cluster the Instructions of a₂ -> non trivial ;
coherence by Def1;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty IC-Ins-separated with-non-trivial-Instruction-Locations AMI-Struct of c₁;
cluster ObjectKind (IC a₂) -> non trivial ;
coherence by AMI_1:def 11;

end;

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₂;
func Output c₃ -> Subset of a₂ means :Def3: :: AMI_7:def 3
for b₁ being Object of a₂ holds
( b₁ in a₄ iff ex b₂ being State of a₂ st b₂ . b₁ <> (Exec a₃,b₂) . b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Output AMI_7:def 3 :

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₂;
func Out_\_Inp c₃ -> Subset of a₂ means :Def4: :: AMI_7:def 4
for b₁ being Object of a₂ holds
( b₁ in a₄ iff for b₂ being State of a₂
for b₃ being Element of ObjectKind b₁ holds Exec a₃,b₂ = Exec a₃,(b₂ +* b₁,b₃) );
existence

proof end;

uniqueness

proof end;

func Out_U_Inp c₃ -> Subset of a₂ means :Def5: :: AMI_7:def 5
for b₁ being Object of a₂ holds
( b₁ in a₄ iff ex b₂ being State of a₂ex b₃ being Element of ObjectKind b₁ st Exec a₃,(b₂ +* b₁,b₃) <> (Exec a₃,b₂) +* b₁,b₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Out_\_Inp AMI_7:def 4 :

:: deftheorem Def5 defines Out_U_Inp AMI_7:def 5 :

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₂;
func Input c₃ -> Subset of a₂ equals :: AMI_7:def 6
(Out_U_Inp a₃) \ (Out_\_Inp a₃);
coherence ;

end;

:: deftheorem Def6 defines Input AMI_7:def 6 :

theorem Th9: :: AMI_7:9

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 Instruction of b₂ holds Out_\_Inp b₃ misses Input b₃ by XBOOLE_1:85;

theorem Th10: :: AMI_7:10

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of b₁
for b₃ being Instruction of b₂ holds Out_\_Inp b₃ c= Output b₃

proof end;

theorem Th11: :: AMI_7:11

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 Instruction of b₂ holds Output b₃ c= Out_U_Inp b₃

proof end;

theorem Th12: :: AMI_7:12

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 Instruction of b₂ holds Input b₃ c= Out_U_Inp b₃ by XBOOLE_1:36;

theorem Th13: :: AMI_7:13

proof end;

theorem Th14: :: AMI_7:14

proof end;

theorem Th15: :: AMI_7:15

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 Instruction of b₂
for b₄ being Object of b₂ st ObjectKind b₄ is trivial holds
not b₄ in Out_U_Inp b₃

proof end;

theorem Th16: :: AMI_7:16

proof end;

theorem Th17: :: AMI_7:17

proof end;

theorem Th18: :: AMI_7: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 Instruction of b₂ holds
( b₃ is halting iff Output b₃ is empty )

proof end;

theorem Th19: :: AMI_7:19

proof end;

theorem Th20: :: AMI_7:20

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 Instruction of b₂ st b₃ is halting holds
Out_U_Inp b₃ is empty

proof end;

theorem Th21: :: AMI_7:21

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 Instruction of b₂ st b₃ is halting holds
Input 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 AMI-Struct of c₁;
let c₃ be halting Instruction of c₂;
cluster Input a₃ -> empty ;
coherence by Th21;
cluster Output a₃ -> empty ;
coherence by Th18;
cluster Out_U_Inp a₃ -> empty ;
coherence by Th20;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of c₁;
let c₃ be halting Instruction of c₂;
cluster Out_\_Inp a₃ -> empty ;
coherence by Th19;

end;

theorem Th22: :: AMI_7:22

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Instruction of b₂ holds not b₃ in Out_\_Inp b₄

proof end;

theorem Th23: :: AMI_7:23

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 b₃ is sequential holds
not IC b₂ in Out_\_Inp b₃

proof end;

theorem Th24: :: AMI_7:24

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 Instruction of b₂ st ex b₄ being State of b₂ st (Exec b₃,b₄) . (IC b₂) <> IC b₄ holds
IC b₂ in Output b₃ by Def3;

theorem Th25: :: AMI_7:25

proof end;

theorem Th26: :: AMI_7:26

proof end;

theorem Th27: :: AMI_7:27

proof end;

theorem Th28: :: AMI_7:28

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 Instruction-Location of b₂
for b₄ being Instruction of b₂ st ( for b₅ being State of b₂
for b₆ being programmed FinPartState of b₂ holds Exec b₄,(b₅ +* b₆) = (Exec b₄,b₅) +* b₆ ) holds
not b₃ in Out_U_Inp b₄

proof end;

theorem Th29: :: AMI_7:29

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 Instruction of b₂
for b₄ being Object of b₂ st b₃ is jump-only & b₄ in Output b₃ holds
b₄ = IC b₂

proof end;

theorem Th30: :: AMI_7:30

for b₁ being Data-Location
for b₂ being State of SCM
for b₃ being Element of ObjectKind (IC SCM ) holds (b₂ +* (IC SCM ),b₃) . b₁ = b₂ . b₁

proof end;

theorem Th31: :: AMI_7:31

for b₁ being Instruction-Location of SCM holds b₁ <> Next b₁

proof end;

definition

let c₁ be State of SCM ;
let c₂ be Data-Location ;
let c₃ be Integer;
redefine func +* as c₁ +* c₂,c₃ -> State of SCM ;
coherence

proof end;

end;

consider c₁ being State of SCM ;

Lemma31: dom c₁ = the carrier of SCM
by AMI_3:36;

Lemma32: for b₁ being Data-Location
for b₂ being Integer holds b₂ is Element of ObjectKind b₁

proof end;

registration

cluster SCM -> with_non_trivial_Instructions with_non_trivial_ObjectKinds ;
coherence

proof end;

end;

theorem Th32: :: AMI_7:32

for b₁ being Data-Location holds Out_\_Inp (b₁ := b₁) = {}

proof end;

theorem Th33: :: AMI_7:33

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Out_\_Inp (b₁ := b₂) = {b₁}

proof end;

theorem Th34: :: AMI_7:34

for b₁, b₂ being Data-Location holds Out_\_Inp (AddTo b₁,b₂) = {}

proof end;

theorem Th35: :: AMI_7:35

for b₁ being Data-Location holds Out_\_Inp (SubFrom b₁,b₁) = {b₁}

proof end;

theorem Th36: :: AMI_7:36

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Out_\_Inp (SubFrom b₁,b₂) = {}

proof end;

theorem Th37: :: AMI_7:37

for b₁, b₂ being Data-Location holds Out_\_Inp (MultBy b₁,b₂) = {}

proof end;

theorem Th38: :: AMI_7:38

for b₁ being Data-Location holds Out_\_Inp (Divide b₁,b₁) = {b₁}

proof end;

theorem Th39: :: AMI_7:39

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Out_\_Inp (Divide b₁,b₂) = {}

proof end;

theorem Th40: :: AMI_7:40

for b₁ being Instruction-Location of SCM holds Out_\_Inp (goto b₁) = {(IC SCM )}

proof end;

consider c₂ being State of SCM ;

Lemma42: dom c₂ = the carrier of SCM
by AMI_3:36;

theorem Th41: :: AMI_7:41

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Out_\_Inp (b₁ =0_goto b₂) = {}

proof end;

theorem Th42: :: AMI_7:42

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Out_\_Inp (b₁ >0_goto b₂) = {}

proof end;

theorem Th43: :: AMI_7:43

for b₁ being Data-Location holds Output (b₁ := b₁) = {(IC SCM )}

proof end;

theorem Th44: :: AMI_7:44

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Output (b₁ := b₂) = {b₁,(IC SCM )}

proof end;

theorem Th45: :: AMI_7:45

for b₁, b₂ being Data-Location holds Output (AddTo b₁,b₂) = {b₁,(IC SCM )}

proof end;

theorem Th46: :: AMI_7:46

for b₁, b₂ being Data-Location holds Output (SubFrom b₁,b₂) = {b₁,(IC SCM )}

proof end;

theorem Th47: :: AMI_7:47

for b₁, b₂ being Data-Location holds Output (MultBy b₁,b₂) = {b₁,(IC SCM )}

proof end;

theorem Th48: :: AMI_7:48

for b₁, b₂ being Data-Location holds Output (Divide b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th49: :: AMI_7:49

for b₁ being Instruction-Location of SCM holds Output (goto b₁) = {(IC SCM )}

proof end;

theorem Th50: :: AMI_7:50

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Output (b₁ =0_goto b₂) = {(IC SCM )}

proof end;

theorem Th51: :: AMI_7:51

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Output (b₁ >0_goto b₂) = {(IC SCM )}

proof end;

theorem Th52: :: AMI_7:52

for b₁ being Instruction-Location of SCM
for b₂ being Instruction of SCM holds not b₁ in Out_U_Inp b₂

proof end;

theorem Th53: :: AMI_7:53

for b₁ being Data-Location holds Out_U_Inp (b₁ := b₁) = {(IC SCM )}

proof end;

theorem Th54: :: AMI_7:54

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Out_U_Inp (b₁ := b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th55: :: AMI_7:55

for b₁, b₂ being Data-Location holds Out_U_Inp (AddTo b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th56: :: AMI_7:56

for b₁, b₂ being Data-Location holds Out_U_Inp (SubFrom b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th57: :: AMI_7:57

for b₁, b₂ being Data-Location holds Out_U_Inp (MultBy b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th58: :: AMI_7:58

for b₁, b₂ being Data-Location holds Out_U_Inp (Divide b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th59: :: AMI_7:59

for b₁ being Instruction-Location of SCM holds Out_U_Inp (goto b₁) = {(IC SCM )}

proof end;

theorem Th60: :: AMI_7:60

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Out_U_Inp (b₁ =0_goto b₂) = {b₁,(IC SCM )}

proof end;

theorem Th61: :: AMI_7:61

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Out_U_Inp (b₁ >0_goto b₂) = {b₁,(IC SCM )}

proof end;

theorem Th62: :: AMI_7:62

for b₁ being Data-Location holds Input (b₁ := b₁) = {(IC SCM )}

proof end;

theorem Th63: :: AMI_7:63

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Input (b₁ := b₂) = {b₂,(IC SCM )}

proof end;

theorem Th64: :: AMI_7:64

for b₁, b₂ being Data-Location holds Input (AddTo b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th65: :: AMI_7:65

for b₁ being Data-Location holds Input (SubFrom b₁,b₁) = {(IC SCM )}

proof end;

theorem Th66: :: AMI_7:66

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Input (SubFrom b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th67: :: AMI_7:67

for b₁, b₂ being Data-Location holds Input (MultBy b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th68: :: AMI_7:68

for b₁ being Data-Location holds Input (Divide b₁,b₁) = {(IC SCM )}

proof end;

theorem Th69: :: AMI_7:69

for b₁, b₂ being Data-Location st b₁ <> b₂ holds
Input (Divide b₁,b₂) = {b₁,b₂,(IC SCM )}

proof end;

theorem Th70: :: AMI_7:70

for b₁ being Instruction-Location of SCM holds Input (goto b₁) = {}

proof end;

theorem Th71: :: AMI_7:71

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Input (b₁ =0_goto b₂) = {b₁,(IC SCM )}

proof end;

theorem Th72: :: AMI_7:72

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds Input (b₁ >0_goto b₂) = {b₁,(IC SCM )}

proof end;