:: SCMPDS_9 semantic presentation

theorem Th1: :: SCMPDS_9:1

for r being real number holds 0 <= r + (abs r)

proof end;

theorem Th2: :: SCMPDS_9:2

for r being real number holds 0 <= (- r) + (abs r)

proof end;

theorem Th3: :: SCMPDS_9:3

for r, s being real number holds
( not abs r = abs s or r = s or r = - s )

proof end;

theorem Th4: :: SCMPDS_9:4

for i, j being natural number st i < j & i <> 0 holds
not i / j is integer

proof end;

theorem Th5: :: SCMPDS_9:5

not { (2 * k) where k is Nat : k > 1 } is finite

proof end;

theorem Th6: :: SCMPDS_9:6

for f being Function
for a, b, c being set st a <> c holds
(f +* (a .--> b)) . c = f . c

proof end;

theorem Th7: :: SCMPDS_9:7

for f being Function
for a, b, c, d being set st a <> b holds
( (f +* (a,b --> c,d)) . a = c & (f +* (a,b --> c,d)) . b = d )

proof end;

Lm1: for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of S
for i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following s)

proof end;

definition

let la, lb be Int_position ;
let a, b be Integer;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of SCMPDS ;
coherence

proof end;

end;

registration

cluster SCMPDS -> with-non-trivial-Instruction-Locations ;
coherence

proof end;

end;

definition

let l be Instruction-Location of SCMPDS ;
func locnum l -> natural number means :Def1: :: SCMPDS_9:def 1
il. it = l;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines locnum SCMPDS_9:def 1 :

definition

let l be Instruction-Location of SCMPDS ;
:: original: locnum
redefine func locnum l -> Nat;
coherence by ORDINAL2:def 21;

end;

theorem Th8: :: SCMPDS_9:8

for l being Instruction-Location of SCMPDS holds l = (2 * (locnum l)) + 2

proof end;

theorem :: SCMPDS_9:9

for l1, l2 being Instruction-Location of SCMPDS st l1 <> l2 holds
locnum l1 <> locnum l2

proof end;

theorem Th10: :: SCMPDS_9:10

for l1, l2 being Instruction-Location of SCMPDS st l1 <> l2 holds
Next l1 <> Next l2

proof end;

theorem Th11: :: SCMPDS_9:11

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for i being Instruction of S
for l being Instruction-Location of S holds JUMP i c= NIC i,l

proof end;

theorem Th12: :: SCMPDS_9:12

for i being Instruction of SCMPDS
for l being Instruction-Location of SCMPDS st ( for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = Next (IC s) ) holds
NIC i,l = {(Next l)}

proof end;

theorem Th13: :: SCMPDS_9:13

for i being Instruction of SCMPDS st ( for l being Instruction-Location of SCMPDS holds NIC i,l = {(Next l)} ) holds
JUMP i is empty

proof end;

theorem Th14: :: SCMPDS_9:14

for l being Instruction-Location of SCMPDS
for k being Integer holds NIC (goto k),l = {((2 * (abs (k + (locnum l)))) + 2)}

proof end;

Lm2: for k being natural number st k > 1 holds
k - 2 is Nat

proof end;

theorem Th15: :: SCMPDS_9:15

for a being Int_position
for l being Instruction-Location of SCMPDS holds NIC (return a),l = { (2 * k) where k is Nat : k > 1 }

proof end;

theorem Th16: :: SCMPDS_9:16

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1 being Integer holds NIC (saveIC a,k1),l = {(Next l)}

proof end;

theorem Th17: :: SCMPDS_9:17

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1 being Integer holds NIC (a := k1),l = {(Next l)}

proof end;

theorem Th18: :: SCMPDS_9:18

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 := k2),l = {(Next l)}

proof end;

theorem Th19: :: SCMPDS_9:19

for a, b being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 := b,k2),l = {(Next l)}

proof end;

theorem Th20: :: SCMPDS_9:20

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (AddTo a,k1,k2),l = {(Next l)}

proof end;

theorem Th21: :: SCMPDS_9:21

for a, b being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (AddTo a,k1,b,k2),l = {(Next l)}

proof end;

theorem Th22: :: SCMPDS_9:22

for a, b being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (SubFrom a,k1,b,k2),l = {(Next l)}

proof end;

theorem Th23: :: SCMPDS_9:23

for a, b being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (MultBy a,k1,b,k2),l = {(Next l)}

proof end;

theorem Th24: :: SCMPDS_9:24

for a, b being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (Divide a,k1,b,k2),l = {(Next l)}

