:: SCM_1 semantic presentation

definition

let i be Integer;
:: original: <*
redefine func <*i*> -> FinSequence of INT ;
coherence

proof end;

end;

theorem Th1: :: SCM_1:1

for s being State of SCM holds
( IC s = s . 0 & CurInstr s = s . (s . 0) ) by AMI_3:4;

theorem Th2: :: SCM_1:2

for s being State of SCM
for k being Nat holds
( CurInstr ((Computation s) . k) = s . (IC ((Computation s) . k)) & CurInstr ((Computation s) . k) = s . (((Computation s) . k) . 0) ) by AMI_3:4, AMI_1:54;

theorem Th3: :: SCM_1:3

for s being State of SCM st ex k being Nat st s . (IC ((Computation s) . k)) = halt SCM holds
s is halting

proof end;

theorem Th4: :: SCM_1:4

for s being State of SCM
for k being Nat st s . (IC ((Computation s) . k)) = halt SCM holds
Result s = (Computation s) . k

proof end;

theorem :: SCM_1:5

canceled;

theorem :: SCM_1:6

canceled;

theorem Th7: :: SCM_1:7

for n, m being Nat holds
( IC SCM <> il. n & IC SCM <> dl. n & il. n <> dl. m ) by AMI_3:56, AMI_3:57;

Lm1: now

let p be FinSequence; :: thesis:
let n be Nat; :: thesis:
assume n < len p ; :: thesis:
then ( n + 1 >= 0 + 1 & n + 1 <= len p ) by NAT_1:38;
then ( n + 1 in dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, FINSEQ_3:27;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def 5; :: thesis:

end;

Lm2: now

let n be Nat; :: thesis:
let x be set ; :: thesis:
let p be FinSequence of x; :: thesis:
assume n < len p ; :: thesis:
then ( p . (n + 1) in rng p & rng p c= x ) by Lm1, FINSEQ_1:def 4;
hence p . (n + 1) in x ; :: thesis:

end;

definition

let I be FinSequence of the Instructions of SCM ;
let D be FinSequence of INT ;
let il, ps, ds be Nat;
mode State-consisting of il,ps,ds,I,D -> State of SCM means :Def1: :: SCM_1:def 1
( IC it = il. il & ( for k being Nat st k < len I holds
it . (il. (ps + k)) = I . (k + 1) ) & ( for k being Nat st k < len D holds
it . (dl. (ds + k)) = D . (k + 1) ) );
existence

proof end;

end;

:: deftheorem Def1 defines State-consisting SCM_1:def 1 :

Lm3: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 )
by FINSEQ_1:3;

Lm4: ( 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4 )
by FINSEQ_1:3;

Lm5: ( 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5 )
by FINSEQ_1:3;

Lm6: ( 1 in Seg 6 & 2 in Seg 6 & 3 in Seg 6 & 4 in Seg 6 & 5 in Seg 6 & 6 in Seg 6 )
by FINSEQ_1:3;

Lm7: ( 1 in Seg 7 & 2 in Seg 7 & 3 in Seg 7 & 4 in Seg 7 & 5 in Seg 7 & 6 in Seg 7 & 7 in Seg 7 )
by FINSEQ_1:3;

Lm8: ( 1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 & 5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 )
by FINSEQ_1:3;

theorem Th8: :: SCM_1:8

for x1, x2, x3, x4 being set
for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )

proof end;

theorem Th9: :: SCM_1:9

for x1, x2, x3, x4, x5 being set
for p being FinSequence st p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> holds
( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )

proof end;

theorem Th10: :: SCM_1:10

for x1, x2, x3, x4, x5, x6 being set
for p being FinSequence st p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> holds
( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )

proof end;

theorem Th11: :: SCM_1:11

for x1, x2, x3, x4, x5, x6, x7 being set
for p being FinSequence st p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> holds
( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )

proof end;

theorem Th12: :: SCM_1:12

for x1, x2, x3, x4, x5, x6, x7, x8 being set
for p being FinSequence st p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> holds
( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )

proof end;

theorem Th13: :: SCM_1:13

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set
for p being FinSequence st p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> holds
( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )

proof end;

theorem :: SCM_1:14

for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM
for i1, i2, i3, i4 being Integer
for il being Nat
for s being State-consisting of il,0,0,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( IC s = il. il & s . (il. 0) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )

