TITLE: A three-parameters identity involving Stirling numbers of both kinds
QUESTION [3 upvotes]: Let $n, m, k $ be three natural numbers, ${n \brack k}$ and ${n \brace k}$ the Stirling numbers of first and second kind respectively.
We have:

$$ \tag{*} {n-1 \choose m}{n-m \brack k}= \sum_i (-1)^{i-m}{k-1+i
 \choose k-1}{i \brace m}{n \brack i+k} $$

where the bounds for $i$ in the sum on the rhs don't need to be specified as there is only a finite number of values of $i$ whose corresponding summand is non-zero and the sum is understood over all such $i$.
This identity can be verified numerically and can be derived from another three parameters identity involving the second kind of Stirling numbers only- namely  Eq. (6.28) in Concrete Mathematics Second Edition, R. L. Graham, D. E. Knuth, O. Patashnik)
$$ \tag{**} {\ell+m \choose \ell}{n \brace \ell+m}= \sum_k {k\brace \ell}{n-k \brace m}{n \choose k} $$
which is obtained rather easily via the exponential generating functions of ${n \brace l+m}$, ${n \brace m}$ and ${n \brace l}$ .
Indeed, if we replace $m$ by $-m$ and $n$ by $-n$ in (**), taking into account that ${-a \brace -b}$ = ${b \brack a}$ and ${-n \choose k}=(-1)^k{n+k-1\choose k}$, we obtain
\begin{align*} {\ell-m \choose \ell}{-n \brace \ell-m}&= \sum_k {k\brace \ell}{-n-k \brace -m}{-n \choose k} \\
(-1)^\ell{m-1 \choose \ell}{m- \ell \brack n}&= \sum_k {k\brace \ell}{m \brack n+k}(-1)^k{n+k-1 \choose k}\end{align*}
which is (*) after the appropriate change of notation.
But in Concrete Mathematics, the identity (**) is given under the condition $\ell,m,n \ge 0$, so I am note sure whether it is licit to do such negation of the indices.
Then my question is: how can we derive (*) directly, without resorting to (**). Maybe with generating functions, coefficient extractors or things like that?

REPLY [2 votes]: We seek to verify that
$$\sum_{q=m}^{n-k} (-1)^{q-m} {k-1+q\choose k-1}
{q\brace m} {n\brack q+k}
= {n-1\choose m} {n-m\brack k}.$$
Using the standard EGFs the LHS becomes
$$\sum_{q=m}^{n-k} (-1)^{q-m} {k-1+q\choose k-1}
q! [z^q] \frac{(\exp(z)-1)^m}{m!}
n! [w^n] \frac{1}{(q+k)!} \left(\log\frac{1}{1-w}\right)^{q+k}
\\ = \frac{n!}{(k-1)! \times m!} [w^n] \sum_{q=m}^{n-k} (-1)^{q-m}
[z^q] (\exp(z)-1)^m
\frac{1}{q+k} \left(\log\frac{1}{1-w}\right)^{q+k}
\\ = \frac{(n-1)!}{(k-1)! \times m!} [w^{n-1}]
\sum_{q=m}^{n-k} (-1)^{q-m}
[z^q] (\exp(z)-1)^m
\left(\log\frac{1}{1-w}\right)^{q+k-1} \frac{1}{1-w}
\\ = \frac{(n-1)!}{(k-1)! \times m!} [w^{n-1}] \frac{1}{1-w}
\\ \times \sum_{q=m}^{n-k} (-1)^{q-m}
[z^{q+k-1}] z^{k-1} (\exp(z)-1)^m
\left(\log\frac{1}{1-w}\right)^{q+k-1}
\\ = \frac{(n-1)!}{(k-1)! \times m!} [w^{n-1}] \frac{1}{1-w}
\\ \times \sum_{q=m+k-1}^{n-1} (-1)^{q-(k-1)-m}
[z^{q}] z^{k-1} (\exp(z)-1)^m
\left(\log\frac{1}{1-w}\right)^{q}.$$
Now as $\log\frac{1}{1-w} = w + \cdots$ when $q\gt n-1$ there is
no contribution from the logarithmic power term due to the coefficient
extractor $[w^{n-1}]$ so we find
$$(-1)^{m+(k-1)} \frac{(n-1)!}{(k-1)! \times m!}
[w^{n-1}] \frac{1}{1-w}
\\ \times \sum_{q\ge m+k-1} (-1)^{q}
\left(\log\frac{1}{1-w}\right)^{q}
[z^{q}] z^{k-1} (\exp(z)-1)^m.$$
Note that $z^{k-1} (\exp(z)-1)^m = z^{m+k-1} + \cdots$ which
means that the remaining sum / coefficient etractor pair covers the
entire series and we get
$$(-1)^{m+(k-1)} \frac{(n-1)!}{(k-1)! \times m!}
[w^{n-1}] \frac{1}{1-w}
\\ \times (-1)^{k-1} \left(\log\frac{1}{1-w}\right)^{k-1}
\left(\exp\left(-\log\frac{1}{1-w}\right)-1\right)^m
\\ = (-1)^{m+(k-1)} \frac{(n-1)!}{(k-1)! \times m!}
[w^{n-1}] \frac{1}{1-w}
\\ \times (-1)^{k-1} \left(\log\frac{1}{1-w}\right)^{k-1} (-w)^m
\\ = \frac{(n-1)!}{(k-1)! \times m!}
[w^{n-1-m}] \frac{1}{1-w}
\left(\log\frac{1}{1-w}\right)^{k-1}
\\ = \frac{(n-1)!}{m!}
[w^{n-1-m}] \frac{1}{1-w}
\frac{1}{(k-1)!} \left(\log\frac{1}{1-w}\right)^{k-1}
\\ = \frac{(n-1)!}{m!}
(n-m) [w^{n-m}]
\frac{1}{k!} \left(\log\frac{1}{1-w}\right)^{k}
\\ = \frac{(n-1)!}{m! \times (n-1-m)!}
(n-m)! [w^{n-m}]
\frac{1}{k!} \left(\log\frac{1}{1-w}\right)^{k}
\\ = {n-1\choose m} {n-m\brack k}.$$
This is the claim.


TITLE: How can I find the point (X, Y, Z) which minimizes this quantity?
QUESTION [2 upvotes]: I have a number of equally powerful light sources $L_i, 1 \le i \le N$ at points within a cube $(x_i, y_i, z_i), -1 \le x_i, y_i, z_i \le 1$. The intensity of each light falls off with distance according to an inverse-square law, as usual. This means that at $(x, y, z)$ the total intensity is given by:
$$\sum_{i = 1}^N \frac{1}{(x - x_i)^2 + (y - y_i)^2 + (z - z_i)^2}$$
What method/algorithm can I use to find the point within the cube $(X, Y, Z), -1 \le X, Y, Z \le 1$ where this quantity is minimal?
How would this method change if I wanted to restrict $(X, Y, Z)$ (but not $(x_i, y_i, z_i)$) to be within a (convex) sub-volume of the cube, e.g. the cylinder $X^2 + Y^2 \le 0.75^2, -0.25 <= Z <= 0.75$?

REPLY [0 votes]: The difficulty of your problem is due to the fact that you have quadratic forms under the fraction bars. In my opinion, there is no quick and easy way to solve this optimization problem as it is non-convex. However, grid-search is not a bad choice here, as you have only three variables. In the latter search prcedure you just try all points inside the cube within a certain grid density. The latter search can also be easily generalized to arbitray search domains (balls, cyliners).


text:
:: Computation of Two Consecutive Program Blocks for SCMPDS
::  by JingChao Chen

environ

 vocabularies NUMBERS, SUBSET_1, SCMPDS_2, AMI_1, FSM_1, INT_1, SETFAM_1,
      RELAT_1, SCMFSA_7, CARD_1, SCMPDS_4, FUNCT_1, AMISTD_2, VALUED_1,
      ARYTM_3, TARSKI, XXREAL_0, TURING_1, FUNCT_4, XBOOLE_0, SCMFSA6B,
      CIRCUIT2, GRAPHSP, MSUALG_1, AMI_2, AMI_3, SCMPDS_1, COMPLEX1, STRUCT_0,
      ARYTM_1, NAT_1, SCMPDS_5, PARTFUN1, EXTPRO_1, SCMFSA6C, COMPOS_1,
      SCMFSA6A;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SETFAM_1, ENUMSET1, SUBSET_1, CARD_1,
      ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1,
      NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, VALUED_1, AMI_2,
      FUNCT_7, SCMPDS_I, SCMPDS_1, SCMPDS_2, INT_2, SCMPDS_4, XXREAL_0;
 constructors ENUMSET1, XXREAL_0, REAL_1, INT_2, SCMPDS_1, SCMPDS_4, PRE_POLY,
      DOMAIN_1, AMI_3, NAT_D, MEMSTR_0, RELSET_1, XTUPLE_0;
 registrations XREAL_0, INT_1, SCMPDS_2, SCMPDS_4, ORDINAL1, AFINSQ_1,
      COMPOS_1, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, COMPOS_0, XTUPLE_0, NAT_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, COMPOS_1, SCMPDS_4, EXTPRO_1, COMPOS_0;
 equalities FUNCOP_1, COMPOS_1, SCMPDS_4, AFINSQ_1, EXTPRO_1, MEMSTR_0,
      COMPOS_0;
 expansions TARSKI, COMPOS_1, SCMPDS_4, EXTPRO_1, COMPOS_0;
 theorems NAT_1, TARSKI, FUNCT_4, FUNCT_1, INT_1, RELAT_1, SCMPDS_2, SCMPDS_3,
      ENUMSET1, ABSVALUE, GRFUNC_1, SCMPDS_4, MEMSTR_0, XBOOLE_0, XBOOLE_1,
      XREAL_1, FUNCOP_1, XXREAL_0, VALUED_1, AFINSQ_1, PBOOLE, PARTFUN1,
      COMPOS_1, EXTPRO_1, AMI_2, COMPOS_0;
 schemes NAT_1;

begin :: Preliminaries

reserve x for set,
  m,n for Nat,
  a,b,c for Int_position,
  i for Instruction of SCMPDS,
  s,s1,s2 for State of SCMPDS,
  k1,k2 for Integer,
  loc,l1 for Nat,
  I,J for Program of SCMPDS,
  N for with_non-empty_elements set;

Lm1: card Stop SCMPDS = 1 by AFINSQ_1:34;

::$CT 11

theorem Th1:
  for I,J being Program of SCMPDS holds I c= stop (I ';' J)
proof
  let I,J be Program of SCMPDS;
  set IS=I ';' (J ';' Stop SCMPDS),
  Ip=stop (I ';' J);
A1: I c= IS by AFINSQ_1:74;
  thus thesis by A1,AFINSQ_1:27;
end;

theorem Th2:
  dom stop I c= dom stop (I ';' J)
proof
  set sI=stop I, sIJ=stop (I ';'J);
A1: card sIJ=card (I ';' J) +1 by Lm1,AFINSQ_1:17
    .=card I + card J +1 by AFINSQ_1:17
    .=card I + 1 + card J;
  card sI=card I +1 by Lm1,AFINSQ_1:17;
  then
A2: card sI <= card sIJ by A1,NAT_1:11;
    set A = NAT;
    let x be object;
    assume
A3: x in dom sI;
    dom sI c= A by RELAT_1:def 18;
    then reconsider l=x as Nat by A3;
    reconsider n = l as Nat;
    n < card sI by A3,AFINSQ_1:66;
    then n < card sIJ by A2,XXREAL_0:2;
    hence x in dom sIJ by AFINSQ_1:66;
end;

theorem Th3:
  for I,J being Program of SCMPDS holds
   stop I +* stop (I ';' J) = stop (I ';' J)
proof
  let I,J be Program of SCMPDS;
  set sI=stop I, IsI=sI, sIJ=stop (I ';' J), IsIJ= sIJ;
  dom sI c= dom sIJ by Th2;
  hence thesis by FUNCT_4:19;
end;

set SA0 = Start-At(0,SCMPDS);

theorem Th4:
  (Initialize s).a = s.a
proof
  not a in dom SA0 by SCMPDS_4:18;
  hence (Initialize s).a =s.a by FUNCT_4:11;
end;

reserve P,P1,P2,Q for Instruction-Sequence of SCMPDS;

theorem Th5:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS
    st stop I c= P1 & stop I c= P2
  for k being Nat holds
    Comput(P1,s,k) =  Comput(P2,s,k) &
   CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k))
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS;
  set SI=stop I;
  assume that
A1: SI c= P1 and
A2: SI c= P2;
    let k be Nat;
A3: IC Comput(P1,s,k) in dom SI by A1,SCMPDS_4:def 6;
A4: IC Comput(P2,s,k) in dom SI by A2,SCMPDS_4:def 6;
    for m being Nat st m < k holds IC(Comput(P2,s,m))
in dom
    SI by A2,SCMPDS_4:def 6;
    hence
A5:   Comput(P1,s,k) =  Comput(P2,s,k) by A1,A2,SCMPDS_4:21;
    thus CurInstr(P2,Comput(P2,s,k))
     = P2.IC Comput(P2,s,k) by PBOOLE:143
      .= SI.IC Comput(P2,s,k) by A2,A4,GRFUNC_1:2
      .= P1.IC Comput(P1,s,k) by A1,A5,A3,GRFUNC_1:2
      .= CurInstr(P1,Comput(P1,s,k)) by PBOOLE:143;
end;

theorem Th6:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS
   st stop I c= P1 & stop I c= P2
  holds LifeSpan(P1,s) = LifeSpan(P2,s) &
   Result(P1,s) =  Result(P2,s)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS;
  set SI=stop I;
  assume that
A1: SI c= P1 and
A2: SI c= P2;
A3: P2 halts_on s by A2,SCMPDS_4:def 7;
A4: P1 halts_on s by A1,SCMPDS_4:def 7;
A5: now
    let l be Nat;
    assume
A6: CurInstr(P2,Comput(P2,s,l)) = halt SCMPDS;
    CurInstr(P1,Comput(P1,s,l))
     = CurInstr(P2,Comput(P2,s,l))
     by A1,A2,Th5;
    hence LifeSpan(P1,s) <= l by A4,A6,EXTPRO_1:def 15;
  end;
  CurInstr(P2,Comput(P2,s,LifeSpan(P1,s)))
     = CurInstr(P1,Comput(P1,s,LifeSpan(P1,s))) by A1,A2,Th5
    .= halt SCMPDS by A4,EXTPRO_1:def 15;
  hence
A7:  LifeSpan(P1,s) = LifeSpan(P2,s) by A5,A3,EXTPRO_1:def 15;
   P2 halts_on s by A2,SCMPDS_4:def 7;
   then
A8: Result(P2,s) = Comput(P2,s,LifeSpan(P1,s))
     by A7,EXTPRO_1:23;
    P1 halts_on s by A1,SCMPDS_4:def 7;
    then
    Result(P1,s) = Comput(P1,s,LifeSpan(P1,s))
      by EXTPRO_1:23;
  hence thesis by A1,A2,A8,Th5;
end;

::$CT

theorem Th7:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS, J being Program of SCMPDS
   st stop I c= P
  for m st m <= LifeSpan(P,s)
   holds  Comput(P,s,m) =  Comput(P+*(I ';' J),s,m)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS, J be Program of SCMPDS;
  set SI=stop I;
  defpred X[Nat] means $1 <= LifeSpan(P,s) implies
     Comput(P,s,$1) =  Comput(P+*(I ';' J),s,$1);
  assume
