The abstract of the Mizar article:

The Construction and Computation of Conditional Statements for SCMPDS

by

Jing-Chao Chen

Received June 15, 1999

MML identifier: SCMPDS_6

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, SCMPDS_2, AMI_1, INT_1, SCMPDS_4, AMI_2, RELAT_1, BOOLE,
      SCM_1, FUNCT_1, FUNCT_7, SCMFSA6A, FUNCT_4, SCMPDS_3, CARD_1, SCMFSA_7,
      ABSVALUE, ARYTM_1, RELOC, SCMFSA6B, SCMPDS_5, AMI_5, SCMFSA8A, CAT_1,
      UNIALG_2, SCMFSA7B, SCMFSA8B, SCMPDS_6;
 notation TARSKI, XBOOLE_0, XCMPLX_0, XREAL_0, ABSVALUE, RELAT_1, FUNCT_1,
      FUNCT_4, INT_1, NAT_1, STRUCT_0, AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7,
      SCMPDS_2, SCMPDS_3, CARD_1, SCMPDS_4, SCM_1, SCMPDS_5;
 constructors NAT_1, AMI_5, SCMFSA_4, SCMPDS_4, SCM_1, SCMPDS_5;
 clusters AMI_1, INT_1, FUNCT_1, SCMPDS_2, SCMFSA_4, SCMPDS_4, SCMPDS_5, NAT_1,
      FRAENKEL, XREAL_0, ORDINAL2, NUMBERS;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve m,n for Nat,
        a for Int_position,
        i,j for Instruction of SCMPDS,
        s,s1,s2 for State of SCMPDS,
        k1 for Integer,
        loc for Instruction-Location of SCMPDS,
        I,J,K for Program-block;

theorem :: SCMPDS_6:1  :: S8A_Th3
 for s being State of SCMPDS holds
     dom (s | the Instruction-Locations of SCMPDS) =
         the Instruction-Locations of SCMPDS;

theorem :: SCMPDS_6:2  ::S8A_Th4
 for s being State of SCMPDS st s is halting
 for k being Nat st LifeSpan s <= k holds
     CurInstr (Computation s).k = halt SCMPDS;

theorem :: SCMPDS_6:3  ::S8A_Th5
 for s being State of SCMPDS st s is halting
 for k being Nat st LifeSpan s <= k holds
     IC (Computation s).k = IC (Computation s).LifeSpan s;

theorem :: SCMPDS_6:4  ::S8A_Th6
 for s1,s2 being State of SCMPDS holds
     s1,s2 equal_outside the Instruction-Locations of SCMPDS
 iff IC s1 = IC s2 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc;

theorem :: SCMPDS_6:5     ::S8A_TI8
   for s being State of SCMPDS, I being Program-block holds
     Initialized s +* Initialized I = s +* Initialized I;

theorem :: SCMPDS_6:6  ::S8A_Th9
   for I being Program-block, l being Instruction-Location of SCMPDS holds
     I c= I +* Start-At l;

theorem :: SCMPDS_6:7
 for s being State of SCMPDS, l being Instruction-Location of SCMPDS holds
     s | SCM-Data-Loc = (s +* Start-At l) | SCM-Data-Loc;

theorem :: SCMPDS_6:8   ::S8A_11
 for s being State of SCMPDS,I being Program-block,
 l being Instruction-Location of SCMPDS holds
     s | SCM-Data-Loc = (s +* (I +* Start-At l)) | SCM-Data-Loc;

theorem :: SCMPDS_6:9
 for s being State of SCMPDS,I being Program-block
 holds s | SCM-Data-Loc = (s +* Initialized I) | SCM-Data-Loc;

theorem :: SCMPDS_6:10  :: S8A_Th12
 for s being State of SCMPDS, l being Instruction-Location of SCMPDS holds
     dom (s | the Instruction-Locations of SCMPDS) misses dom Start-At l;

theorem :: SCMPDS_6:11  ::S8A_Th14
   for s being State of SCMPDS, I,J being Program-block,
 l being Instruction-Location of SCMPDS holds
     s +* (I +* Start-At l), s +* (J +* Start-At l)
         equal_outside the Instruction-Locations of SCMPDS;

theorem :: SCMPDS_6:12  ::S8B_7
 for s1,s2 be State of SCMPDS,I,J be Program-block holds
     s1 | SCM-Data-Loc = s2 | SCM-Data-Loc implies
     s1 +* Initialized I, s2 +* Initialized J
       equal_outside the Instruction-Locations of SCMPDS;

