:: SCM_1 semantic presentation

begin

definition
let i be Integer;
:: original: <*
redefine func<*i*> ->  FinSequence of INT ;
coherence
 <*i*> is FinSequence of INT
proof
reconsider i1 = i as Element of INT by INT_1:def_2;
 <*i1*> is FinSequence of INT ;
hence  <*i*> is FinSequence of INT ; ::_thesis: verum
end;
end;

registration
let i1 be Integer;
cluster<%i1%> ->  INT -valued ;
coherence
 <%i1%> is INT -valued ;
let i2 be Integer;
cluster<%i1,i2%> ->  INT -valued ;
coherence
 <%i1,i2%> is INT -valued ;
let i3 be Integer;
cluster<%i1,i2,i3%> ->  INT -valued ;
coherence
 <%i1,i2,i3%> is INT -valued ;
let i4 be Integer;
cluster<%i1,i2,i3,i4%> ->  INT -valued ;
coherence
 <%i1,i2,i3,i4%> is INT -valued ;
end;

definition
let D be XFinSequence of INT ;
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
 ex b1 being State of SCM st
for k being Element of NAT st k < len D holds
b1 . (dl. k) = D . k
proof
defpred S1[ set , set ] means  ex k being Element of NAT st
( $1 = dl. k & $2 = D . k );
A1: for x, y being set st x in the carrier of SCM & S1[x,y] holds
y in INT by INT_1:def_2;
A2: for x, y1, y2 being set st x in the carrier of SCM & S1[x,y1] & S1[x,y2] holds
y1 = y2 by AMI_3:10;
consider p being PartFunc of SCM,INT such that
A9: for x being set holds
( x in dom p iff ( x in the carrier of SCM & ex y being set st S1[x,y] ) ) and
A10: for x being set st x in dom p holds
S1[x,p . x] from PARTFUN1:sch_2(A1, A2);
A11: p is the carrier of SCM -defined
proof
let e be set ; :: according to TARSKI:def_3,RELAT_1:def_18 ::_thesis: ( not e in proj1 p or e in the carrier of SCM )
thus  ( not e in proj1 p or e in the carrier of SCM ) by A9; ::_thesis: verum
end;
 p is the_Values_of SCM -compatible
proof
let e be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not e in proj1 p or p . e in (the_Values_of SCM) . e )
assume A12: e in dom p ; ::_thesis: p . e in (the_Values_of SCM) . e
then A13: ex y being set st S1[e,y] by A9;
reconsider o = e as Object of SCM by A12, A9;
A14: Values o = INT by A13, AMI_3:11;
consider k being Element of NAT  such that
A15: ( o = dl. k & p . o = D . k ) by A10, A12;
thus  p . e in (the_Values_of SCM) . e by A14, A15, INT_1:def_2; ::_thesis: verum
end;
then reconsider p = p as PartState of SCM by A11;
take s = the State of SCM +* p; ::_thesis: for k being Element of NAT st k < len D holds
s . (dl. k) = D . k
let k be Element of NAT ; ::_thesis: ( k < len D implies s . (dl. k) = D . k )
assume  k < len D ; ::_thesis: s . (dl. k) = D . k
 ex i being Element of NAT st
( dl. k = dl. i & D . k = D . i ) ;
then A16: dl. k in dom p by A9;
then consider i being Element of NAT  such that
A17: ( dl. k = dl. i & p . (dl. k) = D . i ) by A10;
A18: k = i by A17, AMI_3:10;
 p c= s by FUNCT_4:25;
hence  s . (dl. k) = D . k by A18, A17, A16, GRFUNC_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines State-consisting SCM_1:def_1_:_
 for D being XFinSequence of INT
for b2 being State of SCM holds
( b2 is State-consisting of D iff for k being Element of NAT st k < len D holds
b2 . (dl. k) = D . k );

registration
let D be XFinSequence of INT ;
let il be Element of NAT ;
clusterV4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total il -started for State-consisting of D;
existence
 ex b1 being State-consisting of D st b1 is il -started
proof
set s = the State-consisting of D;
set s1 = the State-consisting of D +* (Start-At (il,SCM));
 for k being Element of NAT st k < len D holds
( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k
proof
let k be Element of NAT ; ::_thesis: ( k < len D implies ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k )
assume A1: k < len D ; ::_thesis: ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k
A2: dom (Start-At (il,SCM)) = {(IC )} by FUNCOP_1:13;
 dl. k <> IC by AMI_3:13;
then  not dl. k in dom (Start-At (il,SCM)) by A2, TARSKI:def_1;
hence ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = the State-consisting of D . (dl. k) by FUNCT_4:11
.= D . k by A1, Def1 ;
::_thesis: verum
end;
then reconsider s1 = the State-consisting of D +* (Start-At (il,SCM)) as State-consisting of D by Def1;
take  s1 ; ::_thesis: s1 is il -started
thus  IC s1 = il by MEMSTR_0:16; :: according to MEMSTR_0:def_12 ::_thesis: verum
end;
end;

theorem :: SCM_1:1
for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being b5 -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 )
proof
let i1, i2, i3, i4 be Integer; ::_thesis: for il being Element of NAT
for s being b1 -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 )
let il be Element of NAT ; ::_thesis: for s being il -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 )
let s be il -started State-consisting of <%i1,i2,i3,i4%>; ::_thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )
set D = <%i1,i2,i3,i4%>;
A2: ( <%i1,i2,i3,i4%> . 2 = i3 & <%i1,i2,i3,i4%> . 3 = i4 ) by AFINSQ_1:85;
A3: ( len <%i1,i2,i3,i4%> = 4 & 0 + 0 = 0 ) by AFINSQ_1:84;
 ( <%i1,i2,i3,i4%> . 0 = i1 & <%i1,i2,i3,i4%> . 1 = i2 ) by AFINSQ_1:85;
hence  ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) by A2, A3, Def1; ::_thesis: verum
end;

theorem Th2: :: SCM_1:2
for i1, i2 being Integer
for il being Element of NAT
for s being b3 -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
proof
let i1, i2 be Integer; ::_thesis: for il being Element of NAT
for s being b1 -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
let il be Element of NAT ; ::_thesis: for s being il -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
let s be il -started State-consisting of <%i1,i2%>; ::_thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
set data = <%i1,i2%>;
A3: ( len <%i1,i2%> = 2 & <%i1,i2%> . 0 = i1 ) by AFINSQ_1:38;
 <%i1,i2%> . 1 = i2 by AFINSQ_1:38;
hence  ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by A3, Def1; ::_thesis: verum
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 )
proof
let I1, I2 be Instruction of SCM; ::_thesis: for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds
( F . 0 = I1 & F . 1 = I2 )
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%I1%> ^ <%I2%> c= F implies ( F . 0 = I1 & F . 1 = I2 ) )
assume A1: <%I1%> ^ <%I2%> c= F ; ::_thesis: ( F . 0 = I1 & F . 1 = I2 )
set ins = <%I1%> ^ <%I2%>;
A2: <%I1%> ^ <%I2%> = <%I1,I2%> ;
then A3: (<%I1%> ^ <%I2%>) . 1 = I2 by AFINSQ_1:38;
A4: (<%I1%> ^ <%I2%>) . 0 = I1 by A2, AFINSQ_1:38;
 len (<%I1%> ^ <%I2%>) = 2 by A2, AFINSQ_1:38;
then  ( 0 in dom (<%I1%> ^ <%I2%>) & 1 in dom (<%I1%> ^ <%I2%>) ) by CARD_1:50, TARSKI:def_2;
hence  ( F . 0 = I1 & F . 1 = I2 ) by A1, A3, A4, GRFUNC_1:2; ::_thesis: verum
end;

 Lm1:  for F being NAT -defined the InstructionsF of SCM -valued total Function