A1: SI c= P;
  then
A2: P halts_on s by SCMPDS_4:def 7;
A3: for m st X[m] holds X[m+1]
  proof
    dom(I ';' J) = dom I \/ dom Shift(J, card I) by FUNCT_4:def 1;
    then
A4: dom I c= dom(I ';' J) by XBOOLE_1:7;
    let m;
    assume
A5: m <= LifeSpan(P,s) implies Comput(P,s,m) =  Comput(P+*(I ';' J),s,m);
    assume
A6: m+1 <= LifeSpan(P,s);
A7: Comput(P+*(I ';' J),s,m+1)
    = Following(P+*(I ';' J),Comput(P+*(I ';' J),s,m)) by EXTPRO_1:3;
A8: Comput(P,s,m+1) = Following(P,Comput(P,s,m)) by EXTPRO_1:3;
A9: I ';' J c= P+*(I ';' J) by FUNCT_4:25;
A10: IC Comput(P,s,m) in dom SI by A1,SCMPDS_4:def 6;
A11:  P/.IC Comput(P,s,m) = P.IC Comput(P,s,m) by PBOOLE:143;
A12: CurInstr(P,Comput(P,s,m)) = SI.IC (Comput(P,s,m))
      by A10,A11,A1,GRFUNC_1:2;
A13:  (P+*(I ';' J))/.IC Comput(P+*(I ';' J),s,m)
       = (P+*(I ';' J)).IC Comput(P+*(I ';' J),s,m) by PBOOLE:143;
    m < LifeSpan(P,s) by A6,NAT_1:13;
    then SI.IC(Comput(P,s,m)) <> halt SCMPDS by A2,A12,EXTPRO_1:def 15;
    then
A14: IC Comput(P,s,m) in dom I by A10,COMPOS_1:51;
    CurInstr(P,Comput(P,s,m))
       =I.IC (Comput(P,s,m)) by A12,A14,AFINSQ_1:def 3
      .=(I ';' J).IC(Comput(P,s,m))
              by A14,AFINSQ_1:def 3
      .= CurInstr(P+*(I ';' J),Comput(P+*(I ';' J),s,m))
       by A6,A9,A14,A4,A13,A5,GRFUNC_1:2,NAT_1:13;
    hence thesis by A5,A6,A8,A7,NAT_1:13;
  end;
A15: X[0];
  thus for m holds X[m] from NAT_1:sch 2(A15,A3);
end;

theorem Th8:
 for s being 0-started State of SCMPDS
 for I being parahalting Program of SCMPDS, J being Program of SCMPDS
   st stop I c= P
 for m st m <= LifeSpan(P,s)
 holds  Comput(P,s,m) =  Comput(P+*stop(I ';' J), s,m)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS, J be Program of SCMPDS;
  assume
A1: stop I c= P;
  set sIJ=stop (I ';' J), SS=Stop SCMPDS;
  let m;
  assume
A2: m <= LifeSpan(P,s);
  P +* sIJ = P +* (I ';' (J ';' SS)) by AFINSQ_1:27;
  hence thesis by A1,A2,Th7;
end;

Lm2: Load (DataLoc(0,0):=0) is parahalting
proof
  set ii= DataLoc(0,0):=0, m0= stop Load ii;
  let s be 0-started State of SCMPDS;
  let P such that
A1: m0 c= P;
A2: m0 = Macro ii;
  take 1;
     IC Comput(P,s,1) in NAT;
    hence IC Comput(P,s,1) in dom P by PARTFUN1:def 2;
A3: IC s = 0 by MEMSTR_0:def 11;
  then
A4: IC Exec(ii, s) = 0+1 by SCMPDS_2:45;
   1 in dom m0 by A2,COMPOS_1:57;
  then m0. 1 = P. 1 by A1,GRFUNC_1:2;
  then
A5: P. 1 = halt SCMPDS by A2,COMPOS_1:59;
   0 in dom m0 by A2,COMPOS_1:57;
  then
A6: m0. 0 = P. 0 by A1,GRFUNC_1:2;
A7: P/.IC s = P.IC s by PBOOLE:143;
  Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
    .= Following(P,s)
    .= Exec(ii,s) by A3,A6,A7,A2,COMPOS_1:58;
  hence thesis by A5,A4,PBOOLE:143;
end;

begin :: Non halting instrutions and parahalting instrutions

definition
::$CD
  let i be Instruction of SCMPDS;
  attr i is parahalting means
  :Def1:
  Load i is parahalting;
end;

registration
  cluster No-StopCode shiftable parahalting for Instruction of SCMPDS;
  existence
  proof
    take i=DataLoc(0,0):=0;
  InsCode i=2 by SCMPDS_2:14;
     then i <> halt SCMPDS;
    hence i is No-StopCode;
    thus thesis by Lm2;
  end;
end;

theorem
  goto k1 is No-StopCode
proof
A1: InsCode goto k1 = 14 by SCMPDS_2:12;
 thus goto k1 <> halt the InstructionsF of SCMPDS by A1;
end;

registration
  let a;
  cluster return a -> No-StopCode;
  coherence
  proof
    set i=return a;
    InsCode i=1 by SCMPDS_2:13;
     then i <> halt SCMPDS;
    hence thesis;
  end;
end;

registration
  let a,k1;
  cluster a := k1 -> No-StopCode;
  coherence
  proof
    set i=a:=k1;
    InsCode i=2 by SCMPDS_2:14;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster saveIC(a,k1) -> No-StopCode;
  coherence
  proof
    set i=saveIC(a,k1);
    InsCode i=3 by SCMPDS_2:15;
     then i <> halt SCMPDS;
    hence thesis;
  end;
end;

registration
  let a,k1,k2;
  cluster (a,k1)<>0_goto k2 -> No-StopCode;
  coherence
  proof
    set i=(a,k1)<>0_goto k2;
    InsCode i=4 by SCMPDS_2:16;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster (a,k1)<=0_goto k2 -> No-StopCode;
  coherence
  proof
    set i=(a,k1)<=0_goto k2;
    InsCode i=5 by SCMPDS_2:17;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster (a,k1)>=0_goto k2 -> No-StopCode;
  coherence
  proof
    set i=(a,k1)>=0_goto k2;
    InsCode i=6 by SCMPDS_2:18;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster (a,k1) := k2 -> No-StopCode;
  coherence
  proof
    set i=(a,k1) := k2;
    InsCode i=7 by SCMPDS_2:19;
     then i <> halt SCMPDS;
    hence thesis;
  end;
end;

registration
  let a,k1,k2;
  cluster AddTo(a,k1,k2) -> No-StopCode;
  coherence
  proof
    set i=AddTo(a,k1,k2);
    InsCode i=8 by SCMPDS_2:20;
     then i <> halt SCMPDS;
    hence thesis;
  end;
end;

registration
  let a,b,k1,k2;
  cluster AddTo(a,k1,b,k2) -> No-StopCode;
  coherence
  proof
    set i=AddTo(a,k1,b,k2);
    InsCode i=9 by SCMPDS_2:21;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster SubFrom(a,k1,b,k2) -> No-StopCode;
  coherence
  proof
    set i=SubFrom(a,k1,b,k2);
    InsCode i=10 by SCMPDS_2:22;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster MultBy(a,k1,b,k2) -> No-StopCode;
  coherence
  proof
    set i=MultBy(a,k1,b,k2);
    InsCode i=11 by SCMPDS_2:23;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster Divide(a,k1,b,k2) -> No-StopCode;
  coherence
  proof
    set i=Divide(a,k1,b,k2);
    InsCode i=12 by SCMPDS_2:24;
     then i <> halt SCMPDS;
    hence thesis;
  end;
  cluster (a,k1) := (b,k2) -> No-StopCode;
  coherence
  proof
    set i=(a,k1) := (b,k2);
    InsCode i=13 by SCMPDS_2:25;
     then i <> halt SCMPDS;
    hence thesis;
  end;
end;

registration
  cluster halt SCMPDS -> parahalting;
  coherence
  proof
    Stop SCMPDS=Load halt SCMPDS;
    hence thesis;
  end;
end;

registration
  let i be parahalting Instruction of SCMPDS;
  cluster Load i -> parahalting for Program of SCMPDS;
  coherence by Def1;
end;

       :: ??? is sequential
Lm3: (for s holds Exec(i,s).IC SCMPDS = IC s + 1)
  implies Load i is parahalting
proof
  assume
A1: for s holds Exec(i,s).IC SCMPDS = IC s + 1;
  set m0= stop Load i;
  let t be 0-started State of SCMPDS;
A2: m0 = Macro i;
  let Q such that
A3: m0 c= Q;
  take 1;
     IC Comput(Q,t,1) in NAT;
    hence IC Comput(Q,t,1) in dom Q by PARTFUN1:def 2;
A4: IC t =  0 by MEMSTR_0:def 11;
  then
A5: IC Exec(i, t) = 0+1 by A1;
   1 in dom m0 by A2,COMPOS_1:57;
  then m0. 1 = Q. 1 by A3,GRFUNC_1:2;
  then
A6: Q. 1 = halt SCMPDS by A2,COMPOS_1:59;
   0 in dom m0 by A2,COMPOS_1:57;
  then
A7: m0. 0 = Q. 0 by A3,GRFUNC_1:2;
A8: Q/.IC t = Q.IC t by PBOOLE:143;
  Comput(Q,t,0+1) = Following(Q,Comput(Q,t,0)) by EXTPRO_1:3
    .= Following(Q,t)
    .= Exec(i,t) by A4,A7,A8,A2,COMPOS_1:58;
  hence thesis by A5,A6,PBOOLE:143;
end;

registration
  let a,k1;
  cluster a := k1 -> parahalting;
  coherence
  proof
    set i= a:=k1;
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:45;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
end;