theorem :: SCMPDS_6:13
   for I being programmed FinPartState of SCMPDS, x being set holds
     x in dom I implies I.x is Instruction of SCMPDS;

theorem :: SCMPDS_6:14  ::S8B_Th4
 for s being State of SCMPDS, l1,l2 being Instruction-Location of SCMPDS
 holds s +* Start-At l1 +* Start-At l2 = s +* Start-At l2;

theorem :: SCMPDS_6:15
     card (i ';' I)= card I + 1;

theorem :: SCMPDS_6:16
   (i ';' I).inspos 0=i;

theorem :: SCMPDS_6:17     ::SP_15
  I c= Initialized stop I;

theorem :: SCMPDS_6:18
   loc in dom I implies loc in dom (stop I);

theorem :: SCMPDS_6:19
   loc in dom I implies (stop I).loc=I.loc;

theorem :: SCMPDS_6:20
   loc in dom I implies (Initialized stop I).loc=I.loc;

theorem :: SCMPDS_6:21
     IC (s+* Initialized I)=inspos 0;

theorem :: SCMPDS_6:22
     CurInstr (s+* Initialized stop(i ';' I)) = i;

theorem :: SCMPDS_6:23
 for s being State of SCMPDS,m1,m2 being Nat st IC s=inspos m1
 holds ICplusConst(s,m2)=inspos (m1+m2);

theorem :: SCMPDS_6:24
 for I,J being Program-block holds
     Shift(stop J,card I) c= stop(I ';' J);

theorem :: SCMPDS_6:25
  inspos(card I) in dom (stop I) & (stop I).inspos(card I) = halt SCMPDS;

theorem :: SCMPDS_6:26
  for x,l being Instruction-Location of SCMPDS holds
    IExec(J,s).x = (IExec(I,s) +* Start-At l).x;

theorem :: SCMPDS_6:27
  for x,l being Instruction-Location of SCMPDS holds
    IExec(I,s).x = (s +* Start-At l).x;

theorem :: SCMPDS_6:28  ::S8B_12
   for s being State of SCMPDS, i being No-StopCode parahalting Instruction
 of SCMPDS,J being parahalting shiftable Program-block,a being Int_position
 holds IExec(i ';' J,s).a = IExec(J,Exec(i,Initialized s)).a;

theorem :: SCMPDS_6:29
 for a being Int_position,k1,k2 being Integer holds
     (a,k1)<>0_goto k2 <> halt SCMPDS;

theorem :: SCMPDS_6:30
 for a being Int_position,k1,k2 being Integer holds
     (a,k1)<=0_goto k2 <> halt SCMPDS;

theorem :: SCMPDS_6:31
 for a being Int_position,k1,k2 being Integer holds
     (a,k1)>=0_goto k2 <> halt SCMPDS;

definition
 let k1;
 func Goto k1 -> Program-block equals
:: SCMPDS_6:def 1
   Load (goto k1);
end;

definition
   let n be Nat;
   cluster goto (n+1) -> No-StopCode;

   cluster goto -(n+1) -> No-StopCode;
end;

definition
   let n be Nat;
   cluster Goto (n+1) -> No-StopCode;

   cluster Goto -(n+1) -> No-StopCode;
end;

theorem :: SCMPDS_6:32
    card Goto k1 = 1;

theorem :: SCMPDS_6:33  ::S8A_Th47
     inspos 0 in dom Goto k1 & (Goto k1).inspos 0 = goto k1;

begin :: The predicates of is_closed_on and is_halting_on

definition
 let I be Program-block;
 let s be State of SCMPDS;
 pred I is_closed_on s means
:: SCMPDS_6:def 2
     for k being Nat holds
     IC (Computation (s +* Initialized stop I )).k in dom stop I;
 pred I is_halting_on s means
:: SCMPDS_6:def 3
    s +* Initialized stop I is halting;
end;

theorem :: SCMPDS_6:34  ::S7B_Th24
 for I being Program-block holds
     I is paraclosed iff for s being State of SCMPDS holds I is_closed_on s;

theorem :: SCMPDS_6:35   ::S7B_25
 for I being Program-block holds
  I is parahalting iff for s being State of SCMPDS holds I is_halting_on s;

