:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received October 8, 1993

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

begin

definition

AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2 ;

end;

func SCM -> strict AMI-Struct over 2 equals :: AMI_3:def 1

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

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

AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2 ;

:: deftheorem defines SCM AMI_3:def 1 :

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

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

Lm1: the_Values_of SCM = the ValuesF of SCM * the Object-Kind of SCM

.= SCM-VAL * SCM-OK ;

registration
end;

registration
end;

registration
end;

definition

canceled;

let a, b be Data-Location;

correctness

coherence

[1,{},<*a,b*>] is Instruction of SCM;

coherence

[2,{},<*a,b*>] is Instruction of SCM;

coherence

[3,{},<*a,b*>] is Instruction of SCM;

coherence

[4,{},<*a,b*>] is Instruction of SCM;

coherence

[5,{},<*a,b*>] is Instruction of SCM;

end;
let a, b be Data-Location;

correctness

coherence

[1,{},<*a,b*>] is Instruction of SCM;

proof end;

correctness coherence

[2,{},<*a,b*>] is Instruction of SCM;

proof end;

correctness coherence

[3,{},<*a,b*>] is Instruction of SCM;

proof end;

correctness coherence

[4,{},<*a,b*>] is Instruction of SCM;

proof end;

correctness coherence

[5,{},<*a,b*>] is Instruction of SCM;

proof end;

:: deftheorem defines AddTo AMI_3:def 4 :

for a, b being Data-Location holds AddTo (a,b) = [2,{},<*a,b*>];

for a, b being Data-Location holds AddTo (a,b) = [2,{},<*a,b*>];

:: deftheorem defines SubFrom AMI_3:def 5 :

for a, b being Data-Location holds SubFrom (a,b) = [3,{},<*a,b*>];

for a, b being Data-Location holds SubFrom (a,b) = [3,{},<*a,b*>];

:: deftheorem defines MultBy AMI_3:def 6 :

for a, b being Data-Location holds MultBy (a,b) = [4,{},<*a,b*>];

for a, b being Data-Location holds MultBy (a,b) = [4,{},<*a,b*>];

:: deftheorem defines Divide AMI_3:def 7 :

for a, b being Data-Location holds Divide (a,b) = [5,{},<*a,b*>];

for a, b being Data-Location holds Divide (a,b) = [5,{},<*a,b*>];

definition

let loc be Nat;

correctness

coherence

[6,<*loc*>,{}] is Instruction of SCM;

correctness

coherence

[7,<*loc*>,<*a*>] is Instruction of SCM;

coherence

[8,<*loc*>,<*a*>] is Instruction of SCM;

end;
correctness

coherence

[6,<*loc*>,{}] is Instruction of SCM;

proof end;

let a be Data-Location;correctness

coherence

[7,<*loc*>,<*a*>] is Instruction of SCM;

proof end;

correctness coherence

[8,<*loc*>,<*a*>] is Instruction of SCM;

proof end;

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

for loc being Nat

for a being Data-Location holds a =0_goto loc = [7,<*loc*>,<*a*>];

for loc being Nat

for a being Data-Location holds a =0_goto loc = [7,<*loc*>,<*a*>];

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

for loc being Nat

for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];

for loc being Nat

for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];

begin

theorem Th2: :: AMI_3:2

for a, b being Data-Location

for s being State of SCM holds

( (Exec ((a := b),s)) . (IC ) = succ (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 ) )

for s being State of SCM holds

( (Exec ((a := b),s)) . (IC ) = succ (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 Th3: :: AMI_3:3

for a, b being Data-Location

for s being State of SCM holds

( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (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 ) )

for s being State of SCM holds

( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (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 Th4: :: AMI_3:4

for a, b being Data-Location

for s being State of SCM holds

( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (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 ) )

for s being State of SCM holds

( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (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 Th5: :: AMI_3:5

for a, b being Data-Location

for s being State of SCM holds

( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (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 ) )

for s being State of SCM holds

( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (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 Th6: :: AMI_3:6

for a, b being Data-Location

for s being State of SCM 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 Data-Location st c <> a & c <> b holds

(Exec ((Divide (a,b)),s)) . c = s . c ) )

for s being State of SCM 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 Data-Location st c <> a & c <> b holds

(Exec ((Divide (a,b)),s)) . c = s . c ) )

proof end;

theorem :: AMI_3:7

for c being Data-Location

for loc being Nat

for s being State of SCM holds

( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )

for loc being Nat

for s being State of SCM holds

( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )

proof end;

theorem Th8: :: AMI_3:8

for a, c being Data-Location

for loc being Nat

for s being State of SCM holds

( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )

for loc being Nat

for s being State of SCM holds

( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )

proof end;

theorem Th9: :: AMI_3:9

for a, c being Data-Location

for loc being Nat

for s being State of SCM holds

( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )

for loc being Nat

for s being State of SCM holds

( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )

proof end;

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

not I is halting

proof end;

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

I is halting

proof end;

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

proof end;

Lm5: for a, b being Data-Location holds not AddTo (a,b) is halting

proof end;

Lm6: for a, b being Data-Location holds not SubFrom (a,b) is halting

proof end;

Lm7: for a, b being Data-Location holds not MultBy (a,b) is halting

proof end;

Lm8: for a, b being Data-Location holds not Divide (a,b) is halting

proof end;

Lm9: for loc being Nat holds not SCM-goto loc is halting

proof end;

Lm10: for a being Data-Location

for loc being Nat holds not a =0_goto loc is halting

proof end;

Lm11: for a being Data-Location

for loc being Nat holds not a >0_goto loc is halting

proof end;

Lm12: 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )

proof end;

Lm13: for W being Instruction of SCM st W is halting holds

W = [0,{},{}]

proof end;

begin

definition

let la be Data-Location;

let a be Integer;

:: original: .-->

redefine func la .--> a -> PartState of SCM;

coherence

la .--> a is PartState of SCM

end;
let a be Integer;

:: original: .-->

redefine func la .--> a -> PartState of SCM;

coherence

la .--> a is PartState of SCM

proof end;

definition

let la, lb be Data-Location;

let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCM;

coherence

(la,lb) --> (a,b) is PartState of SCM

end;
let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCM;

coherence

(la,lb) --> (a,b) is PartState of SCM

proof end;

begin

theorem :: AMI_3:14

theorem :: AMI_3:22

theorem :: AMI_3:23

theorem :: AMI_3:24

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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ) by Lm12;

( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ) by Lm12;