:: AMI_7 semantic presentation

theorem Th1: :: AMI_7:1

for x, y, z being set st x <> y & x <> z holds
{x,y,z} \ {x} = {y,z}

proof end;

theorem Th2: :: AMI_7:2

for N being with_non-empty_elements set
for A being non empty non void AMI-Struct of N
for s being State of A
for o being Object of A holds s . o in ObjectKind o

proof end;

theorem :: AMI_7:3

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite realistic AMI-Struct of N
for s being State of A
for f being Instruction-Location of A
for w being Element of ObjectKind (IC A) holds (s +* (IC A),w) . f = s . f

proof end;

definition

let N be with_non-empty_elements set ;
let A be non empty non void IC-Ins-separated definite AMI-Struct of N;
let s be State of A;
let o be Object of A;
let a be Element of ObjectKind o;
:: original: +*
redefine func s +* o,a -> State of A;
coherence

proof end;

end;

theorem Th4: :: AMI_7:4

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of A
for o being Object of A
for f being Instruction-Location of A
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f

proof end;

theorem Th5: :: AMI_7:5

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st o <> IC A holds
IC s = IC (s +* o,w) by FUNCT_7:34;

theorem Th6: :: AMI_7:6

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))

proof end;

theorem Th7: :: AMI_7:7

proof end;

theorem Th8: :: AMI_7:8

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i

proof end;

definition

let N be set ;
let A be AMI-Struct of N;
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 N be set ;
let A be non empty AMI-Struct of N;
attr A is with_non_trivial_ObjectKinds means :Def2: :: AMI_7:def 2
for o being Object of A holds not ObjectKind o is trivial;

end;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMI_7:def 2 :

registration

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

proof end;

end;

registration

let N 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 N;
coherence

proof end;

end;

registration

let N 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 N;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let A be non empty with_non_trivial_ObjectKinds AMI-Struct of N;
let o be Object of A;
cluster ObjectKind o -> non trivial ;
coherence by Def2;

end;

registration

let N be with_non-empty_elements set ;
let A be with_non_trivial_Instructions AMI-Struct of N;
cluster the Instructions of A -> non trivial ;
coherence by Def1;

end;

registration

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

end;

definition

let N be with_non-empty_elements set ;
let A be non empty non void AMI-Struct of N;
let I be Instruction of A;
func Output I -> Subset of A means :Def3: :: AMI_7:def 3
for o being Object of A holds
( o in it iff ex s being State of A st s . o <> (Exec I,s) . o );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Output AMI_7:def 3 :

definition

let N be with_non-empty_elements set ;
let A be non empty non void IC-Ins-separated definite AMI-Struct of N;
let I be Instruction of A;
func Out_\_Inp I -> Subset of A means :Def4: :: AMI_7:def 4
for o being Object of A holds
( o in it iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) );
existence

proof end;

uniqueness

proof end;

func Out_U_Inp I -> Subset of A means :Def5: :: AMI_7:def 5
for o being Object of A holds
( o in it iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a );
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 N be with_non-empty_elements set ;
let A be non empty non void IC-Ins-separated definite AMI-Struct of N;
let I be Instruction of A;
func Input I -> Subset of A equals :: AMI_7:def 6
(Out_U_Inp I) \ (Out_\_Inp I);
coherence ;

end;

:: deftheorem defines Input AMI_7:def 6 :

theorem Th9: :: AMI_7:9

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Out_\_Inp I misses Input I by XBOOLE_1:85;

theorem Th10: :: AMI_7:10

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_\_Inp I c= Output I

proof end;

theorem Th11: :: AMI_7:11

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Output I c= Out_U_Inp I

proof end;

theorem Th12: :: AMI_7:12

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Input I c= Out_U_Inp I by XBOOLE_1:36;

theorem :: AMI_7:13

proof end;

theorem :: AMI_7:14

proof end;

theorem Th15: :: AMI_7:15

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Out_U_Inp I

proof end;

theorem :: AMI_7:16

proof end;

theorem :: AMI_7:17

proof end;

theorem Th18: :: AMI_7:18

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds
( I is halting iff Output I is empty )

proof end;

theorem Th19: :: AMI_7:19

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_\_Inp I is empty

proof end;

theorem Th20: :: AMI_7:20

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_U_Inp I is empty

proof end;

theorem Th21: :: AMI_7:21

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Input I is empty

proof end;

registration

let N be with_non-empty_elements set ;
let A be non empty non void halting IC-Ins-separated definite AMI-Struct of N;
let I be halting Instruction of A;
cluster Input I -> empty ;
coherence by Th21;
cluster Output I -> empty ;
coherence by Th18;
cluster Out_U_Inp I -> empty ;
coherence by Th20;

end;

registration

let N be with_non-empty_elements set ;
let A be non empty non void halting IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N;
let I be halting Instruction of A;
cluster Out_\_Inp I -> empty ;
coherence by Th19;

end;

theorem Th22: :: AMI_7:22

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of N
for f being Instruction-Location of A
for I being Instruction of A holds not f in Out_\_Inp I