theorem :: SCMPDS_6:36
 for s1,s2 being State of SCMPDS, I being Program-block st
     s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
     I is_closed_on s1 implies I is_closed_on s2;

theorem :: SCMPDS_6:37  ::S8B_Th8
   for s1,s2 being State of SCMPDS,I being Program-block st
  s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
     I is_closed_on s1 & I is_halting_on s1 implies
     I is_closed_on s2 & I is_halting_on s2;

theorem :: SCMPDS_6:38  ::S8B_Th9
 for s being State of SCMPDS, I,J being Program-block holds
     I is_closed_on s iff I is_closed_on s +* Initialized J;

theorem :: SCMPDS_6:39
 for I,J being Program-block,s being State of SCMPDS
 st I is_closed_on s & I is_halting_on s holds
 (for k being Nat st k <= LifeSpan (s +* Initialized stop I) holds
     IC (Computation (s +* Initialized stop I)).k =
         IC (Computation (s +* Initialized stop (I ';' J))).k) &
 (Computation (s +* Initialized stop I)).
   (LifeSpan (s +* Initialized stop I)) | SCM-Data-Loc =
     (Computation (s +* Initialized stop (I ';' J))).
         (LifeSpan (s +* Initialized stop I)) | SCM-Data-Loc;

theorem :: SCMPDS_6:40
 for I being Program-block,k be Nat st I is_closed_on s &
 I is_halting_on s & k < LifeSpan (s +* Initialized stop(I))
 holds IC (Computation (s +* Initialized stop(I))).k in dom I;

theorem :: SCMPDS_6:41
 for I,J being Program-block,s being State of SCMPDS,k being Nat
 st I is_closed_on s & I is_halting_on s &
   k < LifeSpan (s +* Initialized stop I) holds
     CurInstr (Computation (s +* Initialized stop I)).k =
     CurInstr (Computation (s +* Initialized stop (I ';' J))).k;

theorem :: SCMPDS_6:42      ::SCMPDS_5:32
 for I being No-StopCode Program-block,s being State of SCMPDS,
 k being Nat st I is_closed_on s & I is_halting_on s &
    k < LifeSpan (s +* Initialized stop I)
 holds CurInstr (Computation (s +* Initialized stop I)).k <> halt SCMPDS;

theorem :: SCMPDS_6:43
 for I being No-StopCode Program-block,s being State of SCMPDS
 st I is_closed_on s & I is_halting_on s holds
   IC (Computation (s +* Initialized stop I)).
   LifeSpan (s +* Initialized stop I) = inspos card I;

theorem :: SCMPDS_6:44   ::S8A_58
 for I,J being Program-block,s being State of SCMPDS
 st I is_closed_on s & I is_halting_on s
 holds
     I ';' Goto (card J + 1) ';' J is_halting_on s &
     I ';' Goto (card J + 1) ';' J is_closed_on s;

theorem :: SCMPDS_6:45   :: SP4_88,Th27
 for I being shiftable Program-block st
 Initialized stop I c= s1 & I is_closed_on s1
 for n being Nat st Shift(stop I,n) c= s2 &
   IC s2 = inspos n & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
   for i being Nat holds
     IC (Computation s1).i + n = IC (Computation s2).i &
     CurInstr ((Computation s1).i) = CurInstr ((Computation s2).i) &
     (Computation s1).i | SCM-Data-Loc = (Computation s2).i | SCM-Data-Loc;

theorem :: SCMPDS_6:46   ::SCMFSA8A:61
 for s being State of SCMPDS,I being No-StopCode Program-block,
 J being Program-block st I is_closed_on s & I is_halting_on s holds
 IC IExec(I ';' Goto (card J + 1) ';' J,s) =inspos (card I + card J + 1);

theorem :: SCMPDS_6:47   ::SCMFSA8A:62
 for s being State of SCMPDS,I being No-StopCode Program-block,
 J being Program-block st I is_closed_on s & I is_halting_on s holds
     IExec(I ';' Goto (card J + 1) ';' J,s) =
     IExec(I,s) +* Start-At inspos (card I + card J + 1);

theorem :: SCMPDS_6:48
 for s being State of SCMPDS,I being No-StopCode Program-block
 st I is_closed_on s & I is_halting_on s
 holds IC IExec(I,s) = inspos card I;

begin :: The construction of conditional statements