registration
  let a,k1,k2;
  cluster (a,k1) := k2 -> parahalting;
  coherence
  proof
    set i= (a,k1) := k2;
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:46;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
  cluster AddTo(a,k1,k2) -> parahalting;
  coherence
  proof
    set i= AddTo(a,k1,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:48;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
end;

registration
  let a,b,k1,k2;
  cluster AddTo(a,k1,b,k2) -> parahalting;
  coherence
  proof
    set i= AddTo(a,k1,b,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:49;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
  cluster SubFrom(a,k1,b,k2) -> parahalting;
  coherence
  proof
    set i= SubFrom(a,k1,b,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:50;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
  cluster MultBy(a,k1,b,k2) -> parahalting;
  coherence
  proof
    set i= MultBy(a,k1,b,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:51;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
  cluster Divide(a,k1,b,k2) -> parahalting;
  coherence
  proof
    set i= Divide(a,k1,b,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:52;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
  cluster (a,k1) := (b,k2) -> parahalting;
  coherence
  proof
    set i= (a,k1) := (b,k2);
    for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:47;
    then Load i is parahalting by Lm3;
    hence thesis;
  end;
end;

theorem Th10:
  InsCode i =1 implies i is not parahalting
proof
  consider s such that
A1: for a holds s.a = 2 by SCMPDS_2:61;
  set P = the Instruction-Sequence of SCMPDS;
  assume InsCode i=1;
  then consider a such that
A2: i = return a by SCMPDS_2:27;
  assume i is parahalting;
  then reconsider Li = Load i as parahalting Program of SCMPDS;
  set pi= Macro i;
  set s1=Initialize s, P1= P+*pi;
  s1.DataLoc(s1.a,RetIC)=s.DataLoc(s1.a,RetIC) by Th4
    .=2 by A1;
  then
A3: Exec(i, s1).IC SCMPDS =|.2.|+2 by A2,SCMPDS_2:58
    .= 2+2 by ABSVALUE:def 1
    .= 4;
  set C1=Comput(P1,s1,1);
   stop Li c= P1 by FUNCT_4:25;
   then
A4: IC C1 in dom pi by SCMPDS_4:def 6;
   0 in dom pi by COMPOS_1:57;
  then
A5: P1. 0= pi. 0 by FUNCT_4:13
    .=i by COMPOS_1:58;
A6: card pi = 2 by COMPOS_1:56;
A7: P1/.IC s1 = P1.IC s1 by PBOOLE:143;
  Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
    .= Following(P1,s1)
    .= Exec(i, s1) by A5,A7,MEMSTR_0:47;
  hence contradiction by A3,A4,A6,AFINSQ_1:66;
end;

registration
  cluster parahalting shiftable halt-free for Program of SCMPDS;
  existence
  proof
    set ii=DataLoc(0,0):=0;
    take II=Load ii;
    now
      let x be Nat;
      assume
      x in dom II;
      then x in { 0} by FUNCOP_1:13;
      then x= 0 by TARSKI:def 1;
      then
A1:   II.x=ii;
      InsCode ii=2 by SCMPDS_2:14;
      hence II.x <> halt SCMPDS by A1;
    end;
    hence thesis;
  end;
end;

registration
  let I,J be halt-free Program of SCMPDS;
  cluster I ';' J -> halt-free;
  coherence
  proof
    set IJ=I ';' J;
      set D = {n+card I where n is Nat: n in dom J };
      dom Shift(J,card I) = D by VALUED_1:def 12;
      then
A1:   dom IJ = dom I \/ D by FUNCT_4:def 1;
      let x be Nat such that
A2:   x in dom IJ;
      per cases by A2,A1,XBOOLE_0:def 3;
      suppose
A3:     x in dom I;
        then I.x=IJ.x by AFINSQ_1:def 3;
        hence IJ.x<>halt SCMPDS by A3,COMPOS_1:def 27;
      end;
      suppose
        x in D;
        then consider n being Nat such that
A4:     x = n+card I and
A5:     n in dom J;
        J. n =IJ.x by A4,A5,AFINSQ_1:def 3;
        hence IJ.x<>halt SCMPDS by A5,COMPOS_1:def 27;
      end;
    end;
end;

registration :: musi byc do najmniej jedna instrukcja rozna of halt
:: nie moze to byc np. Trivial-AMI
  let i be No-StopCode Instruction of SCMPDS;
  cluster Load i -> halt-free;
  coherence
  proof
    set p=Load i;
    now
      let x be Nat;
      assume
      x in dom p;
      then x =  0 by COMPOS_1:50;
      then p.x=i;
      hence p.x <>halt SCMPDS by COMPOS_0:def 12;
    end;
    hence thesis;
  end;
end;

registration
  let i be No-StopCode Instruction of SCMPDS, J be halt-free Program of
  SCMPDS;
  cluster i ';' J -> halt-free;
  coherence;
end;

registration
  let I be halt-free Program of SCMPDS, j be No-StopCode Instruction of
  SCMPDS;
  cluster I ';' j -> halt-free;
  coherence;
end;

registration
  let i,j be No-StopCode Instruction of SCMPDS;
  cluster i ';' j -> halt-free;
  coherence;
end;

theorem Th11:
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS st stop I c= P
   holds IC Comput(P, s,LifeSpan(P +* stop I,s)) =  card I
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS;
  set Css= Comput(P, s,LifeSpan(P,s));
  reconsider n = IC Css as Nat;
  assume
A1: stop I c= P;
  then
A2: P halts_on s by SCMPDS_4:def 7;
A3:  P +* stop I = P by A1,FUNCT_4:98;
  I c= stop I by AFINSQ_1:74;
  then
A4: I c= P by A1;
  now
    assume
A5: IC Css in dom I;
    then I.IC Css=P.IC Css by A4,GRFUNC_1:2
      .=CurInstr(P,Css) by PBOOLE:143
      .=halt SCMPDS by A2,EXTPRO_1:def 15;
    hence contradiction by A5,COMPOS_1:def 27;
  end;
  then
A6: n >= card I by AFINSQ_1:66;
A7: card stop I =card I + 1 by Lm1,AFINSQ_1:17;
  IC Css in dom stop(I) by A1,SCMPDS_4:def 6;
  then n < card I + 1 by A7,AFINSQ_1:66;
  then n <= card I by NAT_1:13;
  hence thesis by A3,A6,XXREAL_0:1;
end;

theorem Th12:
 for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS,k be Nat st
     k < LifeSpan(P +* stop I,s)
 holds IC Comput(P +* stop I,s,k) in dom I
proof let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS,k be Nat;
  set ss= s, PP = P +* stop I, m=LifeSpan(PP,ss);
  set Sk= Comput(PP, ss,k), Ik=IC Sk;
A1: stop I c= PP by FUNCT_4:25;
  then
A2: PP halts_on ss by SCMPDS_4:def 7;
  reconsider n = Ik as Nat;
A3: Ik in dom stop(I) by A1,SCMPDS_4:def 6;
A4: stop I c= PP by FUNCT_4:25;
  assume
A5: k < m;
A6: now
    assume
A7: n = card I;
A8:  0 in dom Stop SCMPDS by COMPOS_1:3;
A9: (Stop SCMPDS). 0 = halt SCMPDS;
    CurInstr(PP,Sk) =PP.Ik by PBOOLE:143
      .=(stop I).(0+n) by A3,A4,GRFUNC_1:2
      .=halt SCMPDS by A7,A9,A8,AFINSQ_1:def 3;
    hence contradiction by A5,A2,EXTPRO_1:def 15;
  end;
  card stop I=card I + 1 by Lm1,AFINSQ_1:17;
  then n < card I + 1 by A3,AFINSQ_1:66;
  then n <= card I by INT_1:7;
  then n < card I by A6,XXREAL_0:1;
  hence thesis by AFINSQ_1:66;
end;

theorem Th13:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS,k be Nat st
    I c= P & k <= LifeSpan(P +* stop I,s)
   holds Comput(P, s,k) = Comput(P +* stop I,s,k)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS,k be Nat;
  set m=LifeSpan(P +* stop I,s);
  assume that
A1: I c= P and
A2: k <= m;
  set s2 = s, P2 = P +* stop I;
  defpred P[Nat] means
    $1 <= m implies Comput(P,s,$1) = Comput(P2,s2,$1);
A3: P = P +* I by A1,FUNCT_4:98;
A4: now
    let k be Nat;
    assume
A5: P[k];
    now
A6:   Comput(P2,s2,k+1) = Following(P2,Comput(P2,s2,k)) by EXTPRO_1:3;
A7:   Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by EXTPRO_1:3;
A8:  k < k+1 by XREAL_1:29;
      assume
A9:  k+1 <= m;
      then
A10:    k < m by A8,XXREAL_0:2;
      then IC Comput(P2,s2,k) in dom I by Th12;
      then
A11:  IC Comput(P2,s2,k) in dom (stop I) by FUNCT_4:12;
A12:   IC Comput(P2,s2,k) in dom I by A10,Th12;
      CurInstr(P,Comput(P,s,k))
         = P.IC Comput(P2,s2,k) by A5,A9,A8,PBOOLE:143,XXREAL_0:2
        .= I.IC Comput(P2,s2,k) by A3,A10,Th12,FUNCT_4:13
        .= (stop I).IC Comput(P2,s2,k) by A12,AFINSQ_1:def 3
        .= (P +* stop I).IC Comput(P2,s2,k) by A11,FUNCT_4:13
        .= CurInstr(P2,Comput(P2,s2,k)) by PBOOLE:143;
      hence  Comput(P,s,k+1) =  Comput(P2,s2,k+1)
        by A5,A9,A8,A7,A6,XXREAL_0:2;
    end;
    hence P[k+1];
  end;
A13: P[0];
  for k be Nat holds P[k] from NAT_1:sch 2(A13,A4);
  hence thesis by A2;
end;

theorem Th14:
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS st I c= P
   holds IC Comput(P,s,LifeSpan(P +* stop I,s)) =  card I
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS;
  set PP = P +* stop I, m=LifeSpan(PP,s);
A1: stop I c= PP by FUNCT_4:25;
A2: stop I +* PP = PP & PP +* stop I = PP by A1,FUNCT_4:97;
  assume I c= P;
  hence IC Comput(P,s,m) = IC Comput(PP,s,m) by Th13
    .= card I by Th11,A2,FUNCT_4:25;
end;

theorem Th15:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS st I c= P
  holds CurInstr(P,Comput(P, s,LifeSpan(P +* stop I,s))) = halt SCMPDS
    or IC Comput(P, s,LifeSpan(P +* stop I,s)) = card I
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS;
  set PP = P+* stop I, m=LifeSpan(PP,s);
  set s1=Comput(P,s,m),
      s2= Comput(PP, s,LifeSpan(PP +* stop I,Initialize s)),
      Ik = IC s2;
A1: stop I c= PP by FUNCT_4:25;
   then
A2: PP halts_on s by SCMPDS_4:def 7;
  reconsider n = Ik as Nat;
A3: Ik in dom stop(I) by A1,SCMPDS_4:def 6;
A4: Initialize s = s by MEMSTR_0:44;
  card stop I = card I + 1 by Lm1,AFINSQ_1:17;
  then n < card I + 1 by A3,AFINSQ_1:66;
  then
A5: n <= card I by INT_1:7;
A6: stop I c= PP by FUNCT_4:25;
  assume
A7: I c= P;
  then
A8: IC s1 =Ik by Th13,A4;
  now
    per cases by A5,XXREAL_0:1;
    case
      n < card I;
      then
A9:    n in dom I by AFINSQ_1:66;
      thus halt SCMPDS
        = CurInstr(PP,s2) by A2,A4,EXTPRO_1:def 15
        .=PP.Ik by PBOOLE:143
        .=(stop I).Ik by A3,A6,GRFUNC_1:2
        .=I.Ik by A9,AFINSQ_1:def 3
        .=P.IC s1 by A7,A8,A9,GRFUNC_1:2
        .=CurInstr(P,s1) by PBOOLE:143;
    end;
    case n = card I;
      hence IC s1 =  card I by A7,Th13,A4;
    end;
  end;
  hence thesis;
end;

theorem Th16:
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS,k being Nat
   st I c= P & k < LifeSpan(P +* stop I,s)
  holds CurInstr(P,Comput(P,s,k)) <> halt SCMPDS
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,k be Nat;
  set PI = P +* stop I, s1= Comput(P, s,k), s2= Comput(PI, s,k);
  assume that
A1: I c= P and
A2: k < LifeSpan(PI,s);
A3: IC s2 in dom I by A2,Th12;
A4: P/.IC s1 = P.IC s1 by PBOOLE:143;
   CurInstr(P,s1)=P.IC s2 by A4,A1,A2,Th13
    .=I.IC s2 by A1,A3,GRFUNC_1:2;
  hence thesis by A3,COMPOS_1:def 27;
end;

theorem Th17:
 for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS,
      J being Program of SCMPDS, k being Nat
   st k <= LifeSpan(P +* stop I,s)
 holds Comput(P +* stop I,s,k) = Comput(P+*(I ';' J),s,k)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS,J be Program of SCMPDS,
      k be Nat;
  set spI= stop I, P1 = P +* spI, P2 = P +* (I ';' J);
  set n=LifeSpan(P1,s);
  defpred X[Nat] means
   $1 <= n implies Comput(P1,s,$1) = Comput(P2,s,$1);
A1: for n being Nat st X[n] holds X[n+1]
  proof
    let m be Nat;
    assume
A2: m <= n implies Comput(P1,s,m) =  Comput(P2,s,m);
A3: Comput(P2,s,m+1) = Following(P2,Comput(P2,s,m)) by EXTPRO_1:3;
  spI c= P1 by FUNCT_4:25;
  then
A4: IC Comput(P1,s,m) in dom spI by SCMPDS_4:def 6;
A5: Comput(P1,s,m+1) = Following(P1,Comput(P1,s,m)) by EXTPRO_1:3;
    assume
A6: m+1 <= n;
A7: m < n by A6,NAT_1:13;
    then IC Comput(P1,s,m) in dom I by Th12;
    then
A8: IC Comput(P1,s,m) in dom (I ';' J) by FUNCT_4:12;
A9: IC Comput(P1,s,m) in dom I by A7,Th12;
    CurInstr(P1,Comput(P1,s,m))
       = P1.IC Comput(P1,s,m) by PBOOLE:143
      .= spI.IC Comput(P1,s,m) by A4,FUNCT_4:13
      .= I.IC Comput(P1,s,m) by A9,AFINSQ_1:def 3
      .= (I ';' J).IC Comput(P1,s,m) by A9,AFINSQ_1:def 3
      .= P2.IC Comput(P1,s,m) by A8,FUNCT_4:13
      .=CurInstr(P2,Comput(P2,s,m)) by A6,A2,NAT_1:13,PBOOLE:143;
    hence thesis by A2,A6,A5,A3,NAT_1:13;
  end;
A10: X[0];
   for k being Nat holds X[k] from NAT_1:sch 2(A10, A1);
  hence thesis;
end;

theorem Th18:
  for s being 0-started State of SCMPDS
  for I being parahalting Program of SCMPDS,J being Program of SCMPDS,
      k being Nat st k <= LifeSpan(P +* stop I,s)
  holds  Comput(P +* stop I, s,k) =  Comput(P+*stop(I ';' J),s,k)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting Program of SCMPDS,J be Program of SCMPDS,
      k be Nat;
A1: stop (I ';' J) = (I ';' (J ';' Stop SCMPDS)) by AFINSQ_1:27;
  thus thesis by A1,Th17;
end;

registration
  let I be parahalting Program of SCMPDS,
      J be parahalting shiftable Program of SCMPDS;
  cluster I ';' J -> parahalting for Program of SCMPDS;
  coherence
  proof
    let p be Program of SCMPDS such that
A1:   p = I ';' J;
    let s be 0-started State of SCMPDS;
    let P;
    set sIJ = stop p;
    set spJ = stop J, s1 = Initialize s,
        P1 = P +* stop I,
        m1 = LifeSpan(P1,s1),
    s3 = Initialize Comput(P1, s1,m1),
    P3 = P1 +* spJ,
    m3 = LifeSpan(P3,s3),
    D = SCM-Data-Loc;
A2: spJ c= P3 by FUNCT_4:25;
    then
A3: P3 halts_on s3 by SCMPDS_4:def 7;
A4: DataPart Comput(P1,s1,m1) = DataPart s3 by MEMSTR_0:45;
A5: I c= sIJ by A1,Th1;
    set s4 = Comput(P,s,m1), P4=P;
    assume
A6: sIJ c= P;
A7: p c= sIJ by AFINSQ_1:74;
A8: s = Initialize s by MEMSTR_0:44;
    P+*(I ';' J) = P by A7,A1,A6,FUNCT_4:98,XBOOLE_1:1;
    then
A9: DataPart s4 = DataPart s3 by A4,A8,Th17;
    per cases by A6,A5,Th15,A8,XBOOLE_1:1;
    suppose
A10:  CurInstr(P,s4) = halt SCMPDS;
      take m1;
     IC Comput(P,s,m1) in NAT;
    hence IC Comput(P,s,m1) in dom P by PARTFUN1:def 2;
    thus thesis by A10;
    end;
    suppose
A11:  IC s4 =  card I;
      reconsider m = m1 + m3 as Nat;
      take m;
     IC Comput(P,s,m) in NAT;
    hence IC Comput(P,s,m) in dom P by PARTFUN1:def 2;
A12: Comput(P,s,m1+m3) = Comput(P,Comput(P,s,m1),m3) by EXTPRO_1:4;
      sIJ = I ';' (J ';' Stop SCMPDS) by A1,AFINSQ_1:27
        .= I +* Shift(spJ, card I);
      then Shift(spJ, card I) c= sIJ by FUNCT_4:25;
      then
A13:    Shift(spJ, card I) c= P4 by A6;
    CurInstr(P3,Comput(P3,s3,m3)) = CurInstr(P,Comput(P,s,m1+m3))
      by A12,A2,A9,A11,A13,SCMPDS_4:29;
     hence thesis by A3,EXTPRO_1:def 15;
    end;
  end;
end;

registration
  let i be parahalting Instruction of SCMPDS, J be parahalting shiftable
  Program of SCMPDS;
  cluster i ';' J -> parahalting;
  coherence;
end;

registration
  let I be parahalting Program of SCMPDS, j be parahalting shiftable
  Instruction of SCMPDS;
  cluster I ';' j -> parahalting;
  coherence;
end;

registration
  let i be parahalting Instruction of SCMPDS, j be parahalting shiftable
  Instruction of SCMPDS;
  cluster i ';' j -> parahalting;
  coherence;
end;

theorem Th19:
  for s being State of SCMPDS, s1 being 0-started State of SCMPDS,
      J being parahalting shiftable Program of SCMPDS
    st stop J c= P & s = Comput(P1 +* stop J, s1,m)
  holds Exec(CurInstr(P,s),IncIC(s,n)) = IncIC(Following(P,s),n)
proof
  let s be State of SCMPDS, s1 be 0-started State of SCMPDS,
      J be parahalting shiftable Program of SCMPDS;
  set pJ=stop J, s2=s1,
      P2 = P1 +* pJ;
  set i = CurInstr(P,s), ss=s +* Start-At(IC s + n,SCMPDS);
  reconsider k = IC s as Element of NAT;
  reconsider Nl=IC s + 1 as Element of NAT;
A1: IC ss + 1 = (k + n + 1) by FUNCT_4:113
    .= IC (Exec(i, s) +*Start-At (Nl + n,SCMPDS)) by FUNCT_4:113;
  assume
A2: pJ c= P;
  assume
A3:  s=Comput(P2,s2,m);
  pJ c= P2 by FUNCT_4:25;
  then
A4: IC s in dom pJ by A3,SCMPDS_4:def 6;
  reconsider n1 = IC s as Nat;
  set IEn=IC Exec(i,s)+n;
A5: IC ss = IC s + n by FUNCT_4:113;
A6: P/.IC s = P.IC s by PBOOLE:143;
A7: i=pJ.(n1) by A4,A6,A2,GRFUNC_1:2;
  then
A8: InsCode i <> 1 by A4,SCMPDS_4:def 9;
A9: i valid_at n1 by A4,A7,SCMPDS_4:def 9;
A10: InsCode i <> 3 by A4,A7,SCMPDS_4:def 9;
   InsCode i <= 14 by SCMPDS_2:6;
  then InsCode i = 0 or ... or InsCode i = 14;
  then per cases by A8,A10;
  suppose
A11:  InsCode i = 0;
A12:  Following(P,s) = s by A11,SCMPDS_2:86;
   thus Exec(CurInstr(P,s),IncIC(s,n)) = IncIC(s,n) by A11,SCMPDS_2:86
         .= IncIC(Following(P,s),n) by A12;
  end;
  suppose
    InsCode i = 14;
    then consider k1 such that
A13: i = goto k1 and
A14: n1+k1 >= 0 by A9;
A15: IC Exec(i,s) =ICplusConst(s,k1) by A13,SCMPDS_2:54;
A16: now
      let b;
      thus Exec(i, ss).b= ss.b by A13,SCMPDS_2:54
        .= s.b by SCMPDS_3:6
        .= Exec(i, s).b by A13,SCMPDS_2:54
        .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
    end;
    IC Exec(i, ss) =ICplusConst(ss,k1) by A13,SCMPDS_2:54
      .=IEn by A5,A14,A15,SCMPDS_4:27
      .= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
    hence thesis by A16,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 2;
    then consider a,k1 such that
A17: i = a := k1 by SCMPDS_2:28;
A18: now
      let b;
      per cases;
      suppose
A19:    a = b;
        hence Exec(i, ss).b = k1 by A17,SCMPDS_2:45
          .= Exec(i,s).b by A17,A19,SCMPDS_2:45
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
      suppose
A20:    a <> b;
        hence Exec(i, ss).b = ss.b by A17,SCMPDS_2:45
          .= s.b by SCMPDS_3:6
          .= Exec(i, s).b by A17,A20,SCMPDS_2:45
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A17,SCMPDS_2:45;
    then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n))
    by A1,A17,SCMPDS_2:45;
    hence thesis by A18,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 4;
    then consider a,k1,k2 such that
A21: i = (a,k1)<>0_goto k2 and
A22: n1+k2 >= 0 by A9;
A23: now
      per cases;
      suppose
A24:    s.DataLoc(s.a,k1) <> 0;
        then
A25:    IC Exec(i,s) =ICplusConst(s,k2) by A21,SCMPDS_2:55;
        ss.DataLoc(s.a,k1) <> 0 by A24,SCMPDS_3:6;
        then ss.DataLoc(ss.a,k1) <> 0 by SCMPDS_3:6;
        hence IC Exec(i, ss) =ICplusConst(ss,k2) by A21,SCMPDS_2:55
          .=IEn by A5,A22,A25,SCMPDS_4:27
          .= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
      end;
      suppose
A26:    s.DataLoc(s.a,k1) = 0;
        then ss.DataLoc(s.a,k1) = 0 by SCMPDS_3:6;
        then
A27:    ss.DataLoc(ss.a,k1) = 0 by SCMPDS_3:6;
        IC Exec(i, s) = Nl by A21,A26,SCMPDS_2:55;
        hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
        by A1,A21,A27,SCMPDS_2:55;
      end;
    end;
    now
      let b;
      thus Exec(i, ss).b= ss.b by A21,SCMPDS_2:55
        .= s.b by SCMPDS_3:6
        .= Exec(i, s).b by A21,SCMPDS_2:55
        .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
    end;
    hence thesis by A23,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 5;
    then consider a,k1,k2 such that
A28: i = (a,k1)<=0_goto k2 and
A29: n1+k2 >= 0 by A9;
A30: now
      per cases;
      suppose
A31:    s.DataLoc(s.a,k1) <= 0;
        then
A32:    IC Exec(i,s) =ICplusConst(s,k2) by A28,SCMPDS_2:56;
        ss.DataLoc(s.a,k1) <= 0 by A31,SCMPDS_3:6;
        then ss.DataLoc(ss.a,k1) <= 0 by SCMPDS_3:6;
        hence IC Exec(i, ss) =ICplusConst(ss,k2) by A28,SCMPDS_2:56
          .=IEn by A5,A29,A32,SCMPDS_4:27
          .= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
      end;
      suppose
A33:    s.DataLoc(s.a,k1) > 0;
        then ss.DataLoc(s.a,k1) > 0 by SCMPDS_3:6;
        then
A34:    ss.DataLoc(ss.a,k1) > 0 by SCMPDS_3:6;
        IC Exec(i, s) = Nl by A28,A33,SCMPDS_2:56;
        hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
        by A1,A28,A34,SCMPDS_2:56;
      end;
    end;
    now
      let b;
      thus Exec(i, ss).b= ss.b by A28,SCMPDS_2:56
        .= s.b by SCMPDS_3:6
        .= Exec(i, s).b by A28,SCMPDS_2:56
        .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
    end;
    hence thesis by A30,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 6;
    then consider a,k1,k2 such that
A35: i = (a,k1)>=0_goto k2 and
A36: n1+k2 >= 0 by A9;
A37: now
      per cases;
      suppose
A38:    s.DataLoc(s.a,k1) >= 0;
        then
A39:    IC Exec(i,s) =ICplusConst(s,k2) by A35,SCMPDS_2:57;
        ss.DataLoc(s.a,k1) >= 0 by A38,SCMPDS_3:6;
        then ss.DataLoc(ss.a,k1) >= 0 by SCMPDS_3:6;
        hence IC Exec(i, ss) =ICplusConst(ss,k2) by A35,SCMPDS_2:57
          .=IEn by A5,A36,A39,SCMPDS_4:27
          .= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
      end;
      suppose
A40:    s.DataLoc(s.a,k1) < 0;
        then ss.DataLoc(s.a,k1) < 0 by SCMPDS_3:6;
        then
A41:    ss.DataLoc(ss.a,k1) < 0 by SCMPDS_3:6;
        IC Exec(i, s) = Nl by A35,A40,SCMPDS_2:57;
        hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
        by A1,A35,A41,SCMPDS_2:57;
      end;
    end;
    now
      let b;
      thus Exec(i, ss).b= ss.b by A35,SCMPDS_2:57
        .= s.b by SCMPDS_3:6
        .= Exec(i, s).b by A35,SCMPDS_2:57
        .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
    end;
    hence thesis by A37,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 7;
    then consider a,k1,k2 such that
A42: i = (a,k1) := k2 by SCMPDS_2:33;
A43: now
      let b;
      per cases;
      suppose
A44:    DataLoc(ss.a,k1) = b;
        then
A45:    DataLoc(s.a,k1) = b by SCMPDS_3:6;
        thus Exec(i, ss).b = k2 by A42,A44,SCMPDS_2:46
          .= Exec(i,s).b by A42,A45,SCMPDS_2:46
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
      suppose
A46:    DataLoc(ss.a,k1) <> b;
        then
A47:    DataLoc(s.a,k1) <> b by SCMPDS_3:6;
        thus Exec(i, ss).b = ss.b by A42,A46,SCMPDS_2:46
          .= s.b by SCMPDS_3:6
          .= Exec(i, s).b by A42,A47,SCMPDS_2:46
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A42,SCMPDS_2:46;
    then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A42,SCMPDS_2:46;
    hence thesis by A43,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 8;
    then consider a,k1,k2 such that
A48: i = AddTo(a,k1,k2) by SCMPDS_2:34;
A49: now
      let b;
      per cases;
      suppose
A50:    DataLoc(ss.a,k1) = b;
        then
A51:    DataLoc(s.a,k1) = b by SCMPDS_3:6;
        thus Exec(i, ss).b = ss.b + k2 by A48,A50,SCMPDS_2:48
          .= s.b + k2 by SCMPDS_3:6
          .= Exec(i, s).b by A48,A51,SCMPDS_2:48
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
      suppose
A52:    DataLoc(ss.a,k1) <> b;
        then
A53:    DataLoc(s.a,k1) <> b by SCMPDS_3:6;
        thus Exec(i, ss).b = ss.b by A48,A52,SCMPDS_2:48
          .= s.b by SCMPDS_3:6
          .= Exec(i, s).b by A48,A53,SCMPDS_2:48
          .= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A48,SCMPDS_2:48;
    then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A48,SCMPDS_2:48;
    hence thesis by A49,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 9;
    then consider a,b,k1,k2 such that
A54: i = AddTo(a,k1,b,k2) by SCMPDS_2:35;
A55: now
      let c;
      per cases;
      suppose
A56:    DataLoc(ss.a,k1) = c;
        then
A57:    DataLoc(s.a,k1) = c by SCMPDS_3:6;
A58:    ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
          .=s.DataLoc(s.b,k2) by SCMPDS_3:6;
        ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
          .=s.DataLoc(s.a,k1) by SCMPDS_3:6;
        hence
        Exec(i, ss).c = s.DataLoc(s.a,k1) + s.DataLoc(s.b,k2) by A54,A56,A58,
SCMPDS_2:49
          .= Exec(i, s).c by A54,A57,SCMPDS_2:49
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
      suppose
A59:    DataLoc(ss.a,k1) <> c;
        then
A60:    DataLoc(s.a,k1) <> c by SCMPDS_3:6;
        thus Exec(i, ss).c = ss.c by A54,A59,SCMPDS_2:49
          .= s.c by SCMPDS_3:6
          .= Exec(i, s).c by A54,A60,SCMPDS_2:49
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A54,SCMPDS_2:49;
    then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A54,SCMPDS_2:49;
    hence thesis by A55,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 10;
    then consider a,b,k1,k2 such that
A61: i = SubFrom(a,k1,b,k2) by SCMPDS_2:36;
A62: now
      let c;
      per cases;
      suppose
A63:    DataLoc(ss.a,k1) = c;
        then
A64:    DataLoc(s.a,k1) = c by SCMPDS_3:6;
A65:    ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
          .=s.DataLoc(s.b,k2) by SCMPDS_3:6;
        ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
          .=s.DataLoc(s.a,k1) by SCMPDS_3:6;
        hence
        Exec(i, ss).c = s.DataLoc(s.a,k1) - s.DataLoc(s.b,k2) by A61,A63,A65,
SCMPDS_2:50
          .= Exec(i, s).c by A61,A64,SCMPDS_2:50
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
      suppose
A66:    DataLoc(ss.a,k1) <> c;
        then
A67:    DataLoc(s.a,k1) <> c by SCMPDS_3:6;
        thus Exec(i, ss).c = ss.c by A61,A66,SCMPDS_2:50
          .= s.c by SCMPDS_3:6
          .= Exec(i, s).c by A61,A67,SCMPDS_2:50
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A61,SCMPDS_2:50;
    then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A61,SCMPDS_2:50;
    hence thesis by A62,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 11;
    then consider a,b,k1,k2 such that
A68: i = MultBy(a,k1,b,k2) by SCMPDS_2:37;
A69: now
      let c;
      per cases;
      suppose
A70:    DataLoc(ss.a,k1) = c;
        then
A71:    DataLoc(s.a,k1) = c by SCMPDS_3:6;
A72:    ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
          .=s.DataLoc(s.b,k2) by SCMPDS_3:6;
        ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
          .=s.DataLoc(s.a,k1) by SCMPDS_3:6;
        hence Exec(i, ss).c = s.DataLoc(s.a,k1) * s.DataLoc(s.b,k2) by A68,A70
,A72,SCMPDS_2:51
          .= Exec(i, s).c by A68,A71,SCMPDS_2:51
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
      suppose
A73:    DataLoc(ss.a,k1) <> c;
        then
A74:    DataLoc(s.a,k1) <> c by SCMPDS_3:6;
        thus Exec(i, ss).c = ss.c by A68,A73,SCMPDS_2:51
          .= s.c by SCMPDS_3:6
          .= Exec(i, s).c by A68,A74,SCMPDS_2:51
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A68,SCMPDS_2:51;
    then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A68,SCMPDS_2:51;
    hence thesis by A69,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 12;
    then consider a,b,k1,k2 such that
A75: i = Divide(a,k1,b,k2) by SCMPDS_2:38;
A76: now
      let c;
A77:  ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
        .=s.DataLoc(s.a,k1) by SCMPDS_3:6;
A78:  ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
        .=s.DataLoc(s.b,k2) by SCMPDS_3:6;
      per cases;
      suppose
A79:    DataLoc(ss.b,k2) = c;
        then
A80:    DataLoc(s.b,k2) = c by SCMPDS_3:6;
        thus Exec(i, ss).c = s.DataLoc(s.a,k1) mod s.DataLoc(s.b,k2) by A75,A77
,A78,A79,SCMPDS_2:52
          .= Exec(i, s).c by A75,A80,SCMPDS_2:52
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
      suppose
A81:    DataLoc(ss.b,k2) <> c;
        then
A82:    DataLoc(s.b,k2) <> c by SCMPDS_3:6;
        hereby
          per cases;
          suppose
A83:        DataLoc(ss.a,k1) <> c;
            then
A84:        DataLoc(s.a,k1) <> c by SCMPDS_3:6;
            thus Exec(i, ss).c = ss.c by A75,A81,A83,SCMPDS_2:52
              .=s.c by SCMPDS_3:6
              .=Exec(i,s).c by A75,A82,A84,SCMPDS_2:52
              .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
          end;
          suppose
A85:        DataLoc(ss.a,k1) = c;
            then
A86:        DataLoc(s.a,k1) = c by SCMPDS_3:6;
            thus Exec(i, ss).c = s.DataLoc(s.a,k1) div s.DataLoc(s.b,k2) by A75
,A77,A78,A81,A85,SCMPDS_2:52
              .= Exec(i,s).c by A75,A82,A86,SCMPDS_2:52
              .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
          end;
        end;
      end;
    end;
    IC Exec(i, s) = Nl by A75,SCMPDS_2:52;
    then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A75,SCMPDS_2:52;
    hence thesis by A76,SCMPDS_2:44;
  end;
  suppose
    InsCode i = 13;
    then consider a,b,k1,k2 such that
A87: i = (a,k1):=(b,k2) by SCMPDS_2:39;
A88: now
      let c;
      per cases;
      suppose
A89:    DataLoc(ss.a,k1) = c;
        then
A90:    DataLoc(s.a,k1) = c by SCMPDS_3:6;
        thus Exec(i, ss).c = ss.DataLoc(ss.b,k2) by A87,A89,SCMPDS_2:47
          .=s.DataLoc(ss.b,k2) by SCMPDS_3:6
          .=s.DataLoc(s.b,k2) by SCMPDS_3:6
          .=Exec(i,s).c by A87,A90,SCMPDS_2:47
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
      suppose
A91:    DataLoc(ss.a,k1) <> c;
        then
A92:    DataLoc(s.a,k1) <> c by SCMPDS_3:6;
        thus Exec(i,ss).c = ss.c by A87,A91,SCMPDS_2:47
          .=s.c by SCMPDS_3:6
          .=Exec(i,s).c by A87,A92,SCMPDS_2:47
          .= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
      end;
    end;
    IC Exec(i, s) = Nl by A87,SCMPDS_2:47;
    then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A87,SCMPDS_2:47;
    hence thesis by A88,SCMPDS_2:44;
  end;
end;

begin :: Computation of two consecutive program blocks

theorem
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS,J being
  parahalting shiftable Program of SCMPDS,k being Nat st
  stop (I ';' J) c= P holds
   IncIC(Comput(P +* stop I +* stop J,
     Initialize Result(P +* stop I,s),k),card I)
  =  Comput(P+*stop(I ';' J),s,LifeSpan(P +* stop I,s)+k)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,J be parahalting
  shiftable Program of SCMPDS,k be Nat;
  set sIsI = s, PIPI = P +* stop I,
      RI = Result(PIPI,sIsI), pJ= stop J,
   RIJ = Initialize RI, PRIJ = PIPI +* pJ,
   pIJ = stop (I ';' J),
   sIsIJ = s, PIPIJ = P +* pIJ;
A1:  pJ c= PRIJ by FUNCT_4:25;
   stop I c= PIPI by FUNCT_4:25;
   then
A2: PIPI halts_on sIsI by SCMPDS_4:def 7;
  set s2 = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+0);
  set s1 = RIJ +* Start-At (IC RIJ + card I,SCMPDS);
  set m1 = LifeSpan(PIPI,sIsI);
A3: I c= pIJ by Th1;
  assume
A4: pIJ c= P;
A5: P +* pIJ = P by A4,FUNCT_4:98;
A6: now
    thus IC s1 = IC RIJ + card I by FUNCT_4:113
      .=  (0+card I) by FUNCT_4:113
      .= IC s2 by A4,A3,Th14,A5,XBOOLE_1:1;

    hereby
      let a be Int_position;
A7: not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
   not a in dom Start-At (IC RIJ + card I,SCMPDS) by SCMPDS_4:18;
      hence s1.a = RIJ.a by FUNCT_4:11
        .= RI.a by A7,FUNCT_4:11
        .= Comput(PIPI, sIsI,m1).a by A2,EXTPRO_1:23
        .= s2.a by Th18;
    end;
  end;
  defpred X[Nat] means
    IncIC(Comput(PRIJ, RIJ,$1), card I)
     = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+$1);
A8: pIJ c= PIPIJ by FUNCT_4:25;
A9: for k being Nat st X[k] holds X[k+1]
  proof
    let k be Nat;
    set k1 = k+1, CRk = Comput(PRIJ, RIJ,k),
       PCRk = PRIJ,
       CRSk = IncIC(CRk,card I),
    CIJk = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+k),
    PCIJk = PIPIJ,
