:: Development of Terminology for {\bf SCM}
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, INT_1, FINSEQ_1, SUBSET_1, FSM_1, AMI_3, PARTFUN1,
      AMI_1, EXTPRO_1, RELAT_1, FUNCT_1, CIRCUIT2, MSUALG_1, ARYTM_3, XXREAL_0,
      CARD_1, TARSKI, AFINSQ_1, ORDINAL4, GRAPHSP, ARYTM_1, SCM_1, STRUCT_0,
      RECDEF_2, FUNCT_4, CAT_1, GOBRD13, MEMSTR_0, NAT_1;
 notations TARSKI, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
      INT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, XXREAL_0, AFINSQ_1, FUNCT_4,
      RECDEF_2, STRUCT_0, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_3;
 constructors AMI_3, RELSET_1, PRE_POLY, XTUPLE_0;
 registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, AMI_3,
      AFINSQ_1, RELAT_1, PBOOLE, FINSEQ_1, STRUCT_0, VALUED_0, FUNCT_4,
      COMPOS_0, XTUPLE_0, MEMSTR_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RELAT_1, FUNCT_1, MEMSTR_0;
 equalities AFINSQ_1, EXTPRO_1, NAT_1, AMI_3, FUNCOP_1, MEMSTR_0;
 theorems NAT_1, INT_1, AMI_3, AFINSQ_1, PARTFUN1, FUNCT_4, FUNCOP_1, TARSKI,
      EXTPRO_1, GRFUNC_1, CARD_1, MEMSTR_0;
 schemes PARTFUN1;

begin

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

definition
  let D be XFinSequence of INT;
  mode State-consisting of D -> State of SCM means
:Def1:
   for k being Element of NAT st k < len D holds it.dl.k = D.k;
  existence
  proof
    defpred P[object,object] means
     ex k being Element of NAT st $1 = dl.k & $2 = D.k;
A1: for x,y being object
     st x in the carrier of SCM & P[x,y] holds y in INT by INT_1:def 2;
A2: for x,y1,y2 being object
     st x in the carrier of SCM & P[x,y1] & P[x,y2] holds y1 = y2 by AMI_3:10;
    consider p being PartFunc of SCM,INT such that
A3: for x being object
      holds x in dom p iff x in the carrier of SCM &
       ex y being object st P[x,y] and
A4: for x being object st x in dom p holds P[x,p.x]
      from PARTFUN1:sch 2(A1,A2);
A5:  p is (the carrier of SCM)-defined
     proof
      let e be object;
      thus thesis by A3;
     end;
    p is (the_Values_of SCM)-compatible
     proof let e be object;
      assume
A6:     e in dom p;
       then
A7:    ex y being object st P[e,y] by A3;
       reconsider o = e as Object of SCM by A6,A3;
A8:     Values o = INT by A7,AMI_3:11;
       consider k being Element of NAT such that
A9:     o = dl.k & p.o = D.k by A4,A6;
      thus p.e in (the_Values_of SCM).e by A8,A9,INT_1:def 2;
     end;
    then reconsider p as PartState of SCM by A5;
   take s = (the State of SCM)+*p;
   let k be Element of NAT;
   assume k < len D;
    ex i being Element of NAT st dl.k = dl.i & D.k = D.i;
    then
A10:   dl.k in dom p by A3;
    then consider i being Element of NAT such that
A11:  dl.k = dl.i & p.dl.k = D.i by A4;
A12:  k = i by A11,AMI_3:10;
    p c= s by FUNCT_4:25;
   hence s.dl.k = D.k by A12,A11,A10,GRFUNC_1:2;
  end;
end;

registration
  let D be XFinSequence of INT, il be Element of NAT;
 cluster il-started for State-consisting of D;
 existence
  proof
   set s = the State-consisting of D;
   set s1 = s +* Start-At(il,SCM);
   for k being Element of NAT st k < len D holds s1.dl.k = D.k
    proof let k be Element of NAT;
     assume