definition
 let a be Int_position,k be Integer;
 let I,J be Program-block;
 func if=0(a,k,I,J) -> Program-block equals
:: SCMPDS_6:def 4
    (a,k)<>0_goto (card I +2) ';' I ';' Goto (card J+1) ';' J;

 func if>0(a,k,I,J) -> Program-block equals
:: SCMPDS_6:def 5
    (a,k)<=0_goto (card I +2) ';' I ';' Goto (card J+1) ';' J;

 func if<0(a,k,I,J) -> Program-block equals
:: SCMPDS_6:def 6
   (a,k)>=0_goto (card I +2) ';' I ';' Goto (card J+1) ';' J;
end;

definition
 let a be Int_position,k be Integer;
 let I be Program-block;
 func if=0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 7
    (a,k)<>0_goto (card I +1) ';' I;

 func if<>0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 8
    (a,k)<>0_goto 2 ';' goto (card I+1) ';' I;

 func if>0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 9
    (a,k)<=0_goto (card I +1) ';' I;

 func if<=0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 10
   (a,k)<=0_goto 2 ';' goto (card I+1) ';' I;

 func if<0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 11
   (a,k)>=0_goto (card I +1) ';' I;

 func if>=0(a,k,I) -> Program-block equals
:: SCMPDS_6:def 12
    (a,k)>=0_goto 2 ';' goto (card I+1) ';' I;
end;

begin :: The computation of "if var=0 then block1 else block2"

theorem :: SCMPDS_6:49  ::S8B_14
     card if=0(a,k1,I,J) = card I + card J + 2;

theorem :: SCMPDS_6:50   ::LmT5
       inspos 0 in dom if=0(a,k1,I,J) & inspos 1 in dom if=0(a,k1,I,J);

theorem :: SCMPDS_6:51   ::Lm6
       if=0(a,k1,I,J).inspos 0 = (a,k1)<>0_goto (card I + 2);

theorem :: SCMPDS_6:52  ::S8B_18
 for s being State of SCMPDS, I,J being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)= 0 & I is_closed_on s & I is_halting_on s holds
     if=0(a,k1,I,J) is_closed_on s & if=0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:53  ::S8B_16
 for s being State of SCMPDS,I being Program-block,J being shiftable
 Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)<> 0 & J is_closed_on s & J is_halting_on s holds
     if=0(a,k1,I,J) is_closed_on s & if=0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:54  ::E,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 J being shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)= 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if=0(a,k1,I,J),s) = IExec(I,s) +*
       Start-At inspos (card I + card J + 2);

theorem :: SCMPDS_6:55  ::E,SCM8B_17
 for s being State of SCMPDS,I being Program-block,J being No-StopCode
 shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)<> 0 & J is_closed_on s & J is_halting_on s holds
  IExec(if=0(a,k1,I,J),s)
   = IExec(J,s) +* Start-At inspos (card I + card J + 2);

definition
   let I,J be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if=0(a,k1,I,J) -> shiftable parahalting;
end;

definition
   let I,J be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if=0(a,k1,I,J) -> No-StopCode;
end;

theorem :: SCMPDS_6:56  ::E,S8B_21A
   for s being State of SCMPDS,I,J being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if=0(a,k1,I,J),s) = inspos (card I + card J + 2);

theorem :: SCMPDS_6:57  ::E,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,J being shiftable Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)= 0 holds
      IExec(if=0(a,k1,I,J),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:58  ::E,S8B_21C
   for s being State of SCMPDS,I being Program-block,J being No-StopCode
 parahalting shiftable Program-block,a,b being Int_position,k1 being
 Integer st s.DataLoc(s.a,k1)<> 0 holds
      IExec(if=0(a,k1,I,J),s).b = IExec(J,s).b;

begin :: The computation of "if var=0 then block"

theorem :: SCMPDS_6:59  ::E,S8B_14
     card if=0(a,k1,I) = card I + 1;

theorem :: SCMPDS_6:60
       inspos 0 in dom if=0(a,k1,I);

theorem :: SCMPDS_6:61    ::Lm6
       if=0(a,k1,I).inspos 0 = (a,k1)<>0_goto (card I + 1);

theorem :: SCMPDS_6:62  ::E,S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)= 0 & I is_closed_on s & I is_halting_on s holds
     if=0(a,k1,I) is_closed_on s & if=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:63  ::E,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)<> 0 holds
     if=0(a,k1,I) is_closed_on s & if=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:64  ::E,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)= 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if=0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 1);