CRk1 = Comput(PRIJ, RIJ,k1
    ), CRSk1 = CRk1 +* Start-At (IC CRk1 + card I,SCMPDS),
    CIJk1 = Comput(PIPIJ, sIsIJ,
    LifeSpan(PIPI,sIsI)+k1);
    assume
A10:  CRSk =  CIJk;
A11: CurInstr(PCRk,CRk) = CurInstr(PCIJk,CIJk)
    proof
A12:  CurInstr(PCIJk,CIJk) = PCIJk.IC CRSk by A10,PBOOLE:143
        .= PCIJk.(IC CRk + card I) by FUNCT_4:113;
      reconsider n = IC CRk as Nat;
A13:  pIJ = I ';' pJ by AFINSQ_1:27;
A14:  IC CRk in dom pJ by A1,SCMPDS_4:def 6;
      then n < card pJ by AFINSQ_1:66;
      then n+card I < card pJ + card I by XREAL_1:6;
      then n+card I < card pIJ by A13,AFINSQ_1:17;
      then
A15:  IC CRk + card I in dom pIJ by AFINSQ_1:66;
A16:  PCRk/.IC CRk = PCRk.IC CRk by PBOOLE:143;
      pJ c= PCRk by FUNCT_4:25;
      hence CurInstr(PCRk,CRk) =pJ.IC CRk by A14,A16,GRFUNC_1:2
        .=pIJ.(IC CRk + card I) by A14,A13,AFINSQ_1:def 3
        .= CurInstr(PCIJk,CIJk) by A12,A8,A15,GRFUNC_1:2;
    end;