proof end;

theorem Th15: :: SCM_1:15

for I1, I2 being Instruction of SCM
for i1, i2 being Integer
for il being Nat
for s being State-consisting of il,0,0,<*I1*> ^ <*I2*>,<*i1*> ^ <*i2*> holds
( IC s = il. il & s . (il. 0) = I1 & s . (il. 1) = I2 & s . (dl. 0) = i1 & s . (dl. 1) = i2 )

proof end;

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 s be State of S;
assume A1: s is halting ;
func Complexity s -> Nat means :Def2: :: SCM_1:def 2
( CurInstr ((Computation s) . it) = halt S & ( for k being Nat st CurInstr ((Computation s) . k) = halt S holds
it <= k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Complexity SCM_1:def 2 :

notation

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 s be State of S;
synonym LifeSpan s for Complexity s;

end;

theorem Th16: :: SCM_1:16

for s being State of SCM
for k being Nat holds
( s . (IC ((Computation s) . k)) <> halt SCM & s . (IC ((Computation s) . (k + 1))) = halt SCM iff ( Complexity s = k + 1 & s is halting ) )

proof end;

theorem Th17: :: SCM_1:17

for s being State of SCM
for k being Nat st IC ((Computation s) . k) <> IC ((Computation s) . (k + 1)) & s . (IC ((Computation s) . (k + 1))) = halt SCM holds
Complexity s = k + 1

proof end;

Lm9: for n being Nat holds Next (il. n) = il. (n + 1)

proof end;

Lm10: for k being Nat
for s being State of SCM holds (Computation s) . (k + 1) = Exec (CurInstr ((Computation s) . k)),((Computation s) . k)

proof end;

Lm11: now

let k, n be Nat; :: thesis:
let s be State of SCM ; :: thesis:
let a, b be Data-Location ; :: thesis:
assume A1: IC ((Computation s) . k) = il. n ; :: thesis:
A2: ((Computation s) . k) . (il. n) = s . (il. n) by AMI_1:54;
set csk = (Computation s) . k;
set csk1 = (Computation s) . (k + 1);
A3: ((Computation s) . k) . 0 = il. n by A1, Th1;
assume A4: ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) ; :: thesis:
thus A5: (Computation s) . (k + 1) = Exec (CurInstr ((Computation s) . k)),((Computation s) . k) by Lm10
.= Exec (s . (il. n)),((Computation s) . k) by A2, A3, Th1 ; :: thesis:
thus IC ((Computation s) . (k + 1)) = ((Computation s) . (k + 1)) . 0 by Th1
.= Next (IC ((Computation s) . k)) by A4, A5, AMI_3:4, AMI_3:8, AMI_3:9, AMI_3:10, AMI_3:11, AMI_3:12
.= il. (n + 1) by A1, Lm9 ; :: thesis:

end;

theorem Th18: :: SCM_1:18

for k, n being Nat
for s being State of SCM
for a, b being Data-Location st IC ((Computation s) . k) = il. n & s . (il. n) = a := b holds
( IC ((Computation s) . (k + 1)) = il. (n + 1) & ((Computation s) . (k + 1)) . a = ((Computation s) . k) . b & ( for d being Data-Location st d <> a holds
((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th19: :: SCM_1:19

for k, n being Nat
for s being State of SCM
for a, b being Data-Location st IC ((Computation s) . k) = il. n & s . (il. n) = AddTo a,b holds
( IC ((Computation s) . (k + 1)) = il. (n + 1) & ((Computation s) . (k + 1)) . a = (((Computation s) . k) . a) + (((Computation s) . k) . b) & ( for d being Data-Location st d <> a holds
((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th20: :: SCM_1:20

for k, n being Nat
for s being State of SCM
for a, b being Data-Location st IC ((Computation s) . k) = il. n & s . (il. n) = SubFrom a,b holds
( IC ((Computation s) . (k + 1)) = il. (n + 1) & ((Computation s) . (k + 1)) . a = (((Computation s) . k) . a) - (((Computation s) . k) . b) & ( for d being Data-Location st d <> a holds
((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th21: :: SCM_1:21

for k, n being Nat
for s being State of SCM
for a, b being Data-Location st IC ((Computation s) . k) = il. n & s . (il. n) = MultBy a,b holds
( IC ((Computation s) . (k + 1)) = il. (n + 1) & ((Computation s) . (k + 1)) . a = (((Computation s) . k) . a) * (((Computation s) . k) . b) & ( for d being Data-Location st d <> a holds
((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th22: :: SCM_1:22

for k, n being Nat
for s being State of SCM
for a, b being Data-Location st IC ((Computation s) . k) = il. n & s . (il. n) = Divide a,b & a <> b holds
( IC ((Computation s) . (k + 1)) = il. (n + 1) & ((Computation s) . (k + 1)) . a = (((Computation s) . k) . a) div (((Computation s) . k) . b) & ((Computation s) . (k + 1)) . b = (((Computation s) . k) . a) mod (((Computation s) . k) . b) & ( for d being Data-Location st d <> a & d <> b holds
((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th23: :: SCM_1:23

for k, n being Nat
for s being State of SCM
for il being Instruction-Location of SCM st IC ((Computation s) . k) = il. n & s . (il. n) = goto il holds
( IC ((Computation s) . (k + 1)) = il & ( for d being Data-Location holds ((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th24: :: SCM_1:24

for k, n being Nat
for s being State of SCM
for a being Data-Location
for il being Instruction-Location of SCM st IC ((Computation s) . k) = il. n & s . (il. n) = a =0_goto il holds
( ( ((Computation s) . k) . a = 0 implies IC ((Computation s) . (k + 1)) = il ) & ( ((Computation s) . k) . a <> 0 implies IC ((Computation s) . (k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds ((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th25: :: SCM_1:25

for k, n being Nat
for s being State of SCM
for a being Data-Location
for il being Instruction-Location of SCM st IC ((Computation s) . k) = il. n & s . (il. n) = a >0_goto il holds
( ( ((Computation s) . k) . a > 0 implies IC ((Computation s) . (k + 1)) = il ) & ( ((Computation s) . k) . a <= 0 implies IC ((Computation s) . (k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds ((Computation s) . (k + 1)) . d = ((Computation s) . k) . d ) )

proof end;

theorem Th26: :: SCM_1:26

( (halt SCM ) `1 = 0 & ( for a, b being Data-Location holds (a := b) `1 = 1 ) & ( for a, b being Data-Location holds (AddTo a,b) `1 = 2 ) & ( for a, b being Data-Location holds (SubFrom a,b) `1 = 3 ) & ( for a, b being Data-Location holds (MultBy a,b) `1 = 4 ) & ( for a, b being Data-Location holds (Divide a,b) `1 = 5 ) & ( for i being Instruction-Location of SCM holds (goto i) `1 = 6 ) & ( for a being Data-Location
for i being Instruction-Location of SCM holds (a =0_goto i) `1 = 7 ) & ( for a being Data-Location
for i being Instruction-Location of SCM holds (a >0_goto i) `1 = 8 ) )

proof end;

theorem Th27: :: SCM_1:27

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

proof end;

theorem :: SCM_1:28

for s1, s2 being State of SCM
for k, c being Nat st s2 = (Computation s1) . k & Complexity s2 = c & s2 is halting & 0 < c holds
Complexity s1 = k + c

proof end;

theorem :: SCM_1:29

for s1, s2 being State of SCM
for k being Nat st s2 = (Computation s1) . k & s2 is halting holds
Result s2 = Result s1

proof end;

theorem :: SCM_1:30

for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM
for i1, i2, i3, i4 being Integer
for il being Nat
for s being State of SCM st IC s = il. il & s . (il. 0) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of il,0,0,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>

proof end;

theorem :: SCM_1:31

for s being State-consisting of 0,0,0,<*(halt SCM )*>, <*> INT holds
( s is halting & Complexity s = 0 & Result s = s )

proof end;

theorem :: SCM_1:32

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*((dl. 0) := (dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & (Result s) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:33

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*(AddTo (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & (Result s) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:34

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*(SubFrom (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & (Result s) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:35

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*(MultBy (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & (Result s) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:36

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*(Divide (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & (Result s) . (dl. 0) = i1 div i2 & (Result s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:37

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*(goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:38

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*((dl. 0) =0_goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:39

for i1, i2 being Integer
for s being State-consisting of 0,0,0,<*((dl. 0) >0_goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & Complexity s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;