A1:    k < len D;
A2:   dom Start-At(il,SCM) = {IC SCM} by FUNCOP_1:13;
      dl.k <> IC SCM by AMI_3:13;
     then not dl.k in dom Start-At(il,SCM) by A2,TARSKI:def 1;
     hence s1.dl.k = s.dl.k by FUNCT_4:11
        .= D.k by A1,Def1;
    end;
   then reconsider s1 as State-consisting of D by Def1;
   take s1;
   thus IC s1 = il by MEMSTR_0:16;
  end;
end;

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

theorem Th2:
  for i1, i2 being Integer, il being Element of NAT,
  s being il-started State-consisting of <%i1,i2%> holds
   s.dl.0 = i1 & s.dl.1 = i2
proof
  let i1, i2 be Integer, il be Element of NAT,
      s be il-started State-consisting of <%i1,i2%>;
  set data = <%i1,i2%>;
A1: len data = 2 & data.0 = i1 by AFINSQ_1:38;
 data.1 = i2;
  hence thesis by A1,Def1;
end;

theorem Th3:
  for I1, I2 being Instruction of SCM
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
   st <%I1%>^<%I2%> c= F
   holds F.0 = I1 & F.1 = I2
proof
  let I1, I2 be Instruction of SCM;
  let F be total
   NAT-defined the InstructionsF of SCM-valued Function such that
A1: <%I1%>^<%I2%> c= F;
  set ins = <%I1%>^<%I2%>;
A2: ins = <%I1, I2%>;
  then
A3: ins.1 = I2;
A4:  ins.0 = I1 by A2;
    len ins = 2 by A2,AFINSQ_1:38;
   then 0 in dom ins & 1 in dom ins by CARD_1:50,TARSKI:def 2;
  hence thesis by A1,A3,A4,GRFUNC_1:2;
end;

reserve F for total
  NAT-defined (the InstructionsF of SCM)-valued Function;

Lm1:
 for k being Nat, s being State of SCM
 holds Comput(F,s,k+1) = Exec(CurInstr(F,Comput(F,s,k)),Comput(F,s,k))
proof
  let k be Nat, s be State of SCM;
  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));
end;

Lm2: now
   let F be total
  NAT-defined (the InstructionsF of SCM)-valued Function;
  let k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k) = n;
  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);
A3: dom F = NAT by PARTFUN1:def 2;
  thus csk1 = (Exec(CurInstr(F,csk), csk)) by Lm1
    .= Exec(F.n, csk) by A1,A3,PARTFUN1:def 6;
  hence IC csk1 = IC csk + 1 by A2,AMI_3:2,3,4,5,6
    .= n+1 by A1;
end;

theorem Th4:
  for k, n being Element of NAT, s being State of SCM,
    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 k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k) = n;
  assume
 F.n = a := b;
  then Comput(F,s,k+1)
   = Exec(a:=b, Comput(F,s,k)) by A1,Lm2;
  hence thesis by A1,AMI_3:2;
end;

theorem Th5:
  for k, n being Element of NAT, s being State of SCM, 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 k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k) = n;
  assume
 F.n = AddTo(a,b);
  then Comput(F,s,k+1)
   = Exec(AddTo(a,b), Comput(F,s,k)) by A1,Lm2;
  hence thesis by A1,AMI_3:3;
end;

theorem Th6:
  for k, n being Element of NAT, s being State of SCM, 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 k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k)= n;
  assume
 F.n = SubFrom(a,b);
  then Comput(F,s,k+1) =
   Exec(SubFrom(a,b), Comput(F,s,k)) by A1,Lm2;
  hence thesis by A1,AMI_3:4;
end;

theorem Th7:
  for k, n being Element of NAT, s being State of SCM, 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 k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k) = n;
  assume
 F.n = MultBy(a,b);
  then Comput(F,s,k+1)
   = Exec(MultBy(a,b), Comput(F,s,k)) by A1,Lm2;
  hence thesis by A1,AMI_3:5;
end;