A17:  Exec(CurInstr(PCIJk,CIJk), CIJk)
   =  IncIC(Following(PCRk,CRk), card I) by A10,Th19,A11,FUNCT_4:25;
    CIJk1 = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+k+1);
    then
A18: CIJk1 = Following(PIPIJ,CIJk) by EXTPRO_1:3;
A19: now
      let a be Int_position;
      thus CRSk1.a = CRk1.a by SCMPDS_3:6
        .= (Following(PRIJ,CRk)).a by EXTPRO_1:3
        .= CIJk1.a by A18,A17,SCMPDS_3:6;
    end;
    IC CRSk1 = IC CRk1 + card I by FUNCT_4:113
      .= IC Following(PRIJ,CRk) + card I by EXTPRO_1:3;
    then
    IC CRSk1 = IC CIJk1 by A18,A17,FUNCT_4:113;
    hence thesis by A19,SCMPDS_4:2;
  end;
A20: X[0] by A6,SCMPDS_4:2;
  for k being Nat holds X[k] from NAT_1:sch 2(A20,A9);
  hence thesis;
end;

Lm4:
 for I being parahalting halt-free Program of SCMPDS,
     J being parahalting shiftable Program of SCMPDS,
  s being 0-started State of SCMPDS st stop (I ';' J) c= P & P1= P +* stop I
   holds IC Comput(P, s,LifeSpan(P1,s)) = card I &
  DataPart Comput(P, s,LifeSpan(P1,s)) =
   DataPart (Initialize Comput(P1,s,LifeSpan(P1,s))) &
   Shift(stop J,card I) c= P &
   LifeSpan(P,s) = LifeSpan(P1,s)
    + LifeSpan(P1 +* stop J,Initialize Result(P1,s))
proof
  set D = SCM-Data-Loc;
  let I be parahalting halt-free Program of SCMPDS,J be parahalting
  shiftable Program of SCMPDS,s be 0-started State of SCMPDS;
  set spJ = stop J,
  sIJ = stop (I ';' J), m1 = LifeSpan(P1,s),
  s3 = Initialize Comput(P1, s, m1),
  P3 = P1 +* spJ;
  set m3 = LifeSpan(P3,s3);
  assume that
A1: sIJ c= P and
A2: P1= P +* stop I;
  set s4 = Comput(P,s,m1), P4 = P;
A3: I c= sIJ by Th1;
  hence
A4: IC s4 =  card I by A1,A2,Th14,XBOOLE_1:1;
  reconsider m = m1 + m3 as Nat;
  sIJ = I ';' (J ';' Stop SCMPDS) by AFINSQ_1:27
    .= I +* Shift(spJ, card I);
  then
A5: Shift(spJ, card I) c= sIJ by FUNCT_4:25;
A6: spJ c= P3 by FUNCT_4:25;
    then
A7: P3 halts_on s3 by SCMPDS_4:def 7;
A8: DataPart Comput(P1, s,m1) = DataPart s3 by MEMSTR_0:45;
  I ';' J c= stop (I ';' J) by AFINSQ_1:74;
  then P+*(I ';' J) = P by A1,FUNCT_4:98,XBOOLE_1:1;
  hence
A9: DataPart s4 = DataPart s3 by A8,A2,Th17;
A10: Comput(P,s,m1+m3) = Comput(P,Comput(P,s,m1),m3) by EXTPRO_1:4;
  thus
A11: Shift(spJ, card I) c= P4 by A5,A1;
  then CurInstr(P3,Comput(P3,s3,m3)) = CurInstr(P,Comput(P,s,m1+m3))
      by A10,A6,A4,A9,SCMPDS_4:29;
  then
A12: CurInstr(P,Comput(P,s,m)) = halt SCMPDS by A7,EXTPRO_1:def 15;
A13: now
    let k be Nat;
    assume
    m1 + k < m;
    then
A14: k < m3 by XREAL_1:6;
    assume
A15: CurInstr(P,Comput(P,s,m1+k)) = halt SCMPDS;
A16: Comput(P,s,m1+k) =
Comput(P,Comput(P,s,m1),k) by EXTPRO_1:4;
    CurInstr(P3,Comput(P3,s3,k))
     = halt SCMPDS by A15,A16,A6,A4,A9,A11,SCMPDS_4:29;
    hence contradiction by A7,A14,EXTPRO_1:def 15;
  end;
  now
    let k be Nat;
    assume
A17: k < m;
    per cases;
    suppose k < m1;
      hence CurInstr(P,Comput(P,s,k)) <> halt SCMPDS
            by A2,Th16,A1,A3,XBOOLE_1:1;
    end;
    suppose
      m1 <= k;
      then consider kk being Nat such that
A18:  m1 + kk = k by NAT_1:10;
      thus CurInstr(P,Comput(P,s,k)) <> halt SCMPDS by A13,A17,A18;
    end;
  end;
  then
A19: for k being Nat st CurInstr(P,Comput(P,s,k)) = halt SCMPDS
        holds m <= k;
 stop I c= P1 by A2,FUNCT_4:25;
 then P1 halts_on s by SCMPDS_4:def 7;
  then
A20: Result(P1,s) = Comput(P1,s,LifeSpan(P1,s)) by EXTPRO_1:23;
  P halts_on s by A1,SCMPDS_4:def 7;
  hence thesis by A20,A12,A19,EXTPRO_1:def 15;
end;

theorem Th21:
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS,
      J being parahalting shiftable Program of SCMPDS holds
  LifeSpan(P+*stop(I ';' J), s)
   = LifeSpan(P +* stop I,s) +
     LifeSpan(P +* stop I +* stop J,Initialize Result(P +* stop I,s))
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,J be parahalting
  shiftable Program of SCMPDS;
  set sI=stop I, sIJ = stop (I ';' J),
  s1= s, s2= s,
  P1 = P +* sIJ, P2 = P +* stop I;
A1: sIJ c= P1 by FUNCT_4:25;
  set
  s3=Initialize Result(P1 +* stop I,s1),
  P3 = P1 +* stop I +* stop J,
  s4=Initialize Result(P2,s2),
  P4 = P2 +* stop J;
A2: stop I c= P2 by FUNCT_4:25;
A3: stop J c= P4 by FUNCT_4:25;
A4: stop J c= P3 by FUNCT_4:25;
A5: stop I c= P1 +* stop I by FUNCT_4:25;
  then s4 =  s3 by A2,Th6;
  then
A6: LifeSpan(P3,s3) = LifeSpan(P4,s4) by A4,A3,Th6;
  LifeSpan(P1 +* stop I,s1) =
  LifeSpan(P2,s2) by A5,A2,Th6;
  hence thesis by A1,A6,Lm4;
end;

theorem Th22:
  for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s)
 = IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,J be parahalting
  shiftable Program of SCMPDS;
  set A = NAT, D = SCM-Data-Loc, sI = stop I,
   sIJ = stop (I ';' J), P1 = P +* stop I,
   m1 = LifeSpan(P1,s), P2 = P +* stop(I ';' J),
   s3 = Initialize Comput(P1,s,m1), P3 = P1 +* stop J,
   m3 = LifeSpan(P3,s3);
A1: stop J c= P3 by FUNCT_4:25;
  then
A2: P3 halts_on s3 by SCMPDS_4:def 7;
A3: stop J c= P +* stop J by FUNCT_4:25;
A4: stop I c= P1 by FUNCT_4:25;
  then
  P1 halts_on s by SCMPDS_4:def 7;
  then
A5: Initialize Comput(P1,s,m1)
      = Initialize IExec(I,P,s) by EXTPRO_1:23;
A6:  Result(P +* stop J,Initialize IExec(I,P,s))
   =  Result(P3,s3) by A1,A3,Th6,A5;
A7: stop I c= P2 +* stop I by FUNCT_4:25;
A8: P2 +* stop I +* sIJ = P2 +* (stop I +* sIJ) by FUNCT_4:14
      .= P2 +* sIJ by Th3;
A9: LifeSpan(P2 +* stop I,s) = m1 by A4,A7,Th6;
 set S1=s,
     E1 = P2 +* stop I;
A10:  Comput(P1,s,m1)
  =  Comput(P1 +* stop(I ';' J), s,m1) by Th8,FUNCT_4:25;
A11:  P +* stop I +* sIJ =  P +* (stop I +* sIJ) by FUNCT_4:14
        .= P +* (sIJ +* sIJ) by Th3
        .= P2 +* stop I +* sIJ by A8;
A12: DataPart(Comput(P2 +* stop I,s,m1))
      = DataPart Comput(P1, s,m1) by A11,A10,A9,Th8,FUNCT_4:25;
A13: sIJ c= P2 by FUNCT_4:25;
  then
A14: DataPart Comput(P2,s,m1)
     = DataPart(Initialize Comput(P2 +* stop I,s,m1)) by A9,Lm4
    .= DataPart(Comput(P2 +* stop I, s,m1)) by MEMSTR_0:45;
A15: Shift(stop J,card I) c= P2 by A13,A7,Lm4;
A16: IC Comput(P2,s,m1) =  card I by A13,A9,Lm4;
A17: DataPart Initialize Comput(P1,s,m1)
     = DataPart Comput(P2,s,m1) by A12,A14,MEMSTR_0:45;
  then
A18: IC Comput(P2, Comput(P2,s,m1),m3) = IC Comput(P3,s3,m3) + card I
        by A15,A1,A16,SCMPDS_4:29;
A19: DataPart Comput(P2, Comput(P2,s,m1),m3) = DataPart Comput(P3,s3,m3)
   by A16,A15,A1,A17,SCMPDS_4:29;
A20: P1 halts_on s by A4,SCMPDS_4:def 7;
   then
A21: s3 = Initialize Result(P1,s) by EXTPRO_1:23;
 set SS1 = Initialize Result(P1,s) +* stop J,
     SS2 = Initialize IExec(I,P,s) +* stop J;
A22: IC Result(P1 +* stop J,Initialize Result(P1,s))
= IC Result(P +* stop J,Initialize IExec(I,P,s)) by Th6,A1,A3;
A23: P2 halts_on s
     by A13,SCMPDS_4:def 7;
A24: IC IExec(I ';' J,P,s)
     = IC Comput(P2,s,LifeSpan(P2,s)) by A23,EXTPRO_1:23
    .= IC Comput(P2,s,m1+m3) by A21,Th21
    .= IC Comput(P3,s3,m3) + card I by A18,EXTPRO_1:4
    .= IC Result(P3,s3) + card I by A2,EXTPRO_1:23
    .= IC IExec(J,P,Initialize IExec(I,P,s)) + card I
          by A22,A20,EXTPRO_1:23;
  IExec(I ';' J,P,s) = Comput(P2,s,LifeSpan(P2,s))
    by A23,EXTPRO_1:23
    .= Comput(P2,s,m1+m3) by A21,Th21;
  then
A25: DataPart IExec(I ';' J,P,s)
     = DataPart Comput(P3,s3,m3) by A19,EXTPRO_1:4
    .= DataPart IExec(J,P,Initialize IExec(I,P,s))
      by A6,A2,EXTPRO_1:23;
  hereby
    reconsider l = IC IExec(J,P,Initialize IExec(I,P,s)) + card I
     as Nat;
A26: dom Start-At(l,SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
A27: now
      let x be object;
      assume
A28:  x in dom IExec(I ';' J,P,s);
      per cases by A28,SCMPDS_4:6;
      suppose
A29:    x is Int_position;
        then x <> IC SCMPDS by SCMPDS_2:43;
        then
A30:    not x in dom Start-At(l,SCMPDS) by A26,TARSKI:def 1;
        IExec(I ';' J,P,s).x
         = IExec(J,P,Initialize IExec(I,P,s)).x
        by A25,A29,SCMPDS_4:8;
        hence
        IExec(I ';' J,P,s).x
         = (IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)).x
           by A30,FUNCT_4:11;
      end;
      suppose
A31:    x = IC SCMPDS;
        then x in {IC SCMPDS} by TARSKI:def 1;
        then
A32:    x in dom Start-At(l,SCMPDS) by FUNCOP_1:13;
        thus IExec(I ';' J,P,s).x = (Start-At(l,SCMPDS)).IC SCMPDS
        by A24,A31,FUNCOP_1:72
          .= (IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)).x
           by A31,A32,FUNCT_4:13;
      end;
    end;
    dom IExec(I ';' J,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
      .= dom IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
                by PARTFUN1:def 2;
    hence thesis by A27,FUNCT_1:2;
  end;
end;

theorem
 for s being 0-started State of SCMPDS
 for I being parahalting halt-free Program of SCMPDS,J being
  parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s).a
   = IExec(J,P,Initialize IExec(I,P,s)).a
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,J be parahalting
  shiftable Program of SCMPDS;
