:: AMI_3 semantic presentation

definition

func SCM -> strict AMI-Struct of {INT } equals :: AMI_3:def 1
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #);
coherence ;

end;

:: deftheorem defines SCM AMI_3:def 1 :

registration

cluster SCM -> non empty strict non void ;
coherence by AMI_1:def 3, STRUCT_0:def 1;

end;

theorem Th1: :: AMI_3:1

SCM is data-oriented

proof end;

theorem Th2: :: AMI_3:2

SCM is definite

proof end;

registration

cluster SCM -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence

proof end;

end;

definition

mode Data-Location -> Object of SCM means :Def2: :: AMI_3:def 2
it in SCM-Data-Loc ;
existence

proof end;

end;

:: deftheorem Def2 defines Data-Location AMI_3:def 2 :

definition

let s be State of SCM ;
let d be Data-Location ;
:: original: .
redefine func s . d -> Integer;
coherence

proof end;

end;

definition

let a, b be Data-Location ;
func a := b -> Instruction of SCM equals :: AMI_3:def 3
[1,<*a,b*>];
correctness

proof end;

func AddTo a,b -> Instruction of SCM equals :: AMI_3:def 4
[2,<*a,b*>];
correctness

proof end;

func SubFrom a,b -> Instruction of SCM equals :: AMI_3:def 5
[3,<*a,b*>];
correctness

proof end;

func MultBy a,b -> Instruction of SCM equals :: AMI_3:def 6
[4,<*a,b*>];
correctness

proof end;

func Divide a,b -> Instruction of SCM equals :: AMI_3:def 7
[5,<*a,b*>];
correctness

proof end;

end;

:: deftheorem defines := AMI_3:def 3 :

:: deftheorem defines AddTo AMI_3:def 4 :

:: deftheorem defines SubFrom AMI_3:def 5 :

:: deftheorem defines MultBy AMI_3:def 6 :

:: deftheorem defines Divide AMI_3:def 7 :

definition

let loc be Instruction-Location of SCM ;
func goto loc -> Instruction of SCM equals :: AMI_3:def 8
[6,<*loc*>];
correctness by AMI_2:3;
let a be Data-Location ;
func a =0_goto loc -> Instruction of SCM equals :: AMI_3:def 9
[7,<*loc,a*>];
correctness

proof end;

func a >0_goto loc -> Instruction of SCM equals :: AMI_3:def 10
[8,<*loc,a*>];
correctness

proof end;

end;

:: deftheorem defines goto AMI_3:def 8 :

:: deftheorem defines =0_goto AMI_3:def 9 :

:: deftheorem defines >0_goto AMI_3:def 10 :

theorem :: AMI_3:3

canceled;

theorem :: AMI_3:4

IC SCM = 0 ;

theorem Th5: :: AMI_3:5

for s being State of SCM
for S being SCM-State st S = s holds
IC s = IC S by AMI_2:def 6;

definition

let loc be Instruction-Location of SCM ;
func Next loc -> Instruction-Location of SCM means :Def11: :: AMI_3:def 11
ex mj being Element of SCM-Instr-Loc st
( mj = loc & it = Next mj );
existence

proof end;

correctness ;

end;

:: deftheorem Def11 defines Next AMI_3:def 11 :

theorem Th6: :: AMI_3:6

for loc being Instruction-Location of SCM
for mj being Element of SCM-Instr-Loc st mj = loc holds
Next mj = Next loc by Def11;

theorem Th7: :: AMI_3:7

for I being Instruction of SCM
for s being State of SCM
for i being Element of SCM-Instr st i = I holds
for S being SCM-State st S = s holds
Exec I,s = SCM-Exec-Res i,S by AMI_2:def 17;

theorem Th8: :: AMI_3:8

for a, b being Data-Location
for s being State of SCM holds
( (Exec (a := b),s) . (IC SCM ) = Next (IC s) & (Exec (a := b),s) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec (a := b),s) . c = s . c ) )

proof end;

theorem Th9: :: AMI_3:9

for a, b being Data-Location
for s being State of SCM holds
( (Exec (AddTo a,b),s) . (IC SCM ) = Next (IC s) & (Exec (AddTo a,b),s) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec (AddTo a,b),s) . c = s . c ) )

proof end;

theorem Th10: :: AMI_3:10

for a, b being Data-Location
for s being State of SCM holds
( (Exec (SubFrom a,b),s) . (IC SCM ) = Next (IC s) & (Exec (SubFrom a,b),s) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec (SubFrom a,b),s) . c = s . c ) )

proof end;

theorem Th11: :: AMI_3:11