for k being Element of 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
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: for k being Element of NAT
for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let k be Element of NAT ; ::_thesis: for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let s be State of SCM; ::_thesis: Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
thus  Comput (F,s,(k + 1)) = Following (F,(Comput (F,s,k))) by EXTPRO_1:3
.= Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) ; ::_thesis: verum
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_)
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))) = succ (IC (Comput (F,s,k))) by A2, AMI_3:2, AMI_3:3, AMI_3:4, AMI_3:5, AMI_3:6
.= n + 1 by A1 ;
::_thesis: verum
end;

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 ) )
proof
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 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 ) )
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 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = a := b implies ( 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 ) ) )
assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( not F . n = a := b or ( 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 ) ) )
assume A2: F . n = a := b ; ::_thesis: ( 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 ) )
then  Comput (F,s,(k + 1)) = Exec ((a := b),(Comput (F,s,k))) by A1, Lm2;
hence  ( 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 ) ) by A1, A2, Lm2, AMI_3:2; ::_thesis: verum
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 ) )
proof
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 = 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 ) )
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 = 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = AddTo (a,b) implies ( 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 ) ) )
assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( not F . n = AddTo (a,b) or ( 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 ) ) )
assume A2: F . n = AddTo (a,b) ; ::_thesis: ( 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 ) )
then  Comput (F,s,(k + 1)) = Exec ((AddTo (a,b)),(Comput (F,s,k))) by A1, Lm2;
hence  ( 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 ) ) by A1, A2, Lm2, AMI_3:3; ::_thesis: verum
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 ) )
proof
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 = 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 ) )
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 = 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) implies ( 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 ) ) )
assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( not F . n = SubFrom (a,b) or ( 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 ) ) )
assume A2: F . n = SubFrom (a,b) ; ::_thesis: ( 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 ) )
then  Comput (F,s,(k + 1)) = Exec ((SubFrom (a,b)),(Comput (F,s,k))) by A1, Lm2;
hence  ( 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 ) ) by A1, A2, Lm2, AMI_3:4; ::_thesis: verum
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 ) )
proof
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 = 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 ) )
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 = 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) implies ( 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 ) ) )
assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( not F . n = MultBy (a,b) or ( 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 ) ) )
assume A2: F . n = MultBy (a,b) ; ::_thesis: ( 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 ) )
then  Comput (F,s,(k + 1)) = Exec ((MultBy (a,b)),(Comput (F,s,k))) by A1, Lm2;
hence  ( 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 ) ) by A1, A2, Lm2, AMI_3:5; ::_thesis: verum
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 ) )
proof
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 = 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 ) )
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 = 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b implies ( 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 ) ) )
assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( not F . n = Divide (a,b) or not a <> b or ( 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 ) ) )
assume A2: ( F . n = Divide (a,b) & a <> b ) ; ::_thesis: ( 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 ) )
then  Comput (F,s,(k + 1)) = Exec ((Divide (a,b)),(Comput (F,s,k))) by A1, Lm2;
hence  ( 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 ) ) by A1, A2, Lm2, AMI_3:6; ::_thesis: verum
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 ) )
proof
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 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 ) )
let k, n be Element of NAT ; ::_thesis: 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let il be Element of NAT ; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = SCM-goto il implies ( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )
assume A1: ( IC (Comput (F,s,k)) = n & F . n = SCM-goto il ) ; ::_thesis: ( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
set csk1 = Comput (F,s,(k + 1));
set csk = Comput (F,s,k);
A2: dom F = NAT by PARTFUN1:def_2;
A3: Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1
.= Exec ((SCM-goto il),(Comput (F,s,k))) by A1, A2, PARTFUN1:def_6 ;
hence  IC (Comput (F,s,(k + 1))) = il by AMI_3:7; ::_thesis: for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d
thus  for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d by A3, AMI_3:7; ::_thesis: verum
end;

theorem Th10: :: SCM_1:10
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 ) )
proof
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 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 ) )
let k, n be Element of NAT ; ::_thesis: 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a be Data-Location; ::_thesis: 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 ) )
let il be Element of NAT ; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = a =0_goto il implies ( ( (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 ) ) )
assume that
A1: IC (Comput (F,s,k)) = n and
A2: F . n = a =0_goto il ; ::_thesis: ( ( (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 ) )
set csk1 = Comput (F,s,(k + 1));
set csk = Comput (F,s,k);
A3: dom F = NAT by PARTFUN1:def_2;
A4: Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1
.= Exec ((a =0_goto il),(Comput (F,s,k))) by A1, A2, A3, PARTFUN1:def_6 ;
hence  ( (Comput (F,s,k)) . a = 0 implies IC (Comput (F,s,(k + 1))) = il ) by AMI_3:8; ::_thesis: ( ( (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 ) )
hereby  ::_thesis: for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d
assume  (Comput (F,s,k)) . a <> 0 ; ::_thesis: IC (Comput (F,s,(k + 1))) = n + 1
hence  IC (Comput (F,s,(k + 1))) = succ n by A1, A4, AMI_3:8
.= n + 1 ;
::_thesis: verum
end;
thus  for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d by A4, AMI_3:8; ::_thesis: verum
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 ) )
proof
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 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 ) )
let k, n be Element of NAT ; ::_thesis: 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 ) )
let s be State of SCM; ::_thesis: 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 ) )
let a be Data-Location; ::_thesis: 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 ) )
let il be Element of NAT ; ::_thesis: ( IC (Comput (F,s,k)) = n & F . n = a >0_goto il implies ( ( (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 ) ) )
assume that
A1: IC (Comput (F,s,k)) = n and
A2: F . n = a >0_goto il ; ::_thesis: ( ( (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 ) )
set csk1 = Comput (F,s,(k + 1));
set csk = Comput (F,s,k);
A3: dom F = NAT by PARTFUN1:def_2;
A4: Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1
.= Exec ((a >0_goto il),(Comput (F,s,k))) by A1, A2, A3, PARTFUN1:def_6 ;
hence  ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) by AMI_3:9; ::_thesis: ( ( (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 ) )
hereby  ::_thesis: for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d
assume  (Comput (F,s,k)) . a <= 0 ; ::_thesis: IC (Comput (F,s,(k + 1))) = n + 1
hence  IC (Comput (F,s,(k + 1))) = succ n by A1, A4, AMI_3:9
.= n + 1 ;
::_thesis: verum
end;
thus  for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d by A4, AMI_3:9; ::_thesis: verum
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, RECDEF_2:def_1;

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%>
proof
let i1, i2, i3, i4 be Integer; ::_thesis: 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%>
let s be State of SCM; ::_thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 implies s is State-consisting of <%i1,i2,i3,i4%> )
assume A1: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) ; ::_thesis: s is State-consisting of <%i1,i2,i3,i4%>
set D = <%i1,i2,i3,i4%>;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_len_<%i1,i2,i3,i4%>_holds_
s_._(dl._k)_=_<%i1,i2,i3,i4%>_._k
let k be Element of NAT ; ::_thesis: ( k < len <%i1,i2,i3,i4%> implies s . (dl. k) = <%i1,i2,i3,i4%> . k )
A2: ( len <%i1,i2,i3,i4%> = 4 & 4 = 3 + 1 ) by AFINSQ_1:84;
assume  k < len <%i1,i2,i3,i4%> ; ::_thesis: s . (dl. k) = <%i1,i2,i3,i4%> . k
then  k <= 3 by A2, NAT_1:13;
then  ( k = 0 or k = 1 or k = 2 or k = 3 ) by NAT_1:27;
hence  s . (dl. k) = <%i1,i2,i3,i4%> . k by A1, AFINSQ_1:85; ::_thesis: verum
end;
hence  s is State-consisting of <%i1,i2,i3,i4%> by Def1; ::_thesis: verum
end;

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 )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(halt SCM)%> c= F implies for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s ) )
assume A1: <%(halt SCM)%> c= F ; ::_thesis: for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
let s be 0 -started State-consisting of <*> INT; ::_thesis: ( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
 1 = dom <%(halt SCM)%> by AFINSQ_1:33;
then  0 in dom <%(halt SCM)%> by CARD_1:49, TARSKI:def_1;
then A2: F . (0 + 0) = <%(halt SCM)%> . 0 by A1, GRFUNC_1:2
.= halt SCM by AFINSQ_1:34 ;
A3: s = Comput (F,s,0) by EXTPRO_1:2;
 F . (IC s) = halt SCM by A2, MEMSTR_0:def_11;
hence A4: F halts_on s by A3, EXTPRO_1:30; ::_thesis: ( LifeSpan (F,s) = 0 & Result (F,s) = s )
 dom F = NAT by PARTFUN1:def_2;
then  CurInstr (F,s) = F . (IC s) by PARTFUN1:def_6
.= halt SCM by A2, MEMSTR_0:def_11 ;
hence  LifeSpan (F,s) = 0 by A4, A3, EXTPRO_1:def_15; ::_thesis: Result (F,s) = s
 IC s = 0 by MEMSTR_0:def_11;
hence  Result (F,s) = s by A2, A3, EXTPRO_1:31; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( 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 ) )
set s1 = Comput (F,s,(0 + 1));
A2: s . (dl. 1) = i2 by Th2;
A3: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def_11;
A4: F . 0 = (dl. 0) := (dl. 1) by A1, Th3;
then A5: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A3, Th4;
A6: F . 1 = halt SCM by A1, Th3;
hence  F halts_on s by A5, EXTPRO_1:30; ::_thesis: ( 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 ) )
thus  LifeSpan (F,s) = 1 by A6, A3, A5, EXTPRO_1:33; ::_thesis: ( (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
 (Comput (F,s,(0 + 1))) . (dl. 0) = s . (dl. 1) by A4, A3, Th4;
hence  (Result (F,s)) . (dl. 0) = i2 by A6, A2, A5, EXTPRO_1:31; ::_thesis: for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: ( d <> dl. 0 implies (Result (F,s)) . d = s . d )
assume A7: d <> dl. 0 ; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A6, A5, EXTPRO_1:31
.= s . d by A4, A3, A7, Th4 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( 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 ) )
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A2: s = Comput (F,s,0) by EXTPRO_1:2;
A3: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by Th2;
A4: IC s = 0 by MEMSTR_0:def_11;
A5: F . 0 = AddTo ((dl. 0),(dl. 1)) by A1, Th3;
then A6: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A4, A2, Th5;
A7: F . 1 = halt SCM by A1, Th3;
hence  F halts_on s by A6, EXTPRO_1:30; ::_thesis: ( 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 ) )
thus  LifeSpan (F,s) = 1 by A4, A7, A2, A6, EXTPRO_1:33; ::_thesis: ( (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
 (Comput (F,s,(0 + 1))) . (dl. 0) = ((Comput (F,s,0)) . (dl. 0)) + ((Comput (F,s,0)) . (dl. 1)) by A4, A5, A2, Th5;
hence  (Result (F,s)) . (dl. 0) = i1 + i2 by A7, A3, A2, A6, EXTPRO_1:31; ::_thesis: for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: ( d <> dl. 0 implies (Result (F,s)) . d = s . d )
assume A8: d <> dl. 0 ; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A7, A6, EXTPRO_1:31
.= s . d by A4, A5, A2, A8, Th5 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( 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 ) )
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A2: s = Comput (F,s,0) by EXTPRO_1:2;
A3: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by Th2;
A4: IC s = 0 by MEMSTR_0:def_11;
A5: F . 0 = SubFrom ((dl. 0),(dl. 1)) by A1, Th3;
then A6: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A4, A2, Th6;
A7: F . 1 = halt SCM by A1, Th3;
hence  F halts_on s by A6, EXTPRO_1:30; ::_thesis: ( 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 ) )
thus  LifeSpan (F,s) = 1 by A4, A7, A2, A6, EXTPRO_1:33; ::_thesis: ( (Result (F,s)) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
 (Comput (F,s,(0 + 1))) . (dl. 0) = ((Comput (F,s,0)) . (dl. 0)) - ((Comput (F,s,0)) . (dl. 1)) by A4, A5, A2, Th6;
hence  (Result (F,s)) . (dl. 0) = i1 - i2 by A7, A3, A2, A6, EXTPRO_1:31; ::_thesis: for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: ( d <> dl. 0 implies (Result (F,s)) . d = s . d )
assume A8: d <> dl. 0 ; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A7, A6, EXTPRO_1:31
.= s . d by A4, A5, A2, A8, Th6 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( 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 ) )
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A2: s = Comput (F,s,0) by EXTPRO_1:2;
A3: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by Th2;
A4: IC s = 0 by MEMSTR_0:def_11;
A5: F . 0 = MultBy ((dl. 0),(dl. 1)) by A1, Th3;
then A6: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A4, A2, Th7;
A7: F . 1 = halt SCM by A1, Th3;
hence  F halts_on s by A6, EXTPRO_1:30; ::_thesis: ( 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 ) )
thus  LifeSpan (F,s) = 1 by A4, A7, A2, A6, EXTPRO_1:33; ::_thesis: ( (Result (F,s)) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
 (Comput (F,s,(0 + 1))) . (dl. 0) = ((Comput (F,s,0)) . (dl. 0)) * ((Comput (F,s,0)) . (dl. 1)) by A4, A5, A2, Th7;
hence  (Result (F,s)) . (dl. 0) = i1 * i2 by A7, A3, A2, A6, EXTPRO_1:31; ::_thesis: for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: ( d <> dl. 0 implies (Result (F,s)) . d = s . d )
assume A8: d <> dl. 0 ; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A7, A6, EXTPRO_1:31
.= s . d by A4, A5, A2, A8, Th7 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( 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 ) )
set s1 = Comput (F,s,(0 + 1));
A2: dl. 0 <> dl. 1 by AMI_3:10;
A3: ( IC s = 0 & F . 0 = Divide ((dl. 0),(dl. 1)) ) by A1, Th3, MEMSTR_0:def_11;
A4: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by Th2;
A5: s = Comput (F,s,0) by EXTPRO_1:2;
 F . 1 = halt SCM by A1, Th3;