A1: not a in
 dom Start-At(IC IExec(J,P,Initialize IExec(I,P,s)) + card I,SCMPDS)
by SCMPDS_4:18;
  IExec(I ';' J,P,s) = IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
   by Th22;
  hence thesis by A1,FUNCT_4:11;
end;

begin :: Computation of the program consisting of a instruction and a block

::$CT

theorem
 s1 | (SCM-Data-Loc \/ {IC SCMPDS})
  = s2 | (SCM-Data-Loc \/ {IC SCMPDS}) implies s1 =  s2
proof
  set Y = NAT;
  set X = SCM-Data-Loc \/ {IC SCMPDS};
A1:  s1 = s1|(Data-Locations SCMPDS \/ {IC SCMPDS})
   &  s2 = s2|(Data-Locations SCMPDS \/ {IC SCMPDS}) by MEMSTR_0:33;
  thus thesis by A1,SCMPDS_2:84;
end;

theorem Th25:
  DataPart s1 = DataPart s2 & InsCode i <> 3 implies
   DataPart Exec(i,s1) = DataPart Exec(i,s2)
proof
  assume that
A1: DataPart s1 = DataPart s2 and
A2: InsCode i <> 3;
  InsCode i = 0 or ... or InsCode i = 14 by SCMPDS_2:6;
  then per cases by A2;
  suppose InsCode i = 0;
   then Exec(i,s1) = s1 & Exec(i,s2) = s2 by SCMPDS_2:86;
   hence thesis by A1;
  end;
  suppose
    InsCode i = 14;
    then
A3: ex k1 st i = goto k1 by SCMPDS_2:26;
    now
      let a;
      thus Exec(i, s1).a = s1.a by A3,SCMPDS_2:54
        .=s2.a by A1,SCMPDS_4:8
        .=Exec(i, s2).a by A3,SCMPDS_2:54;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 1;
    then consider a such that
A4: i = return a by SCMPDS_2:27;
    now
      let b;
      per cases;
      suppose
A5:     a=b;
        hence Exec(i, s1).b= s1.DataLoc(s1.a,RetSP) by A4,SCMPDS_2:58
          .=s2.DataLoc(s2.a,RetSP) by A1,SCMPDS_3:2
          .=Exec(i,s2).b by A4,A5,SCMPDS_2:58;
      end;
      suppose
A6:     a<>b;
        hence Exec(i, s1).b = s1.b by A4,SCMPDS_2:58
          .=s2.b by A1,SCMPDS_4:8
          .=Exec(i,s2).b by A4,A6,SCMPDS_2:58;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 2;
    then consider a,k1 such that
A7: i = a := k1 by SCMPDS_2:28;
    now
      let b;
      per cases;
      suppose
A8:     a=b;
        hence Exec(i, s1).b= k1 by A7,SCMPDS_2:45
          .=Exec(i,s2).b by A7,A8,SCMPDS_2:45;
      end;
      suppose
A9:     a<>b;
        hence Exec(i,s1).b = s1.b by A7,SCMPDS_2:45
          .=s2.b by A1,SCMPDS_4:8
          .=Exec(i,s2).b by A7,A9,SCMPDS_2:45;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 4;
    then
A10: ex a,k1,k2 st i = (a,k1)<>0_goto k2 by SCMPDS_2:30;
    now
      let a;
      thus Exec(i, s1).a = s1.a by A10,SCMPDS_2:55
        .=s2.a by A1,SCMPDS_4:8
        .=Exec(i, s2).a by A10,SCMPDS_2:55;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 5;
    then
A11: ex a,k1,k2 st i = (a,k1)<=0_goto k2 by SCMPDS_2:31;
    now
      let a;
      thus Exec(i, s1).a = s1.a by A11,SCMPDS_2:56
        .=s2.a by A1,SCMPDS_4:8
        .=Exec(i, s2).a by A11,SCMPDS_2:56;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 6;
    then
A12: ex a,k1,k2 st i = (a,k1)>=0_goto k2 by SCMPDS_2:32;
    now
      let a;
      thus Exec(i, s1).a = s1.a by A12,SCMPDS_2:57
        .=s2.a by A1,SCMPDS_4:8
        .=Exec(i, s2).a by A12,SCMPDS_2:57;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 7;
    then consider a,k1,k2 such that
A13: i = (a,k1) := k2 by SCMPDS_2:33;
    now
      let b;
      per cases;
      suppose
A14:    DataLoc(s1.a,k1)=b;
        then
A15:    DataLoc(s2.a,k1)=b by A1,SCMPDS_4:8;
        thus Exec(i, s1).b= k2 by A13,A14,SCMPDS_2:46
          .=Exec(i,s2).b by A13,A15,SCMPDS_2:46;
      end;
      suppose
A16:    DataLoc(s1.a,k1)<>b;
        then
A17:    DataLoc(s2.a,k1)<>b by A1,SCMPDS_4:8;
        thus Exec(i,s1).b = s1.b by A13,A16,SCMPDS_2:46
          .=s2.b by A1,SCMPDS_4:8
          .=Exec(i,s2).b by A13,A17,SCMPDS_2:46;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 8;
    then consider a,k1,k2 such that
A18: i = AddTo(a,k1,k2) by SCMPDS_2:34;
    now
      let b;
      per cases;
      suppose
A19:    DataLoc(s1.a,k1)=b;
        then
A20:    DataLoc(s2.a,k1)=b by A1,SCMPDS_4:8;
        thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A18,A19,SCMPDS_2:48
          .= s2.DataLoc(s2.a,k1)+k2 by A1,SCMPDS_3:2
          .=Exec(i,s2).b by A18,A20,SCMPDS_2:48;
      end;
      suppose
A21:    DataLoc(s1.a,k1)<>b;
        then
A22:    DataLoc(s2.a,k1)<>b by A1,SCMPDS_4:8;
        thus Exec(i,s1).b = s1.b by A18,A21,SCMPDS_2:48
          .=s2.b by A1,SCMPDS_4:8
          .=Exec(i,s2).b by A18,A22,SCMPDS_2:48;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 9;
    then consider a,b,k1,k2 such that
A23: i = AddTo(a,k1,b,k2) by SCMPDS_2:35;
    now
      let c;
      per cases;
      suppose
A24:    DataLoc(s1.a,k1)=c;
        then
A25:    DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
        thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2) by A23,A24
,SCMPDS_2:49
          .= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
          .= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
          .=Exec(i,s2).c by A23,A25,SCMPDS_2:49;
      end;
      suppose
A26:    DataLoc(s1.a,k1)<>c;
        then
A27:    DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
        thus Exec(i,s1).c = s1.c by A23,A26,SCMPDS_2:49
          .=s2.c by A1,SCMPDS_4:8
          .=Exec(i,s2).c by A23,A27,SCMPDS_2:49;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 10;
    then consider a,b,k1,k2 such that
A28: i = SubFrom(a,k1,b,k2) by SCMPDS_2:36;
    now
      let c;
      per cases;
      suppose
A29:    DataLoc(s1.a,k1)=c;
        then
A30:    DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
        thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
         by A28,A29,SCMPDS_2:50
          .= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
          .= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
          .=Exec(i,s2).c by A28,A30,SCMPDS_2:50;
      end;
      suppose
A31:    DataLoc(s1.a,k1)<>c;
        then
A32:    DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
        thus Exec(i,s1).c = s1.c by A28,A31,SCMPDS_2:50
          .=s2.c by A1,SCMPDS_4:8
          .=Exec(i,s2).c by A28,A32,SCMPDS_2:50;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 11;
    then consider a,b,k1,k2 such that
A33: i = MultBy(a,k1,b,k2) by SCMPDS_2:37;
    now
      let c;
      per cases;
      suppose
A34:    DataLoc(s1.a,k1)=c;
        then
A35:    DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
        thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2) by A33,A34
,SCMPDS_2:51
          .= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
          .= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
          .=Exec(i,s2).c by A33,A35,SCMPDS_2:51;
      end;
      suppose
A36:    DataLoc(s1.a,k1)<>c;
        then
A37:    DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
        thus Exec(i,s1).c = s1.c by A33,A36,SCMPDS_2:51
          .=s2.c by A1,SCMPDS_4:8
          .=Exec(i,s2).c by A33,A37,SCMPDS_2:51;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 12;
    then consider a,b,k1,k2 such that
A38: i = Divide(a,k1,b,k2) by SCMPDS_2:38;
    now
      let c;
      per cases;
      suppose
A39:    DataLoc(s1.b,k2)=c;
        then
A40:    DataLoc(s2.b,k2)=c by A1,SCMPDS_4:8;
        thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2) by A38
,A39,SCMPDS_2:52
          .= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
          .= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
          .= Exec(i,s2).c by A38,A40,SCMPDS_2:52;
      end;
      suppose
A41:    DataLoc(s1.b,k2)<>c;
        then
A42:    DataLoc(s2.b,k2)<>c by A1,SCMPDS_4:8;
        hereby
          per cases;
          suppose
A43:        DataLoc(s1.a,k1)<>c;
            then
A44:        DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
            thus Exec(i, s1).c = s1.c by A38,A41,A43,SCMPDS_2:52
              .=s2.c by A1,SCMPDS_4:8
              .=Exec(i,s2).c by A38,A42,A44,SCMPDS_2:52;
          end;
          suppose
A45:        DataLoc(s1.a,k1)=c;
            then
A46:        DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
            thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
            by A38,A41,A45,SCMPDS_2:52
              .= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
              .= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
              .= Exec(i,s2).c by A38,A42,A46,SCMPDS_2:52;
          end;
        end;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
  suppose
    InsCode i = 13;
    then consider a,b,k1,k2 such that
A47: i = (a,k1):=(b,k2) by SCMPDS_2:39;
    now
      let c;
      per cases;
      suppose
A48:    DataLoc(s1.a,k1)=c;
        then
A49:    DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
        thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A47,A48,SCMPDS_2:47
          .= s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
          .=Exec(i,s2).c by A47,A49,SCMPDS_2:47;
      end;
      suppose
A50:    DataLoc(s1.a,k1)<>c;
        then
A51:    DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
        thus Exec(i,s1).c = s1.c by A47,A50,SCMPDS_2:47
          .=s2.c by A1,SCMPDS_4:8
          .=Exec(i,s2).c by A47,A51,SCMPDS_2:47;
      end;
    end;
    hence thesis by SCMPDS_4:8;
  end;
end;

theorem Th26:
  for i being shiftable Instruction of SCMPDS holds (DataPart s1 =
  DataPart s2 implies DataPart Exec(i,s1) = DataPart Exec(i,s2))
proof
  let i be shiftable Instruction of SCMPDS;
  InsCode i <> 3 by SCMPDS_4:def 10;
  hence thesis by Th25;
end;

theorem Th27:
 for s being 0-started State of SCMPDS
  for i being parahalting Instruction of SCMPDS
   holds Exec(i,s) = IExec(Load i,P,s)
proof
  let s be 0-started State of SCMPDS;
  let i be parahalting Instruction of SCMPDS;
  set Li=Load i, Mi= Macro i;
  set PI = P +* Mi;
  set IC1 = IC Comput(PI, s,1);
A1: Initialize s = s by MEMSTR_0:44;
  Mi c= PI by FUNCT_4:25;
  then
A2: PI halts_on s by SCMPDS_4:def 7;
A3:  1 in dom Mi by COMPOS_1:57;
A4:  0 in dom Mi by COMPOS_1:57;
A5: Mi. 1=halt SCMPDS by COMPOS_1:59;
A6: Mi. 0 = i by COMPOS_1:58;
A7: Mi c= PI by FUNCT_4:25;
     then
A8: IC1 in dom Mi by SCMPDS_4:def 6;
A9: PI/.IC s = PI.IC s by PBOOLE:143;
A10: Comput(PI, s,0+1) = Following(PI,Comput(PI,s,0)) by EXTPRO_1:3
    .= Following(PI,s)
    .= Exec(PI. 0, s) by A9,A1,MEMSTR_0:47
    .= Exec(i, s) by A4,A6,A7,GRFUNC_1:2;
  per cases by A8,COMPOS_1:60;
  suppose
A11: IC1 =  0;
    set Ni=InsCode i;
    IC s + 1 = 0+1 by A1,MEMSTR_0:47;
    then
A12: Ni in {0,1,4,5,6,14} by A10,A11,SCMPDS_4:1;
A13: CurInstr(PI,Comput(PI,s,1)) = PI. 0 by A11,PBOOLE:143
      .= i by A4,A6,A7,GRFUNC_1:2;
A14: Ni <> 1 by Th10;
    hereby
      per cases;
      suppose
        i = halt SCMPDS;
        hence thesis by A2,A10,A13,EXTPRO_1:def 9;
      end;
      suppose
A15:    i <> halt SCMPDS;
A16:    now
          let b;
          per cases by A12,A14,ENUMSET1:def 4;
          suppose
            InsCode i = 0;
            hence s.b=Exec(i, s).b by SCMPDS_2:86;
          end;
          suppose
            InsCode i = 14;
            then ex k1 st i = goto k1 by SCMPDS_2:26;
            hence s.b=Exec(i, s).b by SCMPDS_2:54;
          end;
          suppose
            InsCode i = 4;
            then ex a,k1,k2 st i = (a,k1)<>0_goto k2 by SCMPDS_2:30;
            hence s.b=Exec(i, s).b by SCMPDS_2:55;
          end;
          suppose
            InsCode i = 5;
            then ex a,k1,k2 st i = (a,k1)<=0_goto k2 by SCMPDS_2:31;
            hence s.b=Exec(i, s).b by SCMPDS_2:56;
          end;
          suppose
            InsCode i = 6;
            then ex a,k1,k2 st i = (a,k1)>=0_goto k2 by SCMPDS_2:32;
            hence s.b=Exec(i, s).b by SCMPDS_2:57;
          end;
        end;
A17:    Following(PI,s) = Following(PI,Comput(PI,s,0))
          .= Exec(i, s) by A10,EXTPRO_1:3;
A18:    IC s = IC Exec(i, s) by A10,A11,A1,MEMSTR_0:47;
        then
A19:    s = Exec(i, s) by A16,SCMPDS_2:44;
        now
          let n;
          Comput(PI, s,n) = s by A18,A16,A17,EXTPRO_1:27,SCMPDS_2:44
            .= Following(PI,Comput(PI,s,0))
            by A19,A17
            .= Comput(PI, s,0+1) by EXTPRO_1:3;
          hence CurInstr(PI,Comput(PI,s,n)) <> halt SCMPDS by A13,A15;
        end;
        then not PI halts_on s;
        hence thesis by A7,SCMPDS_4:def 7;
      end;
    end;
  end;
  suppose
A20:    IC1 =  1;
    CurInstr(PI,Comput(PI,s,1))
     = PI. 1 by A20,PBOOLE:143
      .= halt SCMPDS by A3,A5,A7,GRFUNC_1:2;
    hence thesis by A2,A10,EXTPRO_1:def 9;
  end;
end;

theorem Th28:
 for s being 0-started State of SCMPDS
  for I being parahalting halt-free Program of SCMPDS,
      j being parahalting shiftable Instruction of SCMPDS
 holds IExec(I ';' j,P,s).a = Exec(j,IExec(I,P,s)).a
proof
  let s be 0-started State of SCMPDS;
  let I be parahalting halt-free Program of SCMPDS,j be parahalting
  shiftable Instruction of SCMPDS;
  set Mj = Load j;
  set SA = Start-At (IC IExec(Mj,P,Initialize IExec(I,P,s)) + card I,SCMPDS);
