The abstract of the Mizar article:

While Macro Instructions of \SCMFSA

by

Jing-Chao Chen

Received December 10, 1997

MML identifier: SCMFSA_9

[ Mizar article, MML identifier index ]

environ

 vocabulary SCMFSA6A, SCMFSA_2, CARD_1, SCMFSA8B, SCMFSA8A, SCMFSA_4, FUNCT_4,
      CAT_1, AMI_3, RELAT_1, BOOLE, AMI_1, AMI_5, FUNCT_1, ARYTM_1, RELOC,
      SF_MASTR, SCMFSA7B, UNIALG_2, AMI_2, SCM_1, CARD_3, SCMFSA6B, FUNCOP_1,
      SCMFSA_9;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, CARD_1, CARD_3, AMI_1, AMI_3, SCM_1,
      AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA6B,
      SCMFSA7B, SCMFSA8A, SCMFSA8B;
 constructors NAT_1, AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, SCMFSA8A,
      SF_MASTR, SCMFSA8B;
 clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SF_MASTR, SCMFSA6B,
      SCMFSA7B, SCMFSA8A, INT_1, RELSET_1, NAT_1, FRAENKEL, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

theorem :: SCMFSA_9:1
 for I being Macro-Instruction, a being Int-Location holds
     card if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop) = card I + 6;

theorem :: SCMFSA_9:2
 for I being Macro-Instruction, a being Int-Location holds
     card if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop) = card I + 6;

:: WHILE  Statement
 reserve m, n for Nat;

definition
 let a be Int-Location;
 let I be Macro-Instruction;
 func while=0(a,I) -> Macro-Instruction equals
:: SCMFSA_9:def 1

 if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop) +*
  ( insloc (card I +4) .--> goto insloc 0 );

 func while>0(a,I) -> Macro-Instruction equals
:: SCMFSA_9:def 2

 if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop) +*
  ( insloc (card I +4) .--> goto insloc 0 );
end;

theorem :: SCMFSA_9:3
 for I being Macro-Instruction, a being Int-Location holds
     card if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0))
   = card I + 11;

definition
 let a be Int-Location;
 let I be Macro-Instruction;
 func while<0(a,I) -> Macro-Instruction equals
:: SCMFSA_9:def 3

  if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0)) +*
  ( insloc (card I +4) .--> goto insloc 0 );
end;

theorem :: SCMFSA_9:4
 for I being Macro-Instruction, a being Int-Location holds
     card while=0(a,I) = card I + 6;

theorem :: SCMFSA_9:5
 for I being Macro-Instruction, a being Int-Location holds
     card while>0(a,I) = card I + 6;

theorem :: SCMFSA_9:6
   for I being Macro-Instruction, a being Int-Location holds
     card while<0(a,I) = card I + 11;

theorem :: SCMFSA_9:7
 for a being Int-Location, l being Instruction-Location of SCM+FSA holds
     a =0_goto l <> halt SCM+FSA;

theorem :: SCMFSA_9:8
 for a being Int-Location, l being Instruction-Location of SCM+FSA holds
     a >0_goto l <> halt SCM+FSA;

theorem :: SCMFSA_9:9
 for l being Instruction-Location of SCM+FSA holds
     goto l <> halt SCM+FSA;

theorem :: SCMFSA_9:10
 for a being Int-Location, I being Macro-Instruction holds
   insloc 0 in dom while=0(a,I) &
   insloc 1 in dom while=0(a,I) &
   insloc 0 in dom while>0(a,I) &
   insloc 1 in dom while>0(a,I);

theorem :: SCMFSA_9:11
 for a being Int-Location, I being Macro-Instruction holds
   while=0(a,I).insloc 0 = a =0_goto insloc 4 &
   while=0(a,I).insloc 1 = goto insloc 2 &
   while>0(a,I).insloc 0 = a >0_goto insloc 4 &
   while>0(a,I).insloc 1 = goto insloc 2;

theorem :: SCMFSA_9:12
 for a being Int-Location, I being Macro-Instruction,k being Nat st
   k < 6 holds insloc k in dom while=0(a,I);

theorem :: SCMFSA_9:13
 for a being Int-Location, I being Macro-Instruction,k being Nat st
   k < 6 holds insloc (card I +k) in dom while=0(a,I);

theorem :: SCMFSA_9:14
 for a being Int-Location, I being Macro-Instruction holds
     while=0(a,I).insloc (card I +5) = halt SCM+FSA;

theorem :: SCMFSA_9:15
 for a being Int-Location, I being Macro-Instruction holds
     while=0(a,I).insloc 3 = goto insloc (card I +5);

