:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki

::

:: Received February 7, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition

AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3 ;

end;

func SCM+FSA -> strict AMI-Struct over 3 equals :: SCMFSA_2:def 1

AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

coherence AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3 ;

:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :

SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

begin

definition

:: original: Int-Locations

redefine func Int-Locations -> Subset of SCM+FSA;

coherence

Int-Locations is Subset of SCM+FSA

coherence

SCM+FSA-Data*-Loc is Subset of SCM+FSA ;

end;
redefine func Int-Locations -> Subset of SCM+FSA;

coherence

Int-Locations is Subset of SCM+FSA

proof end;

canceled;coherence

SCM+FSA-Data*-Loc is Subset of SCM+FSA ;

definition

mode Int-Location is Int-like Object of SCM+FSA;

canceled;

existence

ex b_{1} being Object of SCM+FSA st b_{1} in SCM+FSA-Data*-Loc

end;
canceled;

existence

ex b

proof end;

:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def 5 :

for b_{1} being Object of SCM+FSA holds

( b_{1} is FinSeq-Location iff b_{1} in SCM+FSA-Data*-Loc );

for b

( b

definition

let k be Nat;

coherence

dl. k is Int-Location

- (k + 1) is FinSeq-Location

end;
coherence

dl. k is Int-Location

proof end;

coherence - (k + 1) is FinSeq-Location

proof end;

registration
end;

begin

definition

let a, b be Int-Location;

ex b_{1} being Instruction of SCM+FSA ex A, B being Data-Location st

( a = A & b = B & b_{1} = A := B )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A, B being Data-Location st

( a = A & b = B & b_{1} = A := B ) & ex A, B being Data-Location st

( a = A & b = B & b_{2} = A := B ) holds

b_{1} = b_{2};

;

ex b_{1} being Instruction of SCM+FSA ex A, B being Data-Location st

( a = A & b = B & b_{1} = AddTo (A,B) )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A, B being Data-Location st

( a = A & b = B & b_{1} = AddTo (A,B) ) & ex A, B being Data-Location st

( a = A & b = B & b_{2} = AddTo (A,B) ) holds

b_{1} = b_{2};

;

ex b_{1} being Instruction of SCM+FSA ex A, B being Data-Location st

( a = A & b = B & b_{1} = SubFrom (A,B) )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A, B being Data-Location st

( a = A & b = B & b_{1} = SubFrom (A,B) ) & ex A, B being Data-Location st

( a = A & b = B & b_{2} = SubFrom (A,B) ) holds

b_{1} = b_{2};

;

ex b_{1} being Instruction of SCM+FSA ex A, B being Data-Location st

( a = A & b = B & b_{1} = MultBy (A,B) )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A, B being Data-Location st

( a = A & b = B & b_{1} = MultBy (A,B) ) & ex A, B being Data-Location st

( a = A & b = B & b_{2} = MultBy (A,B) ) holds

b_{1} = b_{2};

;

ex b_{1} being Instruction of SCM+FSA ex A, B being Data-Location st

( a = A & b = B & b_{1} = Divide (A,B) )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A, B being Data-Location st

( a = A & b = B & b_{1} = Divide (A,B) ) & ex A, B being Data-Location st

( a = A & b = B & b_{2} = Divide (A,B) ) holds

b_{1} = b_{2};

;

end;
func a := b -> Instruction of SCM+FSA means :Def8: :: SCMFSA_2:def 8

ex A, B being Data-Location st

( a = A & b = B & it = A := B );

existence ex A, B being Data-Location st

( a = A & b = B & it = A := B );

ex b

( a = A & b = B & b

proof end;

correctness uniqueness

for b

( a = A & b = B & b

( a = A & b = B & b

b

;

func AddTo (a,b) -> Instruction of SCM+FSA means :Def9: :: SCMFSA_2:def 9

ex A, B being Data-Location st

( a = A & b = B & it = AddTo (A,B) );

existence ex A, B being Data-Location st

( a = A & b = B & it = AddTo (A,B) );

ex b

( a = A & b = B & b

proof end;

correctness uniqueness

for b

( a = A & b = B & b

( a = A & b = B & b

b

;

func SubFrom (a,b) -> Instruction of SCM+FSA means :Def10: :: SCMFSA_2:def 10

ex A, B being Data-Location st

( a = A & b = B & it = SubFrom (A,B) );

existence ex A, B being Data-Location st

( a = A & b = B & it = SubFrom (A,B) );

ex b

( a = A & b = B & b

proof end;

correctness uniqueness

for b

( a = A & b = B & b

( a = A & b = B & b

b

;

func MultBy (a,b) -> Instruction of SCM+FSA means :Def11: :: SCMFSA_2:def 11

ex A, B being Data-Location st

( a = A & b = B & it = MultBy (A,B) );

existence ex A, B being Data-Location st

( a = A & b = B & it = MultBy (A,B) );

ex b

( a = A & b = B & b

proof end;

correctness uniqueness

for b

( a = A & b = B & b

( a = A & b = B & b

b

;

func Divide (a,b) -> Instruction of SCM+FSA means :Def12: :: SCMFSA_2:def 12

ex A, B being Data-Location st

( a = A & b = B & it = Divide (A,B) );

existence ex A, B being Data-Location st

( a = A & b = B & it = Divide (A,B) );

ex b

( a = A & b = B & b

proof end;

correctness uniqueness

for b

( a = A & b = B & b

( a = A & b = B & b

b

;

:: deftheorem Def8 defines := SCMFSA_2:def 8 :

for a, b being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = a := b iff ex A, B being Data-Location st

( a = A & b = B & b_{3} = A := B ) );

for a, b being Int-Location

for b

( b

( a = A & b = B & b

:: deftheorem Def9 defines AddTo SCMFSA_2:def 9 :

for a, b being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = AddTo (a,b) iff ex A, B being Data-Location st

( a = A & b = B & b_{3} = AddTo (A,B) ) );

for a, b being Int-Location

for b

( b

( a = A & b = B & b

:: deftheorem Def10 defines SubFrom SCMFSA_2:def 10 :

for a, b being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = SubFrom (a,b) iff ex A, B being Data-Location st

( a = A & b = B & b_{3} = SubFrom (A,B) ) );

for a, b being Int-Location

for b

( b

( a = A & b = B & b

:: deftheorem Def11 defines MultBy SCMFSA_2:def 11 :

for a, b being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = MultBy (a,b) iff ex A, B being Data-Location st

( a = A & b = B & b_{3} = MultBy (A,B) ) );

for a, b being Int-Location

for b

( b

( a = A & b = B & b

:: deftheorem Def12 defines Divide SCMFSA_2:def 12 :

for a, b being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = Divide (a,b) iff ex A, B being Data-Location st

( a = A & b = B & b_{3} = Divide (A,B) ) );

for a, b being Int-Location

for b

( b

( a = A & b = B & b

definition

let la be Element of NAT ;

coherence

SCM-goto la is Instruction of SCM+FSA by Th17;

let a be Int-Location;

ex b_{1} being Instruction of SCM+FSA ex A being Data-Location st

( a = A & b_{1} = A =0_goto la )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A being Data-Location st

( a = A & b_{1} = A =0_goto la ) & ex A being Data-Location st

( a = A & b_{2} = A =0_goto la ) holds

b_{1} = b_{2};

;

ex b_{1} being Instruction of SCM+FSA ex A being Data-Location st

( a = A & b_{1} = A >0_goto la )

uniqueness

for b_{1}, b_{2} being Instruction of SCM+FSA st ex A being Data-Location st

( a = A & b_{1} = A >0_goto la ) & ex A being Data-Location st

( a = A & b_{2} = A >0_goto la ) holds

b_{1} = b_{2};

;

end;
coherence

SCM-goto la is Instruction of SCM+FSA by Th17;

let a be Int-Location;

func a =0_goto la -> Instruction of SCM+FSA means :Def14: :: SCMFSA_2:def 14

ex A being Data-Location st

( a = A & it = A =0_goto la );

existence ex A being Data-Location st

( a = A & it = A =0_goto la );

ex b

( a = A & b

proof end;

correctness uniqueness

for b

( a = A & b

( a = A & b

b

;

func a >0_goto la -> Instruction of SCM+FSA means :Def15: :: SCMFSA_2:def 15

ex A being Data-Location st

( a = A & it = A >0_goto la );

existence ex A being Data-Location st

( a = A & it = A >0_goto la );

ex b

( a = A & b

proof end;

correctness uniqueness

for b

( a = A & b

( a = A & b

b

;

:: deftheorem defines goto SCMFSA_2:def 13 :

for la being Element of NAT holds goto la = SCM-goto la;

for la being Element of NAT holds goto la = SCM-goto la;

:: deftheorem Def14 defines =0_goto SCMFSA_2:def 14 :

for la being Element of NAT

for a being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = a =0_goto la iff ex A being Data-Location st

( a = A & b_{3} = A =0_goto la ) );

for la being Element of NAT

for a being Int-Location

for b

( b

( a = A & b

:: deftheorem Def15 defines >0_goto SCMFSA_2:def 15 :

for la being Element of NAT

for a being Int-Location

for b_{3} being Instruction of SCM+FSA holds

( b_{3} = a >0_goto la iff ex A being Data-Location st

( a = A & b_{3} = A >0_goto la ) );

for la being Element of NAT

for a being Int-Location

for b

( b

( a = A & b

definition

let c, i be Int-Location;

let a be FinSeq-Location ;

coherence

[9,{},<*c,a,i*>] is Instruction of SCM+FSA

[10,{},<*c,a,i*>] is Instruction of SCM+FSA

end;
let a be FinSeq-Location ;

coherence

[9,{},<*c,a,i*>] is Instruction of SCM+FSA

proof end;

coherence [10,{},<*c,a,i*>] is Instruction of SCM+FSA

proof end;

:: deftheorem defines := SCMFSA_2:def 16 :

for c, i being Int-Location

for a being FinSeq-Location holds c := (a,i) = [9,{},<*c,a,i*>];

for c, i being Int-Location

for a being FinSeq-Location holds c := (a,i) = [9,{},<*c,a,i*>];

:: deftheorem defines := SCMFSA_2:def 17 :

for c, i being Int-Location

for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>];

for c, i being Int-Location

for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>];

definition

let i be Int-Location;

let a be FinSeq-Location ;

coherence

[11,{},<*i,a*>] is Instruction of SCM+FSA

[12,{},<*i,a*>] is Instruction of SCM+FSA

end;
let a be FinSeq-Location ;

coherence

[11,{},<*i,a*>] is Instruction of SCM+FSA

proof end;

coherence [12,{},<*i,a*>] is Instruction of SCM+FSA

proof end;

:: deftheorem defines :=len SCMFSA_2:def 18 :

for i being Int-Location

for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>];

for i being Int-Location

for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>];

:: deftheorem defines :=<0,...,0> SCMFSA_2:def 19 :

for i being Int-Location

for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>];

for i being Int-Location

for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>];

theorem :: SCMFSA_2:26

for fa being FinSeq-Location

for c, a being Int-Location holds InsCode (c := (fa,a)) = 9 by RECDEF_2:def 1;

for c, a being Int-Location holds InsCode (c := (fa,a)) = 9 by RECDEF_2:def 1;

theorem :: SCMFSA_2:27

for fa being FinSeq-Location

for a, c being Int-Location holds InsCode ((fa,a) := c) = 10 by RECDEF_2:def 1;

for a, c being Int-Location holds InsCode ((fa,a) := c) = 10 by RECDEF_2:def 1;

theorem :: SCMFSA_2:28

for fa being FinSeq-Location

for a being Int-Location holds InsCode (a :=len fa) = 11 by RECDEF_2:def 1;

for a being Int-Location holds InsCode (a :=len fa) = 11 by RECDEF_2:def 1;

theorem :: SCMFSA_2:29

for fa being FinSeq-Location

for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 by RECDEF_2:def 1;

for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 by RECDEF_2:def 1;

theorem Th30: :: SCMFSA_2:30

for ins being Instruction of SCM+FSA st InsCode ins = 1 holds

ex da, db being Int-Location st ins = da := db

ex da, db being Int-Location st ins = da := db

proof end;

theorem Th31: :: SCMFSA_2:31

for ins being Instruction of SCM+FSA st InsCode ins = 2 holds

ex da, db being Int-Location st ins = AddTo (da,db)

ex da, db being Int-Location st ins = AddTo (da,db)

proof end;

theorem Th32: :: SCMFSA_2:32

for ins being Instruction of SCM+FSA st InsCode ins = 3 holds

ex da, db being Int-Location st ins = SubFrom (da,db)

ex da, db being Int-Location st ins = SubFrom (da,db)

proof end;

theorem Th33: :: SCMFSA_2:33

for ins being Instruction of SCM+FSA st InsCode ins = 4 holds

ex da, db being Int-Location st ins = MultBy (da,db)

ex da, db being Int-Location st ins = MultBy (da,db)

proof end;

theorem Th34: :: SCMFSA_2:34

for ins being Instruction of SCM+FSA st InsCode ins = 5 holds

ex da, db being Int-Location st ins = Divide (da,db)

ex da, db being Int-Location st ins = Divide (da,db)

proof end;

theorem Th35: :: SCMFSA_2:35

for ins being Instruction of SCM+FSA st InsCode ins = 6 holds

ex lb being Element of NAT st ins = goto lb

ex lb being Element of NAT st ins = goto lb

proof end;

theorem Th36: :: SCMFSA_2:36

for ins being Instruction of SCM+FSA st InsCode ins = 7 holds

ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb

ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb

proof end;

theorem Th37: :: SCMFSA_2:37

for ins being Instruction of SCM+FSA st InsCode ins = 8 holds

ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb

ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb

proof end;

theorem Th38: :: SCMFSA_2:38

for ins being Instruction of SCM+FSA st InsCode ins = 9 holds

ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)

ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)

proof end;

theorem Th39: :: SCMFSA_2:39

for ins being Instruction of SCM+FSA st InsCode ins = 10 holds

ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b

ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b

proof end;

theorem Th40: :: SCMFSA_2:40

for ins being Instruction of SCM+FSA st InsCode ins = 11 holds

ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa

ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa

proof end;

theorem Th41: :: SCMFSA_2:41

for ins being Instruction of SCM+FSA st InsCode ins = 12 holds

ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a

ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a

proof end;

begin

theorem Th51: :: SCMFSA_2:51

for i being Instruction of SCM

for ii being Instruction of SCM+FSA

for s being State of SCM

for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds

Exec (ii,ss) = ss +* (Exec (i,s))

for ii being Instruction of SCM+FSA

for s being State of SCM

for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds

Exec (ii,ss) = ss +* (Exec (i,s))

proof end;

registration
end;

definition

let s be State of SCM+FSA;

let d be FinSeq-Location ;

:: original: .

redefine func s . d -> FinSequence of INT ;

coherence

s . d is FinSequence of INT

end;
let d be FinSeq-Location ;

:: original: .

redefine func s . d -> FinSequence of INT ;

coherence

s . d is FinSequence of INT

proof end;

theorem Th52: :: SCMFSA_2:52

for S being State of SCM

for s being State of SCM+FSA st S = s | SCM-Memory holds

s = s +* S by FUNCT_4:75;

for s being State of SCM+FSA st S = s | SCM-Memory holds

s = s +* S by FUNCT_4:75;

theorem Th53: :: SCMFSA_2:53

for S being State of SCM

for s1, s being State of SCM+FSA st s1 = s +* S holds

s1 . (IC ) = S . (IC )

for s1, s being State of SCM+FSA st s1 = s +* S holds

s1 . (IC ) = S . (IC )

proof end;

theorem Th54: :: SCMFSA_2:54

for A being Data-Location

for a being Int-Location

for S being State of SCM

for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds

S . A = s1 . a

for a being Int-Location

for S being State of SCM

for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds

S . A = s1 . a

proof end;

theorem Th55: :: SCMFSA_2:55

for A being Data-Location

for a being Int-Location

for S being State of SCM

for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds

S . A = s . a

for a being Int-Location

for S being State of SCM

for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds

S . A = s . a

proof end;

registration
end;

theorem :: SCMFSA_2:61

for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

s1 = s2

s1 = s2

proof end;

begin

theorem Th63: :: SCMFSA_2:63

for a, b being Int-Location

for s being State of SCM+FSA holds

( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds

(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds

(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )

proof end;

theorem Th64: :: SCMFSA_2:64

for a, b being Int-Location

for s being State of SCM+FSA holds

( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )

proof end;

theorem Th65: :: SCMFSA_2:65

for a, b being Int-Location

for s being State of SCM+FSA holds

( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )

proof end;

theorem Th66: :: SCMFSA_2:66

for a, b being Int-Location

for s being State of SCM+FSA holds

( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds

(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )

proof end;

theorem Th67: :: SCMFSA_2:67

for a, b being Int-Location

for s being State of SCM+FSA holds

( (Exec ((Divide (a,b)),s)) . (IC ) = succ (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 Int-Location st c <> a & c <> b holds

(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((Divide (a,b)),s)) . (IC ) = succ (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 Int-Location st c <> a & c <> b holds

(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )

proof end;

theorem :: SCMFSA_2:68

for a being Int-Location

for s being State of SCM+FSA holds

( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds

(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds

(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )

proof end;

theorem Th69: :: SCMFSA_2:69

for l being Element of NAT

for s being State of SCM+FSA holds

( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )

for s being State of SCM+FSA holds

( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )

proof end;

theorem Th70: :: SCMFSA_2:70

for l being Element of NAT

for a being Int-Location

for s being State of SCM+FSA holds

( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )

for a being Int-Location

for s being State of SCM+FSA holds

( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )

proof end;

theorem Th71: :: SCMFSA_2:71

for l being Element of NAT

for a being Int-Location

for s being State of SCM+FSA holds

( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )

for a being Int-Location

for s being State of SCM+FSA holds

( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )

proof end;

theorem Th72: :: SCMFSA_2:72

for g being FinSeq-Location

for c, a being Int-Location

for s being State of SCM+FSA holds

( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds

(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )

for c, a being Int-Location

for s being State of SCM+FSA holds

( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds

(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )

proof end;

theorem Th73: :: SCMFSA_2:73

for g being FinSeq-Location

for a, c being Int-Location

for s being State of SCM+FSA holds

( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds

(Exec (((g,a) := c),s)) . f = s . f ) )

for a, c being Int-Location

for s being State of SCM+FSA holds

( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds

(Exec (((g,a) := c),s)) . f = s . f ) )

proof end;

theorem Th74: :: SCMFSA_2:74

for g being FinSeq-Location

for c being Int-Location

for s being State of SCM+FSA holds

( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds

(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )

for c being Int-Location

for s being State of SCM+FSA holds

( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds

(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )

proof end;

theorem Th75: :: SCMFSA_2:75

for g being FinSeq-Location

for c being Int-Location

for s being State of SCM+FSA holds

( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds

(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )

for c being Int-Location

for s being State of SCM+FSA holds

( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st

( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds

(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )

proof end;

begin

theorem :: SCMFSA_2:76

for s being State of SCM+FSA

for S being SCM+FSA-State st S = s holds

IC s = IC S by FUNCT_7:def 1, SCMFSA_1:5;

for S being SCM+FSA-State st S = s holds

IC s = IC S by FUNCT_7:def 1, SCMFSA_1:5;

theorem Th77: :: SCMFSA_2:77

for i being Instruction of SCM

for I being Instruction of SCM+FSA st i = I & i is halting holds

I is halting

for I being Instruction of SCM+FSA st i = I & i is halting holds

I is halting

proof end;

theorem Th78: :: SCMFSA_2:78

for I being Instruction of SCM+FSA st ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = succ (IC s) holds

not I is halting

not I is halting

proof end;

registration

let a, b be Int-Location;

set s = the State of SCM+FSA;

coherence

not a := b is halting

not AddTo (a,b) is halting

not SubFrom (a,b) is halting

not MultBy (a,b) is halting

not Divide (a,b) is halting

end;
set s = the State of SCM+FSA;

coherence

not a := b is halting

proof end;

coherence not AddTo (a,b) is halting

proof end;

coherence not SubFrom (a,b) is halting

proof end;

coherence not MultBy (a,b) is halting

proof end;

coherence not Divide (a,b) is halting

proof end;

registration

let a be Int-Location;

let la be Element of NAT ;

set f = the_Values_of SCM+FSA;

set s = the SCM+FSA-State;

coherence

not a =0_goto la is halting

not a >0_goto la is halting

end;
let la be Element of NAT ;

set f = the_Values_of SCM+FSA;

set s = the SCM+FSA-State;

coherence

not a =0_goto la is halting

proof end;

coherence not a >0_goto la is halting

proof end;

theorem :: SCMFSA_2:85

theorem :: SCMFSA_2:86

registration

let c be Int-Location;

let f be FinSeq-Location ;

let a be Int-Location;

set s = the State of SCM+FSA;

coherence

not c := (f,a) is halting

not (f,a) := c is halting

end;
let f be FinSeq-Location ;

let a be Int-Location;

set s = the State of SCM+FSA;

coherence

not c := (f,a) is halting

proof end;

coherence not (f,a) := c is halting

proof end;

theorem :: SCMFSA_2:87

theorem :: SCMFSA_2:88

registration

let c be Int-Location;

let f be FinSeq-Location ;

set s = the State of SCM+FSA;

coherence

not c :=len f is halting

not f :=<0,...,0> c is halting

end;
let f be FinSeq-Location ;

set s = the State of SCM+FSA;

coherence

not c :=len f is halting

proof end;

coherence not f :=<0,...,0> c is halting

proof end;

theorem :: SCMFSA_2:89

theorem :: SCMFSA_2:90

theorem :: SCMFSA_2:91

theorem Th93: :: SCMFSA_2:93

for I being set holds

( I is Instruction of SCM+FSA iff ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) )

( I is Instruction of SCM+FSA iff ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) )

proof end;

Lm1: for W being Instruction of SCM+FSA st W is halting holds

W = [0,{},{}]

proof end;

theorem :: SCMFSA_2:95

theorem :: SCMFSA_2:98

for i being Instruction of SCM

for I being Instruction of SCM+FSA st i = I & not i is halting holds

not I is halting by Th94, Th96;

for I being Instruction of SCM+FSA st i = I & not i is halting holds

not I is halting by Th94, Th96;

theorem :: SCMFSA_2:104

for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

s1 = s2

s1 = s2

proof end;

registration

let f be FinSeq-Location ;

let w be FinSequence of INT ;

coherence

for b_{1} being PartState of SCM+FSA st b_{1} = f .--> w holds

b_{1} is data-only

end;
let w be FinSequence of INT ;

coherence

for b

b

proof end;

registration

let x be Int-Location;

let i be Integer;

coherence

for b_{1} being PartState of SCM+FSA st b_{1} = x .--> i holds

b_{1} is data-only

end;
let i be Integer;

coherence

for b

b

proof end;

registration
end;

registration
end;

registration

let fa be FinSeq-Location ;

let a, c be Int-Location;

coherence

c := (fa,a) is No-StopCode

end;
let a, c be Int-Location;

coherence

c := (fa,a) is No-StopCode

proof end;

registration

let fa be FinSeq-Location ;

let a, c be Int-Location;

coherence

(fa,a) := c is No-StopCode

end;
let a, c be Int-Location;

coherence

(fa,a) := c is No-StopCode

proof end;

registration
end;

registration

let fa be FinSeq-Location ;

let a be Int-Location;

coherence

fa :=<0,...,0> a is No-StopCode

end;
let a be Int-Location;

coherence

fa :=<0,...,0> a is No-StopCode

proof end;