A1: not a in dom SA by SCMPDS_4:18;
A2: a in SCM-Data-Loc by AMI_2:def 16;
  for a holds (Initialize IExec(I,P,s)).a = IExec(I,P,s).a by Th4;
  then
A3: DataPart Initialize IExec(I,P,s) = DataPart IExec(I,P,s) by SCMPDS_4:8;
  thus IExec(I ';' j,P,s).a
   = IncIC(IExec(Mj,P,Initialize IExec(I,P,s)),card I).a by Th22
    .= IExec(Mj,P,Initialize IExec(I,P,s)).a by A1,FUNCT_4:11
    .= Exec(j, Initialize IExec(I,P,s)).a by Th27
    .= (DataPart Exec(j, Initialize IExec(I,P,s))).a
        by A2,FUNCT_1:49,SCMPDS_2:84
    .= (DataPart Exec(j, IExec(I,P,s))).a by A3,Th26
    .= Exec(j, IExec(I,P,s)).a by A2,FUNCT_1:49,SCMPDS_2:84;
end;

theorem
  for s being 0-started State of SCMPDS
  for i being No-StopCode parahalting Instruction of SCMPDS,
      j being shiftable parahalting Instruction of SCMPDS
 holds IExec(i ';' j,P,s).a = Exec(j,Exec(i, s)).a
proof
  let s be 0-started State of SCMPDS;
  let i be No-StopCode parahalting Instruction of SCMPDS, j be shiftable
  parahalting Instruction of SCMPDS;
  set Mi = Load i;
  thus IExec(i ';' j,P,s).a = IExec(Mi ';' j,P,s).a
    .= Exec(j, IExec(Mi,P,s)).a by Th28
    .= Exec(j, Exec(i, s)).a by Th27;
end;

subset_name: curated


TITLE: Proving an inequality involving the 2 first moments of a class of probability distribution
QUESTION [1 upvotes]: Let $X$ be a random variable such that $\langle e^{-X} \rangle = 1$ (which implies $\langle X \rangle \geq 0$). Here I use the notation $\mathbb{E}[X]=\langle X \rangle$.
I would like to show the following (hint from numerical evidence):
$$\frac{\langle X^2 \rangle }{\langle X \rangle }-\sqrt{\langle X^2 \rangle }\leq 2$$
Cauchy-Schwarz inequality gives that the previous expression is positive, but why would it be less than 2?
I found that this would be equivalent to
$$\langle X\rangle \geq \frac{\langle X^2 \rangle}{2+\sqrt{\langle X^2 \rangle }}  $$
or
$$\langle X^2 \rangle \leq \frac{\langle X \rangle^2}{2}+2\langle X \rangle +\frac{\langle X \rangle }{2}\sqrt{\langle X \rangle^2+8\langle X \rangle }$$
I am pretty sure that it comes from the constraint  $\langle e^{-X} \rangle = 1$ but I don't know how to use it. Any idea?

REPLY [1 votes]: A way to solve such problems is to look at the graph $\Gamma=\{(\exp(-x),x,x^2): x\in\mathbb R\}\subset\mathbb R^3\}$ of the map $x\mapsto(\exp(-x),x,x^2)$, at its convex hull $H$, and at the intersection  of $H$ with the set of points of form $(1,a,b)$, namely $M=\{(a,b):(1,a,b)\in H\}\subset\mathbb R^2$.
The points in $M$ are the $(EX,EX^2)=(\langle X\rangle,\langle X^2\rangle)$ that you are interested in.  Look for points in $M$ that are convex combinations of pairs of elements of $\Gamma$.  (The codimension of $M$ in $H$ is 1, so by a theorem of Dubins, extreme points in $M$ are mixtures of pairs of points in $\Gamma$.)
Added 8 hours later.  I don't think the claimed result is true.  If $P(X=-0.340221)=0.711613$ and $P(X=15.555439)=0.288387)$ then $E e^{-X} =1$, $a=E X= 4.243876$, and $b=EX^2= 69.863772$.  But $2+\sqrt b - b/a = -6.103803$, contrary to the OP's conjecture.  (Of course these numbers are how my computer rounded them off.  I told my computer to pick $u<0<v$ at random, to set $P(X=u)=(1-e^{-v})/(e^{-u}-e^{-v})$ and $P(X=v))=(e^{-u}-1)/(e^{-u}-e^{-v})$, so $E\exp^{-X}=1$, and to work out the corresponding $a$ and $b$.) Maybe the OP's numerical experiments were based on the false hypothesis that $X\ge0$ a.s.


TITLE: Proving that the pointwise limit function of sequence of measurable functions is measurable without limsup or liminf
QUESTION [0 upvotes]: Let $ \{f_n\} $ be a sequence of Lebesgue measurable real valued functions defined on some Lebesgue measurable set E. Suppose the sequence converges pointwise on $E$ to some function $f$. Prove that $f$ is Lebesgue measurable.
Most of the proofs I have seen use the limit superior and limit inferior of $f$. I would like an alternative proof that does not use this. Are there any?
Thanks.

REPLY [1 votes]: Such a proof can be found here.
Let me translate.
Consider $U$ an open subset of $\mathbb R$. Let $U_n=\{x\in U, \;\; d(x,  \mathbb R\setminus U)>\frac 1n\}$ and $F_n=\{x\in U , \;\; d(x,  \mathbb R\setminus U)\geq\frac 1n\}$.
Note that: each $U_n$ is open, each $F_n$ is closed, $\cup_n U_n = U$ and $\cup_n F_n=F$.
The following inclusions hold:
$$\begin{align} f^{-1}(U)
&= \cup_n f^{-1}(U_n)  \\
&= \cup_n \{x, \;\; \lim_k f_k(x)\in U_n\}\\
&\subset \cup_n \{x, \;\; \exists K, \forall k\geq K, f_k(x)\in U_n\} \\
&\subset \cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(U_n)\\
\end{align}$$
Note that $\cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(U_n)$ is a member of the sigma-algebra you defined on $E$.
Since $U_n\subset F_n$, $$\cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(U_n) \subset \cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(F_n)$$
Note that for any $n$, $$\cup_K \cap_{k\geq K} \;f_k^{-1}(F_n) = \{x, \exists K, \forall k\geq K, f_k^{-1}(x)\in F_n\}\subset \{x, f(x)\in F_n\}= f^{-1}(F_n)$$
Therefore,
$$\begin{align} \cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(U_n)
&\subset \cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(F_n)\\
&\subset \cup_n f^{-1}(F_n)\\
&= f^{-1}(\cup_n F_n)\\
&= f^{-1}(U)
\end{align}$$
Conclusion: $$f^{-1}(U)  = \cup_n \cup_K \cap_{k\geq K} \;f_k^{-1}(U_n) \in \Sigma $$


TITLE: A probability problem on finding expectation
QUESTION [0 upvotes]: If the random variable $X$ is $N(\mu,1)$, show that the random variable $Y=\frac{1-\Phi(X)}{\phi({X})}$, where $\Phi$ and $\phi$ denote the cdf and pdf of $N(0,1)$, respectively has mean value $\frac{1}{\mu}$. How to proceed in this problem ?

REPLY [1 votes]: The LOTUS should be used and then an interchange of the limits of integration.
$$Y=\frac{1-\Phi(X)}{\phi({X})} = g(X) \Rightarrow E(Y) = \int_{-\infty}^{\infty} f_X(x)g(x) dx= \int_{-\infty}^{\infty} \phi(x-\mu)\frac{1-\Phi(x)}{\phi({x})} dx$$
Calculate explicitly
$$\phi(x-\mu) = \phi(x) \cdot \exp\left \{\mu x\right\} \cdot \exp\left \{-\frac 12 \mu^2\right \}$$
Then
$$E(Y) = \int_{-\infty}^{\infty} \phi(x) \cdot \exp\left \{\mu x\right\} \cdot \exp\left \{-\frac 12 \mu^2\right \}\frac{1-\Phi(x)}{\phi({x})} dx  $$
$$=  \exp\left \{-\frac 12 \mu^2\right \}\int_{-\infty}^{\infty} \exp\left \{\mu x\right\} \left[1-\Phi(x)\right]dx=   \exp\left \{-\frac 12 \mu^2\right \}\int_{-\infty}^{\infty} \exp\left \{\mu x\right\} \Phi(-x)dx $$
We have
$$I_x = \int_{-\infty}^{\infty} \exp\left \{\mu x\right\} \Phi(-x)dx =  \int_{-\infty}^{\infty} \exp\left \{\mu x\right\} \int_{-\infty}^{-x}\phi(z)dzdx = \int_{-\infty}^{\infty}\int_{-\infty}^{-x} \exp\left \{\mu x\right\} \phi(z)dzdx $$
where $z$ is a dummy variable of integration.
Interchange the limits of integration from
\begin{matrix}
-\infty \le x \le \infty\\
-\infty \le z \le -  x
\end{matrix}
to
\begin{matrix}
-\infty \le z \le \infty\\
-\infty \le x \le -  z
\end{matrix}
Then
$$I_x  = \int_{-\infty}^{\infty}\int_{-\infty}^{-z} \exp\left \{\mu x\right\} \phi(z)dxdz =  \int_{-\infty}^{\infty}\phi(z) \Big[\frac {1}{\mu}\exp\left \{\mu x\right\}\Big |_{-\infty}^{-z}\Big]dz$$
$$ =  \frac {1}{\mu}\int_{-\infty}^{\infty}\exp\left \{-\mu z\right\}\phi(z) dz $$
The integral is now the moment generating function in $-\mu$ of a standard normal random variable $Z$,
$$\int_{-\infty}^{\infty}\exp\left \{-\mu z\right\}\phi(z) dz = \text {MGF}_Z(-\mu) = \exp\left\{\frac 12 (-\mu)^2 \right\}= \exp\left\{\frac 12 \mu^2 \right\}$$
So
$$ I_x = \frac {1}{\mu}\exp\left\{\frac 12 \mu^2 \right\} \Rightarrow E(Y) = \exp\left \{-\frac 12 \mu^2\right \}\frac {1}{\mu}\exp\left\{\frac 12 \mu^2 \right\} = \frac {1}{\mu} $$


TITLE: Probability of at least X consecutive failures over N period given P success rate
QUESTION [3 upvotes]: I am trying to figure out the formula used to calculate the numbers of the spreadsheet that I just posted.
To summarize, it is the probability of seeing at least (X) consecutive losing trades within a 50-trade period, given a list of defined winning percentages.
I want the formula/model to solve this so I am able to calculate the probabilities with variables of different values.
Example, the probability of seeing at least 15 consecutive losing trades over a 500-trade period, with a theoretical winning percentage of 45%.
Thank you very much to anybody who can help

REPLY [0 votes]: Here's some possibly-not-perfectly-Pythonic Python code to generate the table in a comma-separated-value format that you can load into common spreadsheet tools such as Excel. This also produces columns for $X=0$ and $X=1.$
Of course the probability in the $X=0$ column will always be $1$
(or very nearly $1,$ depending on how the roundoff errors add up).
def probability_list(p_success, max_failures, n_trials):
    # Returns a list of the probabilities of at least k failures
    # in n trials for k = 0..max_failures.

    p_failure = 1.0 - p_success

    # p_state[i][j] will be the probability that we currently have j
    # consecutive failures and the high-water mark is i consecutive failures.
    p_state = []
    for i in range(max_failures):
        p_state.append([0.0] * (i+1))
    p_max_failures = 0.0

    # Initially, we have never had any consecutive failures
    p_state[0][0] = 1.0

    for t in range(n_trials):
        new_p_state = []
        for i in range(max_failures):
            new_p_state.append([0.0] * (i+1))
        # Put the probabilities at time t+1 in new_p_state
        new_p_state[0][0] = p_success * p_state[0][0]
        for i in range(1, max_failures):
            new_p_state[i][0] = p_success * sum(p_state[i])
            for j in range(1, i + 1):
                new_p_state[i][j] = p_failure * p_state[i][j - 1]
            new_p_state[i][i] += p_failure * p_state[i - 1][i - 1]
        p_max_failures += p_failure * p_state[max_failures-1][max_failures-1]
        p_state = new_p_state

    # cum_p_highwater[i] will be the probability there were at least i
    # consecutive failures.
    cum_p_highwater = [0.0] * (max_failures + 1)
    cum_p_highwater[max_failures] = p_max_failures
    for i in range(max_failures - 1, -1, -1): # count down to zero
        cum_p_highwater[i] = sum(p_state[i]) + cum_p_highwater[i + 1]
    return cum_p_highwater

max_failures = 11
n_trials = 50

print ('p,', ','.join(str(n) for n in range(max_failures + 1)))

for k in range(1, 20):
    p_success = k * 0.05
    list_p = probability_list(p_success, max_failures, n_trials)
    print (p_success, ',', ','.join(str(p) for p in list_p))

The principle of this table is that it computes a probability distribution
over the longest losing sequence seen so far and the length of the current losing sequence, starting at zero trades executed and computing the probabilities after each additional trade from the probabilities before that trade.
The results of this script agree with a result from at least one other answer to this question and with other results I obtained from yet other calculations. They do not agree with the table from the website.
I think that table is either calculated badly or is based on assumptions that are unknown to us.


TITLE: Angle between two vectors equipped with special inner product.
QUESTION [2 upvotes]: Let $u\neq0 $ and $v\neq 0$ be two vectors in a vector space with inner product such as $\left \| u \right \|=\left \| v \right \|=\left \| u-v \right \|$. Determine the angle between $u$ and $v$.
Progress:
$\cos\theta=\frac{\left \langle u,v \right \rangle}{\left \| u \right \|\left \| v \right \|}=\frac{\left \langle u,v \right \rangle}{\left \| u-v \right \|^2}=\frac{\left \| u-v \right \|^2-2\left \| u \right \|^2}{2\left \| u \right \|^2}=\frac{-\left \| u \right \|^2}{2 \left \| u \right \|^2}=-\frac{1}{2}$
$\cos\theta=-\frac{1}{2}\rightarrow \theta=\frac{2\pi }{3}$. Correct answer is $\theta=\frac{\pi }{3}$

REPLY [2 votes]: Your third equality is wrong. Instead of $\frac{||u-v^2||^2-2||u||^2}{2||u||^2}$, it should read $\frac{2||u||^2-||u-v^2||^2}{2||u||^2}$, which yields the right answer.


TITLE: Inverse of disintegration theorem on euclidean spaces
QUESTION [1 upvotes]: i was asking myself if some sort of "inverse" of the disintegration theorem holds (or eventually when).
Let's say I have a family of Borel measures $(\mu_t)_{t \in [0,1]}$ over $R^d$ such that the map $t \rightarrow \mu_t(B)$ is borel measurable for each Borel set $B$, and let's say I want to associate to this family a finite Borel measure $\mu$ over $R^d \times [0,1]$ clearly such that if $f \in C_0^\infty(R^d \times [0,1])$ the following holds:
$\int_{R^d \times [0,1]} f(x,t)d\mu= \int_0^1 \int_{R^d}f(x,t)d\mu_tdt.$
Is this always possible?
edit: the family $\mu_t$ is a family of finite borel measures