theorem :: SCMFSA_9:16
 for a being Int-Location, I being Macro-Instruction holds
     while=0(a,I).insloc 2 = goto insloc 3;

theorem :: SCMFSA_9:17
   for a being Int-Location, I being Macro-Instruction,k being Nat st
   k < card I +6 holds insloc k in dom while=0(a,I);

theorem :: SCMFSA_9:18
 for s being State of SCM+FSA, I being Macro-Instruction,
   a being read-write Int-Location st s.a <> 0 holds
   while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s;

theorem :: SCMFSA_9:19
 for a being Int-Location, I being Macro-Instruction,
 s being State of SCM+FSA,k being Nat st
   I is_closed_on s & I is_halting_on s &
   k < LifeSpan (s +* (I +* Start-At insloc 0)) &
   IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k) =
   IC (Computation (s +* ( I +* Start-At insloc 0))).k + 4 &
   (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k) |
    (Int-Locations \/ FinSeq-Locations) =
   (Computation (s +* ( I +* Start-At insloc 0))).k |
    (Int-Locations \/ FinSeq-Locations) holds
   IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k+1) =
   IC (Computation (s +* (I +* Start-At insloc 0))).(k+1) + 4 &
   (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k+1) |
     (Int-Locations \/ FinSeq-Locations) =
   (Computation (s +* (I +* Start-At insloc 0))).(k+1) |
     (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA_9:20
 for a being Int-Location, I being Macro-Instruction,
  s being State of SCM+FSA st
   I is_closed_on s & I is_halting_on s &
   IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 +
   LifeSpan (s +* (I +* Start-At insloc 0 ) ) ) =
   IC (Computation (s +* ( I +* Start-At insloc 0))).
   LifeSpan (s +* (I +* Start-At insloc 0 ) ) + 4
   holds
   CurInstr (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 +
   LifeSpan (s +* (I +* Start-At insloc 0)) ) = goto insloc (card I +4);

theorem :: SCMFSA_9:21
 for a being Int-Location, I being Macro-Instruction holds
     while=0(a,I).insloc (card I +4) = goto insloc 0;

reserve f for FinSeq-Location,
        c for Int-Location;

theorem :: SCMFSA_9:22
 for s being State of SCM+FSA, I being Macro-Instruction,
 a being read-write Int-Location
 st I is_closed_on s & I is_halting_on s & s.a =0 holds
    IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).
    (LifeSpan (s +* (I +* Start-At insloc 0)) + 3) = insloc 0 &
    for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) + 3
    holds IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).k
    in dom while=0(a,I);

reserve s for State of SCM+FSA,
   I for Macro-Instruction,
   a for read-write Int-Location;

definition
 let s,I,a;
 func StepWhile=0(a,I,s) -> Function of NAT,product the Object-Kind of SCM+FSA
  means
:: SCMFSA_9:def 4

   it.0 = s &
   for i being Nat
    holds it.(i+1)=(Computation (it.i +* (while=0(a,I) +* sl0))).
      (LifeSpan (it.i +* (I +* sl0)) + 3);
end;

 reserve i,k,m,n for Nat;

canceled 2;

theorem :: SCMFSA_9:25
 StepWhile=0(a,I,s).(k+1)=StepWhile=0(a,I,StepWhile=0(a,I,s).k).1;

scheme MinIndex { F(Nat)->Nat,j() -> Nat} :
  ex k st F(k)=0 & for n st F(n)=0 holds k <= n
   provided
 F(0) = j() and
 for k holds (F(k+1) < F(k) or F(k) = 0);

theorem :: SCMFSA_9:26
   for f,g being Function holds f +* g +* g = f +* g;

theorem :: SCMFSA_9:27
 for f,g,h being Function, D being set holds
     (f +* g)|D =h | D implies (h +* g) | D = (f +* g) | D;

theorem :: SCMFSA_9:28
   for f,g,h being Function, D being set holds
     f | D =h | D implies (h +* g) | D = (f +* g) | D;

theorem :: SCMFSA_9:29
 for s1,s2 being State of SCM+FSA
       st IC s1 = IC s2 & s1 | (Int-Locations \/ FinSeq-Locations) =
       s2 | (Int-Locations \/ FinSeq-Locations) & s1 | IL = s2 | IL
  holds s1 = s2;

theorem :: SCMFSA_9:30
  for I being Macro-Instruction,a being read-write Int-Location,
   s being State of SCM+FSA holds
   StepWhile=0(a,I,s).(0+1)=(Computation (s +* (while=0(a,I) +* sl0))).
   (LifeSpan (s+* (I +* sl0)) + 3);