theorem :: SCMPDS_6:65  ::E,SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)<> 0 holds
  IExec(if=0(a,k1,I),s) = s +* Start-At inspos (card I + 1);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if=0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if=0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:66  ::E2,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if=0(a,k1,I),s) = inspos (card I + 1);

theorem :: SCMPDS_6:67  ::E2,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)= 0 holds
      IExec(if=0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:68  ::E2,S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)<> 0 holds
      IExec(if=0(a,k1,I),s).b = s.b;

begin :: The computation of "if var<>0 then block"

theorem :: SCMPDS_6:69  ::E3,S8B_14
     card if<>0(a,k1,I) = card I + 2;

theorem :: SCMPDS_6:70     ::LmT5
     inspos 0 in dom if<>0(a,k1,I) & inspos 1 in dom if<>0(a,k1,I);

theorem :: SCMPDS_6:71    ::Lm6
     if<>0(a,k1,I).inspos 0 = (a,k1)<>0_goto 2 &
     if<>0(a,k1,I).inspos 1 = goto (card I + 1);

theorem :: SCMPDS_6:72  ::S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)<>0 & I is_closed_on s & I is_halting_on s holds
     if<>0(a,k1,I) is_closed_on s & if<>0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:73  ::E3,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)= 0 holds
     if<>0(a,k1,I) is_closed_on s & if<>0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:74  ::SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <> 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if<>0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 2);

theorem :: SCMPDS_6:75  ::SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)= 0 holds
  IExec(if<>0(a,k1,I),s) = s +* Start-At inspos (card I + 2);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if<>0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if<>0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:76  ::E3,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if<>0(a,k1,I),s) = inspos (card I + 2);

theorem :: SCMPDS_6:77  ::E3,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)<> 0 holds
      IExec(if<>0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:78  ::E3,S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)= 0 holds
      IExec(if<>0(a,k1,I),s).b = s.b;

begin :: The computation of "if var>0 then block1 else block2"

theorem :: SCMPDS_6:79  ::G,S8B_14
     card if>0(a,k1,I,J) = card I + card J + 2;

theorem :: SCMPDS_6:80
       inspos 0 in dom if>0(a,k1,I,J) & inspos 1 in dom if>0(a,k1,I,J);

theorem :: SCMPDS_6:81
       if>0(a,k1,I,J).inspos 0 = (a,k1)<=0_goto (card I + 2);

theorem :: SCMPDS_6:82  ::G,S8B_18
 for s being State of SCMPDS, I,J being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)>0 & I is_closed_on s & I is_halting_on s holds
     if>0(a,k1,I,J) is_closed_on s & if>0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:83  ::S8B_16
 for s being State of SCMPDS,I being Program-block,J being shiftable
 Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <= 0 & J is_closed_on s & J is_halting_on s holds
    if>0(a,k1,I,J) is_closed_on s & if>0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:84  ::G,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 J being shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) > 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if>0(a,k1,I,J),s) = IExec(I,s) +*
       Start-At inspos (card I + card J + 2);

theorem :: SCMPDS_6:85  ::G,SCM8B_17
 for s being State of SCMPDS,I being Program-block,J being No-StopCode
 shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <= 0 & J is_closed_on s & J is_halting_on s holds
  IExec(if>0(a,k1,I,J),s)
   = IExec(J,s) +* Start-At inspos (card I + card J + 2);

definition
   let I,J be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if>0(a,k1,I,J) -> shiftable parahalting;
end;

definition
   let I,J be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if>0(a,k1,I,J) -> No-StopCode;
end;

theorem :: SCMPDS_6:86  ::G,S8B_21A
   for s being State of SCMPDS,I,J being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if>0(a,k1,I,J),s) = inspos (card I + card J + 2);