for a, b being Data-Location
for s being State of SCM holds
( (Exec (MultBy a,b),s) . (IC SCM ) = Next (IC s) & (Exec (MultBy a,b),s) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec (MultBy a,b),s) . c = s . c ) )

proof end;

theorem Th12: :: AMI_3:12

for a, b being Data-Location
for s being State of SCM holds
( (Exec (Divide a,b),s) . (IC SCM ) = Next (IC s) & ( a <> b implies (Exec (Divide a,b),s) . a = (s . a) div (s . b) ) & (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) )

proof end;

theorem :: AMI_3:13

for c being Data-Location
for loc being Instruction-Location of SCM
for s being State of SCM holds
( (Exec (goto loc),s) . (IC SCM ) = loc & (Exec (goto loc),s) . c = s . c )

proof end;

theorem Th14: :: AMI_3:14

for a, c being Data-Location
for loc being Instruction-Location of SCM
for s being State of SCM holds
( ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = Next (IC s) ) & (Exec (a =0_goto loc),s) . c = s . c )

proof end;

theorem Th15: :: AMI_3:15

for a, c being Data-Location
for loc being Instruction-Location of SCM
for s being State of SCM holds
( ( s . a > 0 implies (Exec (a >0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <= 0 implies (Exec (a >0_goto loc),s) . (IC SCM ) = Next (IC s) ) & (Exec (a >0_goto loc),s) . c = s . c )

proof end;

Lm1: for I being Instruction of SCM st ex s being State of SCM st (Exec I,s) . (IC SCM ) = Next (IC s) holds
not I is halting

proof end;

Lm2: for I being Instruction of SCM st I = [0,{} ] holds
I is halting

proof end;

Lm3: for a, b being Data-Location holds not a := b is halting

proof end;

Lm4: for a, b being Data-Location holds not AddTo a,b is halting

proof end;

Lm5: for a, b being Data-Location holds not SubFrom a,b is halting

proof end;

Lm6: for a, b being Data-Location holds not MultBy a,b is halting

proof end;

Lm7: for a, b being Data-Location holds not Divide a,b is halting

proof end;

Lm8: for loc being Instruction-Location of SCM holds not goto loc is halting

proof end;

Lm9: for a being Data-Location
for loc being Instruction-Location of SCM holds not a =0_goto loc is halting

proof end;

Lm10: for a being Data-Location
for loc being Instruction-Location of SCM holds not a >0_goto loc is halting

proof end;

Lm11: for I being set holds
( I is Instruction of SCM iff ( I = [0,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) )

proof end;

registration

cluster SCM -> non empty strict non void halting IC-Ins-separated data-oriented definite ;
coherence

proof end;

end;

Lm12: for I being Instruction of SCM st I is halting holds
I = halt SCM

proof end;

Lm13: halt SCM = [0,{} ]

proof end;

theorem :: AMI_3:16

canceled;

theorem :: AMI_3:17

canceled;

theorem Th18: :: AMI_3:18

for m, j being Integer holds m * j,0 are_congruent_mod m

proof end;

scheme :: AMI_3:sch 1
INDI{ F₁() -> Nat, F₂() -> Nat, P₁[ set ] } :

P₁[F₂()]

provided

A1: P₁[0] and
A2: F₁() > 0 and
A3: for i, j being Nat st P₁[F₁() * i] & j <> 0 & j <= F₁() holds
P₁[(F₁() * i) + j]

proof end;

theorem Th19: :: AMI_3:19

for X, Y being non empty set
for f, g being PartFunc of X,Y st ( for x being Element of X
for y being Element of Y holds
( [x,y] in f iff [x,y] in g ) ) holds
f = g

proof end;

Lm14: for f, g being Function
for A, B being set st f | A = g | A & f | B = g | B holds
f | (A \/ B) = g | (A \/ B)
by RELAT_1:185;

Lm15: for f being Function
for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
by GRFUNC_1:89;

Lm16: for f being Function
for X being set st X misses dom f holds
f | X = {}
by RELAT_1:95;

theorem :: AMI_3:20

canceled;

theorem :: AMI_3:21

canceled;

theorem :: AMI_3:22

canceled;

theorem :: AMI_3:23

canceled;

theorem Th24: :: AMI_3:24

for f, g being Function
for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}

proof end;

theorem Th25: :: AMI_3:25

for f, g being Function
for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}

proof end;

theorem :: AMI_3:26

for f, g being Function
for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}

proof end;

theorem Th27: :: AMI_3:27

for a, b being set
for f being Function st a in dom f & f . a = b holds
a .--> b c= f

proof end;

theorem :: AMI_3:28

canceled;

theorem :: AMI_3:29

for a, b, c, d being set
for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
a,c --> b,d c= f

proof end;

theorem :: AMI_3:30