theorem :: SCMFSA_9:31
  for I being Macro-Instruction,a being read-write Int-Location,
   s being State of SCM+FSA,k,n being Nat st
IC StepWhile=0(a,I,s).k =insloc 0 & StepWhile=0(a,I,s).k=
(Computation (s +* (while=0(a,I) +* Start-At insloc 0))).n holds
StepWhile=0(a,I,s).k = StepWhile=0(a,I,s).k +* (while=0(a,I)+*
Start-At insloc 0) &
StepWhile=0(a,I,s).(k+1)=(Computation (s +* (while=0(a,I) +*
Start-At insloc 0))).
(n +(LifeSpan (StepWhile=0(a,I,s).k +* (I +* Start-At insloc 0)) + 3));

theorem :: SCMFSA_9:32
  for I being Macro-Instruction,a being read-write Int-Location,
    s being State of SCM+FSA st (for k being Nat holds
     I is_closed_on StepWhile=0(a,I,s).k &
     I is_halting_on StepWhile=0(a,I,s).k) &
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for k being Nat holds (f.(StepWhile=0(a,I,s).(k+1)) <
      f.(StepWhile=0(a,I,s).k)
      or f.(StepWhile=0(a,I,s).k) = 0) &
      ( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 ) )
     holds
     while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s;

theorem :: SCMFSA_9:33
  for I being parahalting Macro-Instruction, a being read-write
    Int-Location, s being State of SCM+FSA st
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for k being Nat holds (f.(StepWhile=0(a,I,s).(k+1)) <
      f.(StepWhile=0(a,I,s).k) or f.(StepWhile=0(a,I,s).k) = 0) &
      ( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 ) )
     holds
     while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s;

theorem :: SCMFSA_9:34
    for I being parahalting Macro-Instruction, a being read-write
  Int-Location st
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for s being State of SCM+FSA holds (f.(StepWhile=0(a,I,s).1) < f.s
      or f.s = 0) & ( f.s =0 iff s.a <> 0 ))
     holds while=0(a,I) is parahalting;

theorem :: SCMFSA_9:35
for l1,l2 being Instruction-Location of SCM+FSA,a being Int-Location holds
(l1 .--> goto l2) does_not_destroy a;

theorem :: SCMFSA_9:36
for i being Instruction of SCM+FSA st i does_not_destroy intloc 0 holds
Macro i is good;

definition
 let I,J be good Macro-Instruction,a be Int-Location;
 cluster if=0(a,I,J) -> good;
end;

definition
 let I be good Macro-Instruction,a be Int-Location;
 cluster while=0(a,I) -> good;
end;

:: -----------------------------------------------------------
:: WHILE>0  Statement

theorem :: SCMFSA_9:37
 for a being Int-Location, I being Macro-Instruction,k being Nat st
 k < 6 holds insloc k in dom while>0(a,I);

theorem :: SCMFSA_9:38
 for a being Int-Location, I being Macro-Instruction,k being Nat st
  k < 6 holds insloc (card I +k) in dom while>0(a,I);

theorem :: SCMFSA_9:39
 for a being Int-Location, I being Macro-Instruction holds
     while>0(a,I).insloc (card I +5) = halt SCM+FSA;

theorem :: SCMFSA_9:40
 for a being Int-Location, I being Macro-Instruction holds
     while>0(a,I).insloc 3 = goto insloc (card I +5);

theorem :: SCMFSA_9:41
 for a being Int-Location, I being Macro-Instruction holds
     while>0(a,I).insloc 2 = goto insloc 3;

theorem :: SCMFSA_9:42
   for a being Int-Location, I being Macro-Instruction,k being Nat st
 k < card I +6 holds insloc k in dom while>0(a,I);

theorem :: SCMFSA_9:43
 for s being State of SCM+FSA, I being Macro-Instruction,
 a being read-write Int-Location
 st s.a <= 0 holds
     while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s;

theorem :: SCMFSA_9:44
 for a being Int-Location, I being Macro-Instruction,
 s being State of SCM+FSA,k being Nat st
   I is_closed_on s & I is_halting_on s &
   k < LifeSpan (s +* (I +* Start-At insloc 0)) &
   IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k) =
   IC (Computation (s +* ( I +* Start-At insloc 0))).k + 4 &
   (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k) | D =
   (Computation (s +* ( I +* Start-At insloc 0))).k | D
  holds
   IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k+1) =
   IC (Computation (s +* (I +* Start-At insloc 0))).(k+1) + 4 &
   (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k+1) | D =
   (Computation (s +* (I +* Start-At insloc 0))).(k+1) | D;