proof end;

theorem :: SCMPDS_9:25

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 <>0_goto k2),l = {(Next l),((abs (2 * (k2 + (locnum l)))) + 2)}

proof end;

theorem :: SCMPDS_9:26

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 <=0_goto k2),l = {(Next l),((abs (2 * (k2 + (locnum l)))) + 2)}

proof end;

theorem :: SCMPDS_9:27

for a being Int_position
for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 >=0_goto k2),l = {(Next l),((abs (2 * (k2 + (locnum l)))) + 2)}

proof end;

Lm3: for k being Integer holds JUMP (goto k) = {}

proof end;

registration

let k be Integer;
cluster JUMP (goto k) -> empty ;
coherence by Lm3;

end;

theorem Th28: :: SCMPDS_9:28

for a being Int_position holds JUMP (return a) = { (2 * k) where k is Nat : k > 1 }

proof end;

registration

let a be Int_position ;
cluster JUMP (return a) -> infinite ;
coherence by Th5, Th28;

end;

registration

let a be Int_position ;
let k1 be Integer;
cluster JUMP (saveIC a,k1) -> empty ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1 be Integer;
cluster JUMP (a := k1) -> empty ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster JUMP (a,k1 := k2) -> empty ;
coherence

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster JUMP (a,k1 := b,k2) -> empty ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster JUMP (AddTo a,k1,k2) -> empty ;
coherence

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster JUMP (AddTo a,k1,b,k2) -> empty ;
coherence

proof end;

cluster JUMP (SubFrom a,k1,b,k2) -> empty ;
coherence

proof end;

cluster JUMP (MultBy a,k1,b,k2) -> empty ;
coherence

proof end;

cluster JUMP (Divide a,k1,b,k2) -> empty ;
coherence

proof end;

end;

Lm4: not 5 / 3 is integer

proof end;

Lm5: for a being real number st a > 0 holds
- ((2 * a) + (1 + a)) < - 0

proof end;

Lm6: for d being real number holds (((2 * ((abs d) + (((- d) + (abs d)) + 4))) + 2) - 2) + (2 * d) <> - ((((2 * (((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) + 2) - 2) + (2 * d))

proof end;

Lm7: for b, d being real number holds (2 * b) + 2 <> (2 * b) + ((2 * (((- d) + (abs d)) + 4)) + (2 * d))

proof end;

Lm8: for c, d being real number st c > 0 holds
(2 * ((abs d) + c)) + 2 <> - (((2 * ((abs d) + c)) + (2 * c)) + (2 * d))

proof end;

Lm9: for b being real number
for d being Integer st d <> 5 holds
2 * ((b + (((- d) + (abs d)) + 4)) + 1) <> 2 * (b + d)

proof end;

Lm10: for c, d being real number st - ((2 * c) + (1 + c)) < - 0 holds
(2 * (((abs d) + c) + c)) + 2 <> - ((2 * ((abs d) + c)) + (2 * d))

proof end;

Lm11: for a being Int_position
for k1 being Integer holds JUMP (a,k1 <>0_goto 5) = {}

proof end;

Lm12: for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 <>0_goto k2) = {}

proof end;

Lm13: for a being Int_position
for k1 being Integer holds JUMP (a,k1 <=0_goto 5) = {}

proof end;

Lm14: for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 <=0_goto k2) = {}

proof end;

Lm15: for a being Int_position
for k1 being Integer holds JUMP (a,k1 >=0_goto 5) = {}

proof end;

Lm16: for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 >=0_goto k2) = {}

proof end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster JUMP (a,k1 <>0_goto k2) -> empty ;
coherence

proof end;

cluster JUMP (a,k1 <=0_goto k2) -> empty ;
coherence

proof end;

cluster JUMP (a,k1 >=0_goto k2) -> empty ;
coherence

proof end;

end;

theorem Th29: :: SCMPDS_9:29

for l being Instruction-Location of SCMPDS holds SUCC l = the Instruction-Locations of SCMPDS

proof end;

theorem Th30: :: SCMPDS_9:30

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for l1, l2 being Instruction-Location of S st SUCC l1 = the Instruction-Locations of S holds
l1 <= l2

proof end;

registration

cluster SCMPDS -> non InsLoc-antisymmetric with-non-trivial-Instruction-Locations ;
coherence

proof end;

end;

registration

cluster SCMPDS -> non InsLoc-antisymmetric non standard with-non-trivial-Instruction-Locations ;
coherence by AMISTD_1:30;

end;