:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received October 8, 1993

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

registration

let i1 be Integer;

coherence

<%i1%> is INT -valued ;

let i2 be Integer;

coherence

<%i1,i2%> is INT -valued ;

let i3 be Integer;

coherence

<%i1,i2,i3%> is INT -valued ;

let i4 be Integer;

coherence

<%i1,i2,i3,i4%> is INT -valued ;

end;
coherence

<%i1%> is INT -valued ;

let i2 be Integer;

coherence

<%i1,i2%> is INT -valued ;

let i3 be Integer;

coherence

<%i1,i2,i3%> is INT -valued ;

let i4 be Integer;

coherence

<%i1,i2,i3,i4%> is INT -valued ;

definition

let D be XFinSequence of INT ;

ex b_{1} being State of SCM st

for k being Element of NAT st k < len D holds

b_{1} . (dl. k) = D . k

end;
mode State-consisting of D -> State of SCM means :Def1: :: SCM_1:def 1

for k being Element of NAT st k < len D holds

it . (dl. k) = D . k;

existence for k being Element of NAT st k < len D holds

it . (dl. k) = D . k;

ex b

for k being Element of NAT st k < len D holds

b

proof end;

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

for D being XFinSequence of INT

for b_{2} being State of SCM holds

( b_{2} is State-consisting of D iff for k being Element of NAT st k < len D holds

b_{2} . (dl. k) = D . k );

for D being XFinSequence of INT

for b

( b

b

registration

let D be XFinSequence of INT ;

let il be Element of NAT ;

ex b_{1} being State-consisting of D st b_{1} is il -started

end;
let il be Element of NAT ;

cluster V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total il -started for State-consisting of D;

existence ex b

proof end;

theorem :: SCM_1:1

for i1, i2, i3, i4 being Integer

for il being Element of NAT

for s being b_{5} -started State-consisting of <%i1,i2,i3,i4%> holds

( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )

for il being Element of NAT

for s being b

( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )

proof end;

theorem Th2: :: SCM_1:2

for i1, i2 being Integer

for il being Element of NAT

for s being b_{3} -started State-consisting of <%i1,i2%> holds

( s . (dl. 0) = i1 & s . (dl. 1) = i2 )

for il being Element of NAT

for s being b

( s . (dl. 0) = i1 & s . (dl. 1) = i2 )

proof end;

theorem Th3: :: SCM_1:3

for I1, I2 being Instruction of SCM

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds

( F . 0 = I1 & F . 1 = I2 )

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds

( F . 0 = I1 & F . 1 = I2 )

proof end;

Lm1: for F being NAT -defined the InstructionsF of SCM -valued total Function

for k being Nat

for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))

proof end;

Lm2: now :: thesis: for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let k, n be Element of NAT ; :: thesis: for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let s be State of SCM; :: thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let a, b be Data-Location; :: thesis: ( IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )

assume A1: IC (Comput (F,s,k)) = n ; :: thesis: ( ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )

set csk1 = Comput (F,s,(k + 1));

set csk = Comput (F,s,k);

assume A2: ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) ; :: thesis: ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

A3: dom F = NAT by PARTFUN1:def 2;

thus Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1

.= Exec ((F . n),(Comput (F,s,k))) by A1, A3, PARTFUN1:def 6 ; :: thesis: IC (Comput (F,s,(k + 1))) = n + 1

hence IC (Comput (F,s,(k + 1))) = (IC (Comput (F,s,k))) + 1 by A2, AMI_3:2, AMI_3:3, AMI_3:4, AMI_3:5, AMI_3:6

.= n + 1 by A1 ;

:: thesis: verum

end;
for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let k, n be Element of NAT ; :: thesis: for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let s be State of SCM; :: thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds

( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

let a, b be Data-Location; :: thesis: ( IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )

assume A1: IC (Comput (F,s,k)) = n ; :: thesis: ( ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )

set csk1 = Comput (F,s,(k + 1));

set csk = Comput (F,s,k);

assume A2: ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) ; :: thesis: ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )

A3: dom F = NAT by PARTFUN1:def 2;

thus Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1

.= Exec ((F . n),(Comput (F,s,k))) by A1, A3, PARTFUN1:def 6 ; :: thesis: IC (Comput (F,s,(k + 1))) = n + 1

hence IC (Comput (F,s,(k + 1))) = (IC (Comput (F,s,k))) + 1 by A2, AMI_3:2, AMI_3:3, AMI_3:4, AMI_3:5, AMI_3:6

.= n + 1 by A1 ;

:: thesis: verum

theorem Th4: :: SCM_1:4

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = a := b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = (Comput (F,s,k)) . b & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = a := b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = (Comput (F,s,k)) . b & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th5: :: SCM_1:5

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = AddTo (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) + ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = AddTo (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) + ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th6: :: SCM_1:6

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th7: :: SCM_1:7

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) * ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) * ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th8: :: SCM_1:8

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds

( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds

(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th9: :: SCM_1:9

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds

( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds

( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th10: :: SCM_1:10

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Nat

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a =0_goto il holds

( ( (Comput (F,s,k)) . a = 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <> 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Nat

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a =0_goto il holds

( ( (Comput (F,s,k)) . a = 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <> 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th11: :: SCM_1:11

for F being NAT -defined the InstructionsF of SCM -valued total Function

for k, n being Element of NAT

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

for k, n being Element of NAT

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

proof end;

theorem Th12: :: SCM_1:12

( (halt SCM) `1_3 = 0 & ( for a, b being Data-Location holds (a := b) `1_3 = 1 ) & ( for a, b being Data-Location holds (AddTo (a,b)) `1_3 = 2 ) & ( for a, b being Data-Location holds (SubFrom (a,b)) `1_3 = 3 ) & ( for a, b being Data-Location holds (MultBy (a,b)) `1_3 = 4 ) & ( for a, b being Data-Location holds (Divide (a,b)) `1_3 = 5 ) & ( for i being Element of NAT holds (SCM-goto i) `1_3 = 6 ) & ( for a being Data-Location

for i being Element of NAT holds (a =0_goto i) `1_3 = 7 ) & ( for a being Data-Location

for i being Element of NAT holds (a >0_goto i) `1_3 = 8 ) ) by AMI_3:26;

for i being Element of NAT holds (a =0_goto i) `1_3 = 7 ) & ( for a being Data-Location

for i being Element of NAT holds (a >0_goto i) `1_3 = 8 ) ) by AMI_3:26;

theorem :: SCM_1:13

for i1, i2, i3, i4 being Integer

for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds

s is State-consisting of <%i1,i2,i3,i4%>

for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds

s is State-consisting of <%i1,i2,i3,i4%>

proof end;

:: Empty program

theorem :: SCM_1:14

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(halt SCM)%> c= F holds

for s being 0 -started State-consisting of <*> INT holds

( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )

for s being 0 -started State-consisting of <*> INT holds

( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )

proof end;

:: Assignment

theorem :: SCM_1:15

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

proof end;

:: Adding two integers

theorem :: SCM_1:16

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

proof end;

:: Subtracting two integers

theorem :: SCM_1:17

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

proof end;

:: Multiplying two integers

theorem :: SCM_1:18

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds

(Result (F,s)) . d = s . d ) )

proof end;

:: Dividing two integers

theorem :: SCM_1:19

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds

(Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds

(Result (F,s)) . d = s . d ) )

proof end;

:: Unconditional jump

theorem :: SCM_1:20

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(SCM-goto 1)%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

proof end;

:: Jump at zero

theorem :: SCM_1:21

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

proof end;

:: Jump at greater than zero

theorem :: SCM_1:22

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> c= F holds

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

for i1, i2 being Integer

for s being 0 -started State-consisting of <%i1,i2%> holds

( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )

proof end;