theorem :: SCMFSA_9:45
 for a being Int-Location, I being Macro-Instruction,
  s being State of SCM+FSA st
   I is_closed_on s & I is_halting_on s &
   IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 +
   LifeSpan (s +* (I +* Start-At insloc 0 ) ) ) =
   IC (Computation (s +* ( I +* Start-At insloc 0))).
   LifeSpan (s +* (I +* Start-At insloc 0 ) ) + 4
   holds
   CurInstr (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 +
   LifeSpan (s +* (I +* Start-At insloc 0)) ) = goto insloc (card I +4);

theorem :: SCMFSA_9:46
 for a being Int-Location, I being Macro-Instruction holds
     while>0(a,I).insloc (card I +4) = goto insloc 0;

theorem :: SCMFSA_9:47
 for s being State of SCM+FSA, I being Macro-Instruction,
 a being read-write Int-Location
 st I is_closed_on s & I is_halting_on s & s.a >0 holds
    IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).
    (LifeSpan (s +* (I +* Start-At insloc 0)) + 3) = insloc 0 &
    for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) + 3
    holds IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).k
    in dom while>0(a,I);

reserve s for State of SCM+FSA,
   I for Macro-Instruction,
   a for read-write Int-Location;

definition
 let s,I,a;
 func StepWhile>0(a,I,s) -> Function of NAT,product the Object-Kind of SCM+FSA
  means
:: SCMFSA_9:def 5
   it.0 = s & for i being Nat holds
    it.(i+1)=(Computation (it.i +* (while>0(a,I) +* sl0))).
      (LifeSpan (it.i +* (I +* sl0)) + 3);
end;

canceled 2;

theorem :: SCMFSA_9:50
 StepWhile>0(a,I,s).(k+1)=StepWhile>0(a,I,StepWhile>0(a,I,s).k).1;

theorem :: SCMFSA_9:51
  for I being Macro-Instruction,a being read-write Int-Location,
   s being State of SCM+FSA holds
   StepWhile>0(a,I,s).(0+1)=(Computation (s +* (while>0(a,I) +* sl0))).
   (LifeSpan (s+* (I +* sl0)) + 3);

theorem :: SCMFSA_9:52
  for I being Macro-Instruction,a being read-write Int-Location,
   s being State of SCM+FSA,k,n being Nat st
IC StepWhile>0(a,I,s).k =insloc 0 & StepWhile>0(a,I,s).k=
(Computation (s +* (while>0(a,I) +* Start-At insloc 0))).n holds
StepWhile>0(a,I,s).k = StepWhile>0(a,I,s).k +* (while>0(a,I)+*
Start-At insloc 0) &
StepWhile>0(a,I,s).(k+1)=(Computation (s +* (while>0(a,I) +*
Start-At insloc 0))).
(n +(LifeSpan (StepWhile>0(a,I,s).k +* (I +* Start-At insloc 0)) + 3));

theorem :: SCMFSA_9:53
  for I being Macro-Instruction,a being read-write Int-Location,
    s being State of SCM+FSA st (for k being Nat holds
     I is_closed_on StepWhile>0(a,I,s).k &
     I is_halting_on StepWhile>0(a,I,s).k) &
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for k being Nat holds (f.(StepWhile>0(a,I,s).(k+1)) <
      f.(StepWhile>0(a,I,s).k)
      or f.(StepWhile>0(a,I,s).k) = 0) &
      ( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 ) )
     holds
     while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s;

theorem :: SCMFSA_9:54
  for I being parahalting Macro-Instruction, a being read-write
    Int-Location, s being State of SCM+FSA st
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for k being Nat holds (f.(StepWhile>0(a,I,s).(k+1)) <
      f.(StepWhile>0(a,I,s).k) or f.(StepWhile>0(a,I,s).k) = 0) &
      ( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 ) )
     holds
     while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s;

theorem :: SCMFSA_9:55
    for I being parahalting Macro-Instruction, a being read-write
  Int-Location st
    ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for s being State of SCM+FSA holds (f.(StepWhile>0(a,I,s).1) < f.s
      or f.s = 0) & ( f.s =0 iff s.a <= 0 ))
     holds while>0(a,I) is parahalting;

definition
 let I,J be good Macro-Instruction,a be Int-Location;
 cluster if>0(a,I,J) -> good;
end;

definition
 let I be good Macro-Instruction,a be Int-Location;
 cluster while>0(a,I) -> good;
end;