proof end;

theorem Th23: :: AMI_7:23

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
not IC A in Out_\_Inp I

proof end;

theorem Th24: :: AMI_7:24

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st ex s being State of A st (Exec I,s) . (IC A) <> IC s holds
IC A in Output I by Def3;

theorem Th25: :: AMI_7:25

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
IC A in Output I

proof end;

theorem Th26: :: AMI_7:26

proof end;

theorem Th27: :: AMI_7:27

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
IC A in Out_U_Inp I

proof end;

theorem Th28: :: AMI_7:28

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for f being Instruction-Location of A
for I being Instruction of A st ( for s being State of A
for p being programmed FinPartState of A holds Exec I,(s +* p) = (Exec I,s) +* p ) holds
not f in Out_U_Inp I

proof end;

theorem :: AMI_7:29

for N being with_non-empty_elements set
for A being non empty non void IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st I is jump-only & o in Output I holds
o = IC A

proof end;

theorem Th30: :: AMI_7:30

for a being Data-Location
for s being State of SCM
for w being Element of ObjectKind (IC SCM ) holds (s +* (IC SCM ),w) . a = s . a

proof end;

theorem Th31: :: AMI_7:31

for f being Instruction-Location of SCM holds f <> Next f

proof end;

definition

let s be State of SCM ;
let dl be Data-Location ;
let k be Integer;
:: original: +*
redefine func s +* dl,k -> State of SCM ;
coherence

proof end;

end;

consider t being State of SCM ;

Lm1: dom t = the carrier of SCM
by AMI_3:36;

Lm2: for l being Data-Location
for i being Integer holds i is Element of ObjectKind l

proof end;

registration

cluster SCM -> with_non_trivial_Instructions with_non_trivial_ObjectKinds ;
coherence

proof end;

end;

theorem Th32: :: AMI_7:32

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

proof end;

theorem Th33: :: AMI_7:33

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

proof end;

theorem Th34: :: AMI_7:34

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

proof end;

theorem Th35: :: AMI_7:35

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

proof end;

theorem Th36: :: AMI_7:36

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

proof end;

theorem Th37: :: AMI_7:37

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

proof end;

theorem Th38: :: AMI_7:38

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

proof end;

theorem Th39: :: AMI_7:39

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

proof end;

theorem Th40: :: AMI_7:40

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

proof end;

consider q being State of SCM ;

Lm3: dom q = the carrier of SCM
by AMI_3:36;

theorem Th41: :: AMI_7:41

for a being Data-Location
for f being Instruction-Location of SCM holds Out_\_Inp (a =0_goto f) = {}

proof end;

theorem Th42: :: AMI_7:42

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

proof end;

theorem :: AMI_7:43

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

proof end;

theorem Th44: :: AMI_7:44

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

proof end;

theorem Th45: :: AMI_7:45

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

proof end;

theorem Th46: :: AMI_7:46

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

proof end;

theorem Th47: :: AMI_7:47

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

proof end;

theorem Th48: :: AMI_7:48

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

proof end;

theorem Th49: :: AMI_7:49

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

proof end;

theorem Th50: :: AMI_7:50

for a being Data-Location
for f being Instruction-Location of SCM holds Output (a =0_goto f) = {(IC SCM )}

proof end;

theorem Th51: :: AMI_7:51

for a being Data-Location
for f being Instruction-Location of SCM holds Output (a >0_goto f) = {(IC SCM )}

proof end;

theorem Th52: :: AMI_7:52

for f being Instruction-Location of SCM
for I being Instruction of SCM holds not f in Out_U_Inp I

proof end;

theorem Th53: :: AMI_7:53

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

proof end;

theorem Th54: :: AMI_7:54

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

proof end;

theorem Th55: :: AMI_7:55

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

proof end;

theorem Th56: :: AMI_7:56

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

proof end;

theorem Th57: :: AMI_7:57

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

proof end;

theorem Th58: :: AMI_7:58

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

proof end;

theorem Th59: :: AMI_7:59

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

proof end;

theorem Th60: :: AMI_7:60

for a being Data-Location
for f being Instruction-Location of SCM holds Out_U_Inp (a =0_goto f) = {a,(IC SCM )}

proof end;

theorem Th61: :: AMI_7:61

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

proof end;

theorem :: AMI_7:62

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

proof end;

theorem :: AMI_7:63

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

proof end;

theorem :: AMI_7:64

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

proof end;

theorem :: AMI_7:65

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

proof end;

theorem :: AMI_7:66

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

proof end;

theorem :: AMI_7:67

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

proof end;

theorem :: AMI_7:68

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

proof end;

theorem :: AMI_7:69

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

proof end;

theorem :: AMI_7:70

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

proof end;

theorem :: AMI_7:71

for a being Data-Location
for f being Instruction-Location of SCM holds Input (a =0_goto f) = {a,(IC SCM )}

proof end;

theorem :: AMI_7:72

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

proof end;