theorem :: SCMPDS_6:87  ::G,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,J being shiftable Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)>0 holds
      IExec(if>0(a,k1,I,J),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:88  ::G,S8B_21C
   for s being State of SCMPDS,I being Program-block,J being No-StopCode
 parahalting shiftable Program-block,a,b being Int_position,k1 being
 Integer st s.DataLoc(s.a,k1) <= 0 holds
      IExec(if>0(a,k1,I,J),s).b = IExec(J,s).b;

begin :: The computation of "if var>0 then block"

theorem :: SCMPDS_6:89  ::S8B_14
     card if>0(a,k1,I) = card I + 1;

theorem :: SCMPDS_6:90     ::LmT5
       inspos 0 in dom if>0(a,k1,I);

theorem :: SCMPDS_6:91    ::Lm6
       if>0(a,k1,I).inspos 0 = (a,k1)<=0_goto (card I + 1);

theorem :: SCMPDS_6:92  ::G2,S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)> 0 & I is_closed_on s & I is_halting_on s holds
     if>0(a,k1,I) is_closed_on s & if>0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:93  ::G,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) <= 0 holds
     if>0(a,k1,I) is_closed_on s & if>0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:94  ::G2,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)> 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if>0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 1);

theorem :: SCMPDS_6:95  ::G2,SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) <= 0 holds
  IExec(if>0(a,k1,I),s) = s +* Start-At inspos (card I + 1);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if>0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if>0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:96  ::G,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if>0(a,k1,I),s) = inspos (card I + 1);

theorem :: SCMPDS_6:97  ::G,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)> 0 holds
      IExec(if>0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:98  ::G,S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) <= 0 holds
      IExec(if>0(a,k1,I),s).b = s.b;

begin :: The computation of "if var<=0 then block"

theorem :: SCMPDS_6:99  ::S8B_14
     card if<=0(a,k1,I) = card I + 2;

theorem :: SCMPDS_6:100     ::LmT5
     inspos 0 in dom if<=0(a,k1,I) & inspos 1 in dom if<=0(a,k1,I);

theorem :: SCMPDS_6:101    ::Lm6
     if<=0(a,k1,I).inspos 0 = (a,k1)<=0_goto 2 &
     if<=0(a,k1,I).inspos 1 = goto (card I + 1);

theorem :: SCMPDS_6:102  ::S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <= 0 & I is_closed_on s & I is_halting_on s holds
     if<=0(a,k1,I) is_closed_on s & if<=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:103  ::G3,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) > 0 holds
     if<=0(a,k1,I) is_closed_on s & if<=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:104  ::SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <= 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if<=0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 2);

theorem :: SCMPDS_6:105  ::G3,SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) > 0 holds
  IExec(if<=0(a,k1,I),s) = s +* Start-At inspos (card I + 2);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if<=0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if<=0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:106  ::G3,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if<=0(a,k1,I),s) = inspos (card I + 2);

theorem :: SCMPDS_6:107  ::G3,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) <= 0 holds
      IExec(if<=0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:108  ::S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) > 0 holds
      IExec(if<=0(a,k1,I),s).b = s.b;

begin :: The computation of "if var<0 then block1 else block2"

theorem :: SCMPDS_6:109  ::L,S8B_14
     card if<0(a,k1,I,J) = card I + card J + 2;

theorem :: SCMPDS_6:110
       inspos 0 in dom if<0(a,k1,I,J) & inspos 1 in dom if<0(a,k1,I,J);

theorem :: SCMPDS_6:111
       if<0(a,k1,I,J).inspos 0 = (a,k1)>=0_goto (card I + 2);

theorem :: SCMPDS_6:112  ::L,S8B_18
 for s being State of SCMPDS, I,J being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1)<0 & I is_closed_on s & I is_halting_on s holds
     if<0(a,k1,I,J) is_closed_on s & if<0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:113  ::L,S8B_16
 for s being State of SCMPDS,I being Program-block,J being shiftable
 Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) >= 0 & J is_closed_on s & J is_halting_on s holds
    if<0(a,k1,I,J) is_closed_on s & if<0(a,k1,I,J) is_halting_on s;

theorem :: SCMPDS_6:114  ::L,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 J being shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) < 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if<0(a,k1,I,J),s) = IExec(I,s) +*
       Start-At inspos (card I + card J + 2);

theorem :: SCMPDS_6:115  ::L,SCM8B_17
 for s being State of SCMPDS,I being Program-block,J being No-StopCode
 shiftable Program-block,a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) >= 0 & J is_closed_on s & J is_halting_on s holds
  IExec(if<0(a,k1,I,J),s)
   = IExec(J,s) +* Start-At inspos (card I + card J + 2);

definition
   let I,J be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if<0(a,k1,I,J) -> shiftable parahalting;
end;

definition
   let I,J be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if<0(a,k1,I,J) -> No-StopCode;
end;