canceled;

theorem Th31: :: AMI_3:31

for N being set
for S being AMI-Struct of N
for p being FinPartState of S holds p in FinPartSt S

proof end;

registration

let N be set ;
let S be AMI-Struct of N;
cluster FinPartSt S -> non empty ;
coherence by Th31;

end;

theorem Th32: :: AMI_3:32

for N being set
for S being AMI-Struct of N
for p being Element of FinPartSt S holds p is FinPartState of S

proof end;

theorem Th33: :: AMI_3:33

for N being set
for S being AMI-Struct of N
for F1, F2 being PartFunc of FinPartSt S, FinPartSt S st ( for p, q being FinPartState of S holds
( [p,q] in F1 iff [p,q] in F2 ) ) holds
F1 = F2

proof end;

scheme :: AMI_3:sch 2
EqFPSFunc{ F₁() -> non empty with_non-empty_elements set , F₂() -> AMI-Struct of F₁(), P₁[ set , set ], F₃() -> PartFunc of FinPartSt F₂(), FinPartSt F₂(), F₄() -> PartFunc of FinPartSt F₂(), FinPartSt F₂() } :

F₃() = F₄()

provided

A1: for p, q being FinPartState of F₂() holds
( [p,q] in F₃() iff P₁[p,q] ) and
A2: for p, q being FinPartState of F₂() holds
( [p,q] in F₄() iff P₁[p,q] )

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let l be Instruction-Location of S;
func Start-At l -> FinPartState of S equals :: AMI_3:def 12
(IC S) .--> l;
correctness

proof end;

end;

:: deftheorem defines Start-At AMI_3:def 12 :

theorem :: AMI_3:34

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for l being Instruction-Location of S holds dom (Start-At l) = {(IC S)}

proof end;

definition

let N be set ;
let S be AMI-Struct of N;
let IT be FinPartState of S;
attr IT is programmed means :Def13: :: AMI_3:def 13
dom IT c= the Instruction-Locations of S;

end;

:: deftheorem Def13 defines programmed AMI_3:def 13 :

registration

let N be set ;
let S be AMI-Struct of N;
cluster programmed FinPartState of S;
existence

proof end;

end;

theorem :: AMI_3:35

for N being set
for S being AMI-Struct of N
for p1, p2 being programmed FinPartState of S holds p1 +* p2 is programmed

proof end;

theorem Th36: :: AMI_3:36

for N being with_non-empty_elements set
for S being non void AMI-Struct of N
for s being State of S holds dom s = the carrier of S

proof end;

theorem Th37: :: AMI_3:37

for N being with_non-empty_elements set
for S being AMI-Struct of N
for p being FinPartState of S holds dom p c= the carrier of S

proof end;

theorem :: AMI_3:38

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being programmed FinPartState of S
for s being State of S st p c= s holds
for k being Nat holds p c= (Computation s) . k

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated AMI-Struct of N;
let s be State of S;
let l be Instruction-Location of S;
pred s starts_at l means :: AMI_3:def 14
IC s = l;

end;

:: deftheorem defines starts_at AMI_3:def 14 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated AMI-Struct of N;
let s be State of S;
let l be Instruction-Location of S;
pred s halts_at l means :Def15: :: AMI_3:def 15
s . l = halt S;

end;

:: deftheorem Def15 defines halts_at AMI_3:def 15 :

theorem Th39: :: AMI_3:39

for N being with_non-empty_elements set
for S being non void AMI-Struct of N
for p being FinPartState of S ex s being State of S st p c= s

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let p be FinPartState of S;
assume A1: IC S in dom p ;
func IC p -> Instruction-Location of S equals :Def16: :: AMI_3:def 16
p . (IC S);
coherence

proof end;

end;

:: deftheorem Def16 defines IC AMI_3:def 16 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let p be FinPartState of S;
let l be Instruction-Location of S;
pred p starts_at l means :: AMI_3:def 17
( IC S in dom p & IC p = l );

end;

:: deftheorem defines starts_at AMI_3:def 17 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite AMI-Struct of N;
let p be FinPartState of S;
let l be Instruction-Location of S;
pred p halts_at l means :: AMI_3:def 18
( l in dom p & p . l = halt S );

end;

:: deftheorem defines halts_at AMI_3:def 18 :

theorem Th40: :: AMI_3:40

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S holds
( s is halting iff ex k being Nat st s halts_at IC ((Computation s) . k) )

proof end;

theorem :: AMI_3:41

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s halts_at l

proof end;

theorem Th42: :: AMI_3:42

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Nat st s is halting holds
( Result s = (Computation s) . k iff s halts_at IC ((Computation s) . k) )

proof end;