theorem Th8:
  for k, n being Element of NAT, s being State of SCM, 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 k, n be Element of NAT, s be State of SCM, a, b be Data-Location;
  assume
A1: IC Comput(F,s,k) = n;
  assume
A2: F.n = Divide(a,b) & a <> b;
  then Comput(F,s,k+1)
   = Exec(Divide(a,b), Comput(F,s,k)) by A1,Lm2;
  hence thesis by A1,A2,AMI_3:6;
end;

theorem Th9:
  for k, n being Element of NAT, s being State of SCM, 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 k, n be Element of NAT, s be State of SCM, il be Element of NAT;
  assume
A1: IC Comput(F,s,k) = n & F.n = SCM-goto il;
  set csk1 = Comput(F,s,k+1);
  set csk = Comput(F,s,k);
A2:  dom F = NAT by PARTFUN1:def 2;
A3: csk1 = Exec(CurInstr(F,csk), csk) by Lm1
    .= Exec(SCM-goto il, csk) by A1,A2,PARTFUN1:def 6;
  hence IC csk1 = il by AMI_3:7;
  thus thesis by A3,AMI_3:7;
end;

theorem Th10:
  for k, n being Nat, s being State of SCM, a being
  Data-Location, 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 k, n be Nat, s be State of SCM, a be Data-Location, il be
  Element of NAT;
  assume that
A1: IC Comput(F,s,k) = n and
A2: F.n = a =0_goto il;
  set csk1 = Comput(F,s,k+1);
  set csk = Comput(F,s,k);
A3:  dom F = NAT by PARTFUN1:def 2;
A4: csk1 = Exec(CurInstr(F,csk), csk) by Lm1
    .= Exec(a =0_goto il, csk) by A1,A2,A3,PARTFUN1:def 6;
  hence csk.a = 0 implies IC csk1 = il by AMI_3:8;
  thus thesis by A1,A4,AMI_3:8;
end;

theorem Th11:
  for k, n being Element of NAT, s being State of SCM, a being
  Data-Location, 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 k, n be Element of NAT, s be State of SCM, a be Data-Location, il be
  Element of NAT;
  assume that
A1: IC Comput(F,s,k) = n and
A2: F.n = a >0_goto il;
  set csk1 = Comput(F,s,k+1);
  set csk = Comput(F,s,k);
A3:  dom F = NAT by PARTFUN1:def 2;
  csk1 = Exec(CurInstr(F,csk), csk) by Lm1
    .= Exec(a >0_goto il, csk) by A1,A2,A3,PARTFUN1:def 6;
 hence thesis by A1,AMI_3:9;
end;