REPLY [1 votes]: As the other states what you are looking for are products or compositions (different authors swap these around confusingly) of transition kernels. However there are different types of products and compositions in the literature, and the one you are looking for does not look exactly like the one provided in the Wiki pages, so will provide some more detail.
The collection $(\mu_t)$ defines a transition kernel $\kappa$ with source $([0,1],\mathcal B([0,1]))$ and target $(\mathbb R^d,\mathcal B(\mathbb R^d))$. In other words $\kappa:[0,1]\times \mathcal B(\mathbb R^d)\to[0,\infty)$ is defined by $\kappa(t,B)=\mu_t(B)$. Furthermore the Lebesgue measure $\lambda$ on $[0,1]$ can be thought of as a transition kernel from a singleton set $S:=\{s\}$ to $([0,1],\mathcal B([0,1]))$. This is all standard so far and contained in the Wiki article. Now what you are looking for is precisely a product(composition) kernel $\lambda\otimes \kappa$ from $S$ to the product space $[0,1]\times \mathbb R^d$ equipped with the product $\sigma$-algebra. This is defined for any $s\in S$ and $B\in \mathcal B([0,1])\otimes\mathcal B(\mathbb R^d)$ by
$$\lambda\otimes \kappa(s,B)=\int_{[0,1]}\int_{\mathbb R^d}\mathbb 1_B(t,x)\kappa(t,dx)\lambda(dt).$$
In our case $S$ is a singleton, so $\lambda\otimes \kappa$ is just a measure, and precisely the $\mu$ you want.
To understand it better we can examine its behaviour on product sets:
$$\mu(A\times B)=\int_{[0,1]}\mathbb 1_A(t)\int_{\mathbb R^d}\mathbb 1_B(x)\kappa(t,dx)\lambda(dt)=\int_{[0,1]}\mathbb 1_A(t)\mu_t(B)\lambda(dt).$$
From this characterisation you can easily prove (via Caratheodory extension theorem) that $\mu$ is indeed a Borel measure on $([0,1],\mathcal B([0,1]))$. Finally you can prove that your function characteristic holds for $\mu$ by taking the limit of step functions.


text:
(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "The Monty Hall Problem"

theory Monty imports "../pGCL" begin

text \<open>
We now tackle a more substantial example, allowing us to demonstrate
the tools for compositional reasoning and the use of invariants in
non-recursive programs.  Our example is the well-known Monty Hall puzzle
in statistical inference \citep{Selvin_75}.

The setting is a game show:  There is a prize hidden behind one
of three doors, and the contestant is invited to choose one.  Once
the guess is made, the host than opens one of the remaining two
doors, revealing a goat and showing that the prize is elsewhere.  The
contestent is then given the choice of switching their guess to the
other unopened door, or sticking to their first guess.

The puzzle is whether the contestant is better off switching or
staying put; or indeed whether it makes a difference at all.  Most people's
intuition suggests that it make no difference, whereas in fact,
switching raises the chance of success from 1/3 to 2/3.
\<close>

subsection \<open>The State Space\<close>

text \<open>The game state consists of the prize location, the guess,
and the clue (the door the host opens).  These are not constrained a
priori to the range @{term "{1::real,2,3}"}, but are simply natural numbers:
We instead show that this is in fact an invariant.
\<close>

record game =
  prize  :: nat
 "guess" :: nat
  clue   :: nat

text \<open>The victory condition: The player wins if they have guessed the
  correct door, when the game ends.\<close>
definition player_wins :: "game \<Rightarrow> bool"
where "player_wins g \<equiv> guess g = prize g"

subsubsection \<open>Invariants\<close>

text \<open>We prove explicitly that only valid doors are ever chosen.\<close>

definition inv_prize :: "game \<Rightarrow> bool"
where "inv_prize g \<equiv> prize g \<in> {1,2,3}"

definition inv_clue :: "game \<Rightarrow> bool"
where "inv_clue g \<equiv> clue g \<in> {1,2,3}"

definition inv_guess :: "game \<Rightarrow> bool"
where "inv_guess g \<equiv> guess g \<in> {1,2,3}"

subsection \<open>The Game\<close>

text \<open>Hide the prize behind door @{term D}.\<close>
definition hide_behind :: "nat \<Rightarrow> game prog"
where "hide_behind D \<equiv> Apply (prize_update (\<lambda>x. D))"

text \<open>Choose door @{term D}.\<close>
definition guess_behind :: "nat \<Rightarrow> game prog"
where "guess_behind D \<equiv> Apply (guess_update (\<lambda>x. D))"

text \<open>Open door @{term D} and reveal what's behind.\<close>
definition open_door :: "nat \<Rightarrow> game prog"
where "open_door D \<equiv> Apply (clue_update (\<lambda>x. D))"

text \<open>Hide the prize behind door 1, 2 or 3, demonically i.e.~according
  to any probability distribution (or none).\<close>
definition hide_prize :: "game prog"
where "hide_prize \<equiv> hide_behind 1 \<Sqinter> hide_behind 2 \<Sqinter> hide_behind 3"

text \<open>Guess uniformly at random.\<close>
definition make_guess :: "game prog"
where "make_guess \<equiv> guess_behind 1 \<^bsub>(\<lambda>s. 1/3)\<^esub>\<oplus>
                    guess_behind 2 \<^bsub>(\<lambda>s. 1/2)\<^esub>\<oplus> guess_behind 3"

text \<open>Open one of the two doors that \emph{doesn't} hide the prize.\<close>
definition reveal :: "game prog"
where "reveal \<equiv> \<Sqinter>d\<in>(\<lambda>s. {1,2,3} - {prize s, guess s}). open_door d"

text \<open>Switch your guess to the other unopened door.\<close>
definition switch_guess :: "game prog"
where "switch_guess \<equiv> \<Sqinter>d\<in>(\<lambda>s. {1,2,3} - {clue s, guess s}). guess_behind d"

text \<open>The complete game, either with or without switching guesses.\<close>
definition monty :: "bool \<Rightarrow> game prog"
where
  "monty switch \<equiv> hide_prize ;;
                  make_guess ;;
                  reveal ;;
                  (if switch then switch_guess else Skip)"

subsection \<open>A Brute Force Solution\<close>

text \<open>For sufficiently simple programs, we can calculate the exact weakest
  pre-expectation by unfolding.\<close>

lemma eval_win[simp]:
  "p = g \<Longrightarrow> \<guillemotleft>player_wins\<guillemotright> (s\<lparr> prize := p, guess := g, clue := c \<rparr>) = 1"
  by(simp add:embed_bool_def player_wins_def)

lemma eval_loss[simp]:
  "p \<noteq> g \<Longrightarrow> \<guillemotleft>player_wins\<guillemotright> (s\<lparr> prize := p, guess := g, clue := c \<rparr>) = 0"
  by(simp add:embed_bool_def player_wins_def)

text \<open>If they stick to their guns, the player wins with $p=1/3$.\<close>
lemma wp_monty_noswitch:
  "(\<lambda>s. 1/3) = wp (monty False) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def hide_prize_def make_guess_def reveal_def
            hide_behind_def guess_behind_def open_door_def
            switch_guess_def
  by(simp add:wp_eval insert_Diff_if o_def)

lemma swap_upd:
  "s\<lparr> prize := p, clue := c, guess := g \<rparr> =
   s\<lparr> prize := p, guess := g, clue := c \<rparr>"
  by(simp)

text \<open>If they switch, they win with $p=2/3$.  Brute force here
  takes longer, but is still feasible.  On larger programs,
  this will rapidly become impossible, as the size of the terms
  (generally) grows exponentially with the length of the program.\<close>

lemma wp_monty_switch_bruteforce:
  "(\<lambda>s. 2/3) = wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def hide_prize_def make_guess_def reveal_def
            hide_behind_def guess_behind_def open_door_def
            switch_guess_def
  \<comment> \<open>Note that this is getting slow\<close>
  by (simp add: wp_eval insert_Diff_if swap_upd o_def cong del: INF_cong_simp)

subsection \<open>A Modular Approach\<close>

text \<open>We can solve the problem more efficiently, at the cost of
  a little more user effort, by breaking up the problem and annotating
  each step of the game separately.  While this is not strictly necessary
  for this program, it will scale to larger examples, as the work in
  annotation only increases linearly with the length of the program.\<close>

subsubsection \<open>Healthiness\<close>

text \<open>We first establish healthiness for each step. This follows
  straightforwardly by applying the supplied rulesets.\<close>

lemma wd_hide_prize:
  "well_def hide_prize"
  unfolding hide_prize_def hide_behind_def
  by(simp add:wd_intros)

lemma wd_make_guess:
  "well_def make_guess"
  unfolding make_guess_def guess_behind_def
  by(simp add:wd_intros)

lemma wd_reveal:
  "well_def reveal"
proof -
  txt \<open>Here, we do need a subsidiary lemma: that there is always
    a `fresh' door available.  The rest of the healthiness proof follows
    as usual.\<close>
  have "\<And>s. {1, 2, 3} - {prize s, guess s} \<noteq> {}"
    by(auto simp:insert_Diff_if)
  thus ?thesis
    unfolding reveal_def open_door_def
    by(intro wd_intros, auto)
qed

lemma wd_switch_guess:
  "well_def switch_guess"
proof -
  have "\<And>s. {1, 2, 3} - {clue s, guess s} \<noteq> {}"
    by(auto simp:insert_Diff_if)
  thus ?thesis
    unfolding switch_guess_def guess_behind_def
    by(intro wd_intros, auto)
qed

lemmas monty_healthy =
  wd_switch_guess wd_reveal wd_make_guess wd_hide_prize

subsubsection \<open>Annotations\<close>

text \<open>We now annotate each step individually, and then combine them to
  produce an annotation for the entire program.\<close>

text \<open>@{term hide_prize} chooses a valid door.\<close>
lemma wp_hide_prize:
  "(\<lambda>s. 1) \<tturnstile> wp hide_prize \<guillemotleft>inv_prize\<guillemotright>"
  unfolding hide_prize_def hide_behind_def wp_eval o_def
  by(simp add:embed_bool_def inv_prize_def)

text \<open>Given the prize invariant, @{term make_guess} chooses a valid
  door, and guesses incorrectly with probability at least 2/3.\<close>
lemma wp_make_guess:
  "(\<lambda>s. 2/3 * \<guillemotleft>\<lambda>g. inv_prize g\<guillemotright> s) \<tturnstile>
   wp make_guess \<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g\<guillemotright>"
  unfolding make_guess_def guess_behind_def wp_eval o_def
  by(auto simp:embed_bool_def inv_prize_def inv_guess_def)

lemma last_one:
  assumes "a \<noteq> b" and "a \<in> {1::nat,2,3}" and "b \<in> {1,2,3}"
  shows "\<exists>!c. {1,2,3} - {b,a} = {c}"
  apply(simp add:insert_Diff_if)
  using assms by(auto intro:assms)

text \<open>Given the composed invariants, and an incorrect guess, @{term reveal}
  will give a clue that is neither the prize, nor the guess.\<close>
lemma wp_reveal:
  "\<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g\<guillemotright> \<tturnstile>
   wp reveal \<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and>
                  clue g \<noteq> prize g \<and>
                  clue g \<noteq> guess g \<and>
                  inv_prize g \<and> inv_guess g \<and> inv_clue g\<guillemotright>"
  (is "?X \<tturnstile> wp reveal ?Y")
proof(rule use_premise, rule well_def_wp_healthy[OF wd_reveal], clarify)
  fix s
  assume "guess s \<noteq> prize s"
     and "inv_prize s"
     and "inv_guess s"
  moreover then obtain c
    where singleton: "{Suc 0,2,3} -  {prize s, guess s} = {c}"
      and "c \<noteq> prize s"
      and "c \<noteq> guess s"
      and "c \<in> {Suc 0,2,3}"
    unfolding inv_prize_def inv_guess_def
    by(force dest:last_one elim!:ex1E)
  ultimately show "1 \<le> wp reveal ?Y s"
    by(simp add:reveal_def open_door_def wp_eval singleton o_def
                embed_bool_def inv_prize_def inv_guess_def inv_clue_def)
qed

text \<open>Showing that the three doors are all district is a largeish
  first-order problem, for which sledgehammer gives us a reasonable
  script.\<close>
lemma distinct_game:
  "\<lbrakk> guess g \<noteq> prize g; clue g \<noteq> prize g; clue g \<noteq> guess g;
     inv_prize g; inv_guess g; inv_clue g \<rbrakk> \<Longrightarrow>
   {1, 2, 3} = {guess g, prize g, clue g}"
  unfolding inv_prize_def inv_guess_def inv_clue_def
  apply(rule set_eqI)
  apply(rule iffI)
   apply(clarify)
   apply(metis (full_types) empty_iff insert_iff)
  apply(metis insert_iff)
  done

text \<open>Given the invariants, switching from the wrong guess gives
  the right one.\<close>
lemma wp_switch_guess:
  "\<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and>
        inv_prize g \<and> inv_guess g \<and> inv_clue g\<guillemotright> \<tturnstile>
   wp switch_guess \<guillemotleft>player_wins\<guillemotright>"
proof(rule use_premise, safe)
  from wd_switch_guess show "healthy (wp switch_guess)" by(auto)

  fix s
  assume "guess s \<noteq> prize s" and "clue s \<noteq> prize s"
     and "clue s \<noteq> guess s" and "inv_prize s"
     and "inv_guess s" and "inv_clue s"
  note state = this
  hence "1 \<le> Inf ((\<lambda>a. \<guillemotleft> player_wins \<guillemotright> (s\<lparr>guess := a\<rparr>)) `
    ({guess s, prize s, clue s} - {clue s, guess s}))"
    by(auto simp:insert_Diff_if player_wins_def)
  also from state
  have "... = Inf ((\<lambda>a. \<guillemotleft> player_wins \<guillemotright> (s\<lparr>guess := a\<rparr>)) `
                  ({1, 2, 3} - {clue s, guess s}))"
    by(simp add:distinct_game[symmetric])
  also have "... = wp switch_guess \<guillemotleft>player_wins\<guillemotright> s"
    by(simp add:switch_guess_def guess_behind_def wp_eval o_def)
  finally show "1 \<le> wp switch_guess \<guillemotleft> player_wins \<guillemotright> s" .
qed

text \<open>Given componentwise specifications, we can glue them together
with calculational reasoning to get our result.\<close>
lemma wp_monty_switch_modular:
  "(\<lambda>s. 2/3) \<tturnstile> wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
proof(rule wp_validD)  \<comment> \<open>Work in probabilistic Hoare triples\<close>
  note wp_validI[OF wp_scale, OF wp_hide_prize, simplified]
    \<comment> \<open>Here we apply scaling to match our pre-expectation\<close>
  also note wp_validI[OF wp_make_guess]
  also note wp_validI[OF wp_reveal]
  also note wp_validI[OF wp_switch_guess]
  finally show "\<lbrace>\<lambda>s. 2/3\<rbrace> monty True \<lbrace>\<guillemotleft>player_wins\<guillemotright>\<rbrace>p"
    unfolding monty_def
    by(simp add:wd_intros sound_intros monty_healthy)
qed

subsubsection \<open>Using the VCG\<close>

lemmas scaled_hide = wp_scale[OF wp_hide_prize, simplified]
declare scaled_hide[pwp] wp_make_guess[pwp] wp_reveal[pwp] wp_switch_guess[pwp]
declare wd_hide_prize[wd] wd_make_guess[wd] wd_reveal[wd] wd_switch_guess[wd]

text \<open>Alternatively, the VCG will get this using the same annotations.\<close>
lemma wp_monty_switch_vcg:
  "(\<lambda>s. 2/3) \<tturnstile> wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def
  by(simp, pvcg)

end