then A6: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A3, A2, A5, Th8;
hence  F halts_on s by EXTPRO_1:30; ::_thesis: ( 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 ) )
 Divide ((dl. 0),(dl. 1)) <> halt SCM by Th12;
hence  LifeSpan (F,s) = 1 by A3, A5, A6, EXTPRO_1:32; ::_thesis: ( (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 ) )
thus (Result (F,s)) . (dl. 0) = (Comput (F,s,(0 + 1))) . (dl. 0) by A6, EXTPRO_1:31
.= i1 div i2 by A3, A4, A2, A5, Th8 ; ::_thesis: ( (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 ) )
thus (Result (F,s)) . (dl. 1) = (Comput (F,s,(0 + 1))) . (dl. 1) by A6, EXTPRO_1:31
.= i1 mod i2 by A3, A4, A2, A5, Th8 ; ::_thesis: for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: ( d <> dl. 0 & d <> dl. 1 implies (Result (F,s)) . d = s . d )
assume A7: ( d <> dl. 0 & d <> dl. 1 ) ; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A6, EXTPRO_1:31
.= s . d by A3, A2, A5, A7, Th8 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%(SCM-goto 1)%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%(SCM-goto 1)%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
set s1 = Comput (F,s,(0 + 1));
A2: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def_11;
A3: F . 0 = SCM-goto 1 by A1, Th3;
then A4: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, Th9;
A5: F . 1 = halt SCM by A1, Th3;
hence  F halts_on s by A4, EXTPRO_1:30; ::_thesis: ( LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
thus  LifeSpan (F,s) = 1 by A5, A2, A4, EXTPRO_1:33; ::_thesis: for d being Data-Location holds (Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A5, A4, EXTPRO_1:31
.= s . d by A3, A2, Th9 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
set s1 = Comput (F,s,(0 + 1));
A2: F . 0 = (dl. 0) =0_goto 1 by A1, Th3;
A3: F . 1 = halt SCM by A1, Th3;
A4: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def_11;
 s . (dl. 0) = i1 by Th2;
then A5: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, A4, Th10;
hence  F halts_on s by A3, EXTPRO_1:30; ::_thesis: ( LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
thus  LifeSpan (F,s) = 1 by A3, A4, A5, EXTPRO_1:33; ::_thesis: for d being Data-Location holds (Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A3, A5, EXTPRO_1:31
.= s . d by A2, A4, Th10 ; ::_thesis: verum
end;

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 ) )
proof
let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: ( <%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> c= F implies 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 ) ) )
assume A1: <%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> c= F ; ::_thesis: 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 ) )
let i1, i2 be Integer; ::_thesis: 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 ) )
let s be 0 -started State-consisting of <%i1,i2%>; ::_thesis: ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
set s1 = Comput (F,s,(0 + 1));
A2: F . 0 = (dl. 0) >0_goto 1 by A1, Th3;
A3: F . 1 = halt SCM by A1, Th3;
A4: ( IC s = 0 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def_11;
 s . (dl. 0) = i1 by Th2;
then A5: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, A4, Th11;
hence  F halts_on s by A3, EXTPRO_1:30; ::_thesis: ( LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
thus  LifeSpan (F,s) = 1 by A3, A4, A5, EXTPRO_1:33; ::_thesis: for d being Data-Location holds (Result (F,s)) . d = s . d
let d be Data-Location; ::_thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A3, A5, EXTPRO_1:31
.= s . d by A2, A4, Th11 ; ::_thesis: verum
end;

theorem :: SCM_1:23
for s being State of SCM holds s is State-consisting of <*> INT
proof
let s be State of SCM; ::_thesis: s is State-consisting of <*> INT
let k be Element of NAT ; :: according to SCM_1:def_1 ::_thesis: ( k < len (<*> INT) implies s . (dl. k) = (<*> INT) . k )
thus  ( k < len (<*> INT) implies s . (dl. k) = (<*> INT) . k ) ; ::_thesis: verum
end;