theorem :: SCMPDS_6:116  ::L,S8B_21A
   for s being State of SCMPDS,I,J being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if<0(a,k1,I,J),s) = inspos (card I + card J + 2);

theorem :: SCMPDS_6:117  ::S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,J being shiftable Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1)<0 holds
      IExec(if<0(a,k1,I,J),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:118  ::L,S8B_21C
   for s being State of SCMPDS,I being Program-block,J being No-StopCode
 parahalting shiftable Program-block,a,b being Int_position,k1 being
 Integer st s.DataLoc(s.a,k1) >= 0 holds
      IExec(if<0(a,k1,I,J),s).b = IExec(J,s).b;

begin :: The computation of "if var<0 then block"

theorem :: SCMPDS_6:119  ::L2,S8B_14
     card if<0(a,k1,I) = card I + 1;

theorem :: SCMPDS_6:120     ::LmT5
       inspos 0 in dom if<0(a,k1,I);

theorem :: SCMPDS_6:121    ::Lm6
       if<0(a,k1,I).inspos 0 = (a,k1)>=0_goto (card I + 1);

theorem :: SCMPDS_6:122  ::L2,S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) < 0 & I is_closed_on s & I is_halting_on s holds
     if<0(a,k1,I) is_closed_on s & if<0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:123  ::L,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) >= 0 holds
     if<0(a,k1,I) is_closed_on s & if<0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:124  ::L,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) < 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if<0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 1);

theorem :: SCMPDS_6:125  ::L,SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) >= 0 holds
  IExec(if<0(a,k1,I),s) = s +* Start-At inspos (card I + 1);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if<0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if<0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:126  ::L2,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if<0(a,k1,I),s) = inspos (card I + 1);

theorem :: SCMPDS_6:127  ::L,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) < 0 holds
      IExec(if<0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:128  ::L2,S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) >= 0 holds
      IExec(if<0(a,k1,I),s).b = s.b;

begin :: The computation of "if var>=0 then block"

theorem :: SCMPDS_6:129  ::L3,S8B_14
     card if>=0(a,k1,I) = card I + 2;

theorem :: SCMPDS_6:130     ::LmT5
     inspos 0 in dom if>=0(a,k1,I) & inspos 1 in dom if>=0(a,k1,I);

theorem :: SCMPDS_6:131    ::Lm6
     if>=0(a,k1,I).inspos 0 = (a,k1)>=0_goto 2 &
     if>=0(a,k1,I).inspos 1 = goto (card I + 1);

theorem :: SCMPDS_6:132  ::S8B_18
 for s being State of SCMPDS, I being shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) >= 0 & I is_closed_on s & I is_halting_on s holds
     if>=0(a,k1,I) is_closed_on s & if>=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:133  ::L3,S8B_16
 for s being State of SCMPDS,I being Program-block, a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) < 0 holds
     if>=0(a,k1,I) is_closed_on s & if>=0(a,k1,I) is_halting_on s;

theorem :: SCMPDS_6:134  ::L,SCM8B_19
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) >= 0 & I is_closed_on s & I is_halting_on s holds
 IExec(if>=0(a,k1,I),s) = IExec(I,s) +* Start-At inspos (card I + 2);

theorem :: SCMPDS_6:135  ::L,SCM8B_17
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) < 0 holds
  IExec(if>=0(a,k1,I),s) = s +* Start-At inspos (card I + 2);

definition
   let I be shiftable parahalting Program-block,
   a be Int_position,k1 be Integer;
   cluster if>=0(a,k1,I) -> shiftable parahalting;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,k1 be Integer;
   cluster if>=0(a,k1,I) -> No-StopCode;
end;

theorem :: SCMPDS_6:136  ::L2,S8B_21A
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a being Int_position,k1 being Integer holds
     IC IExec(if>=0(a,k1,I),s) = inspos (card I + 2);

theorem :: SCMPDS_6:137   ::L,S8B_21B
   for s being State of SCMPDS,I being No-StopCode shiftable parahalting
 Program-block,a,b being Int_position,k1 being Integer
 st s.DataLoc(s.a,k1) >= 0 holds
      IExec(if>=0(a,k1,I),s).b = IExec(I,s).b;

theorem :: SCMPDS_6:138  ::L,S8B_21C
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 k1 being Integer st s.DataLoc(s.a,k1) < 0 holds
      IExec(if>=0(a,k1,I),s).b = s.b;