theorem :: AMI_3:43

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for p being programmed FinPartState of S
for k being Nat holds
( p c= s iff p c= (Computation s) . k )

proof end;

theorem Th44: :: AMI_3:44

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Nat st s halts_at IC ((Computation s) . k) holds
Result s = (Computation s) . k

proof end;

theorem Th45: :: AMI_3:45

for i, j being Nat
for N being with_non-empty_elements set st i <= j holds
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S st s halts_at IC ((Computation s) . i) holds
s halts_at IC ((Computation s) . j)

proof end;

theorem :: AMI_3:46

proof end;

theorem :: AMI_3:47

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S st ex k being Nat st s halts_at IC ((Computation s) . k) holds
for i being Nat holds Result s = Result ((Computation s) . i)

proof end;

theorem :: AMI_3:48

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for l being Instruction-Location of S
for k being Nat holds
( s halts_at l iff (Computation s) . k halts_at l )

proof end;

theorem :: AMI_3:49

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for p being FinPartState of S
for l being Instruction-Location of S st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l

proof end;

theorem :: AMI_3:50

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for l being Instruction-Location of S holds (Start-At l) . (IC S) = l by CQC_LANG:6;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let l be Instruction-Location of S;
let I be Element of the Instructions of S;
:: original: .-->
redefine func l .--> I -> programmed FinPartState of S;
coherence

proof end;

end;

Lm17: for s being State of SCM
for i being Instruction of SCM
for l being Instruction-Location of SCM holds (Exec i,s) . l = s . l

proof end;

theorem :: AMI_3:51

SCM is realistic by AMI_1:def 21, AMI_2:6;

registration

cluster SCM -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence

proof end;

end;

definition

let k be natural number ;
func dl. k -> Data-Location equals :: AMI_3:def 19
(2 * k) + 1;
coherence

proof end;

func il. k -> Instruction-Location of SCM equals :: AMI_3:def 20
(2 * k) + 2;
coherence

proof end;

end;

:: deftheorem defines dl. AMI_3:def 19 :

:: deftheorem defines il. AMI_3:def 20 :

theorem :: AMI_3:52

for i, j being natural number st i <> j holds
dl. i <> dl. j

proof end;

theorem :: AMI_3:53

for i, j being natural number st i <> j holds
il. i <> il. j

proof end;

theorem :: AMI_3:54

for k being natural number holds Next (il. k) = il. (k + 1)

proof end;

theorem Th55: :: AMI_3:55

for l being Data-Location holds ObjectKind l = INT

proof end;

definition

let la be Data-Location ;
let a be Integer;
:: original: .-->
redefine func la .--> a -> FinPartState of SCM ;
coherence

proof end;

end;

definition

let la, lb be Data-Location ;
let a, b be Integer;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of SCM ;
coherence

proof end;

end;

theorem :: AMI_3:56

for i, j being natural number holds dl. i <> il. j

proof end;

theorem :: AMI_3:57

for i being natural number holds
( IC SCM <> dl. i & IC SCM <> il. i ) ;

theorem :: AMI_3:58

for I being Instruction of SCM st ex s being State of SCM st (Exec I,s) . (IC SCM ) = Next (IC s) holds
not I is halting by Lm1;

theorem :: AMI_3:59

for I being Instruction of SCM st I = [0,{} ] holds
I is halting by Lm2;

theorem :: AMI_3:60

for a, b being Data-Location holds not a := b is halting by Lm3;

theorem :: AMI_3:61

for a, b being Data-Location holds not AddTo a,b is halting by Lm4;

theorem :: AMI_3:62

for a, b being Data-Location holds not SubFrom a,b is halting by Lm5;

theorem :: AMI_3:63

for a, b being Data-Location holds not MultBy a,b is halting by Lm6;

theorem :: AMI_3:64

for a, b being Data-Location holds not Divide a,b is halting by Lm7;

theorem :: AMI_3:65

for loc being Instruction-Location of SCM holds not goto loc is halting by Lm8;

theorem :: AMI_3:66

for a being Data-Location
for loc being Instruction-Location of SCM holds not a =0_goto loc is halting by Lm9;

theorem :: AMI_3:67

for a being Data-Location
for loc being Instruction-Location of SCM holds not a >0_goto loc is halting by Lm10;

theorem :: AMI_3:68

[0,{} ] is Instruction of SCM by AMI_2:2;

theorem :: AMI_3:69

for I being set holds
( I is Instruction of SCM iff ( I = [0,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) ) by Lm11;

theorem :: AMI_3:70

for I being Instruction of SCM st I is halting holds
I = halt SCM by Lm12;

theorem :: AMI_3:71

halt SCM = [0,{} ] by Lm13;