theorem Th12:
  (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, i being Element of NAT
   holds (a =0_goto i)`1_3 = 7) &
  for a being Data-Location, i being Element of NAT holds
   (a >0_goto i)`1_3 = 8 by AMI_3:26;

theorem
  for i1, i2, i3, i4 being Integer,
  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, s be State of SCM such that
A1: s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4;
  set D = <%i1,i2,i3,i4%>;
  now
    let k be Element of NAT;
A2: len D=4 & 4=3+1 by AFINSQ_1:84;
    assume k < len D;
    then k <= 3 by A2,NAT_1:13;
    then k=0 or ... or k=3;
    hence s.dl.k=D.k by A1;
  end;
  hence thesis by Def1;
end;

:: Empty program

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%halt SCM%> c= F
  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 total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%halt SCM%> c= F;
  let s be 0-started State-consisting of <*>INT;
  1 = len <%halt SCM%> by AFINSQ_1:34;
  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;
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;
  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;
  IC s = 0 by MEMSTR_0:def 11;
  hence thesis by A2,A3,EXTPRO_1:7;
end;

:: Assignment

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0 := dl.1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      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 total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%dl.0 := dl.1%>^<%halt SCM%> c= F;
  let i1, i2 be Integer,
    s be 0-started State-consisting of <%i1,i2%>;
  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 s1 = 0+1 by A3,Th4;
A6: F.1 = halt SCM by A1,Th3;
  hence F halts_on s by A5,EXTPRO_1:30;
  thus LifeSpan(F,s) = 1 by A6,A3,A5,EXTPRO_1:33;
  s1.dl.0 = s.dl.1 by A4,A3,Th4;
  hence (Result(F,s)).dl.0 = i2 by A6,A2,A5,EXTPRO_1:7;
  let d be Data-Location;
  assume
A7: d<>dl.0;
  thus (Result(F,s)).d = s1.d by A6,A5,EXTPRO_1:7
    .= s.d by A4,A3,A7,Th4;
end;

:: Adding two integers

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

:: Subtracting two integers

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

:: Multiplying two integers

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

:: Dividing two integers

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%Divide(dl.0,dl.1)%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
    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 being total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%Divide(dl.0,dl.1)%>^<%halt SCM%> c= F;
  let i1, i2 be Integer,
      s be 0-started State-consisting of  <%i1,i2%>;
  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 s1) = halt SCM by A3,A2,A5,Th8;
  hence F halts_on s by EXTPRO_1:30;
  Divide(dl.0, dl.1) <> halt SCM by Th12;
  hence LifeSpan(F,s) = 1 by A3,A5,A6,EXTPRO_1:32;
  thus (Result(F,s)).dl.0 = s1.dl.0 by A6,EXTPRO_1:7
    .= i1 div i2 by A3,A4,A2,A5,Th8;
  thus (Result(F,s)).dl.1 = s1.dl.1 by A6,EXTPRO_1:7
    .= i1 mod i2 by A3,A4,A2,A5,Th8;
  let d be Data-Location;
  assume
A7: d<>dl.0 & d<>dl.1;
  thus (Result(F,s)).d = s1.d by A6,EXTPRO_1:7
    .= s.d by A3,A2,A5,A7,Th8;
end;

:: Unconditional jump

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%SCM-goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      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 being total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%SCM-goto 1%>^<%halt SCM%> c= F;
  let i1, i2 be Integer,
      s be 0-started State-consisting of <%i1,i2%>;
  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 s1 = (0+1) by A2,Th9;
A5: F.1 = halt SCM by A1,Th3;
  hence F halts_on s by A4,EXTPRO_1:30;
  thus LifeSpan(F,s) = 1 by A5,A2,A4,EXTPRO_1:33;
  let d be Data-Location;
  thus (Result(F,s)).d = s1.d by A5,A4,EXTPRO_1:7
    .= s.d by A3,A2,Th9;
end;

:: Jump at zero

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0=0_goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      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 being total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%dl.0=0_goto 1%>^<%halt SCM%> c= F;
  let i1, i2 be Integer,
      s be 0-started State-consisting of <%i1,i2%>;
  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 s1 = (0+1) by A2,A4,Th10;
  hence F halts_on s by A3,EXTPRO_1:30;
  thus LifeSpan(F,s) = 1 by A3,A4,A5,EXTPRO_1:33;
  let d be Data-Location;
  thus (Result(F,s)).d = s1.d by A3,A5,EXTPRO_1:7
    .= s.d by A2,A4,Th10;
end;

:: Jump at greater than zero

theorem
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0>0_goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      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 being total
   NAT-defined (the InstructionsF of SCM)-valued Function such that
A1: <%dl.0>0_goto 1%>^<%halt SCM%> c= F;
  let i1, i2 be Integer,
      s be 0-started State-consisting of <%i1,i2%>;
  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 s1 = (0+1) by A2,A4,Th11;
  hence F halts_on s by A3,EXTPRO_1:30;
  thus LifeSpan(F,s) = 1 by A3,A4,A5,EXTPRO_1:33;
  let d be Data-Location;
  thus (Result(F,s)).d = s1.d by A3,A5,EXTPRO_1:7
    .= s.d by A2,A4,Th11;
end;

theorem
 for s being State of SCM holds s is State-consisting of <*>INT
 proof let s be State of SCM;
  let k be Element of NAT;
  thus thesis;
 end;