:: On SCM+FSA Programs
::  by Andrzej Trybulec
::
:: Received May 19, 2013
:: Copyright (c) 2014-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SCMFSA_2, AMI_1, SCMFSA6A, ORDINAL4, AMI_3, SCMFSA8A, CARD_1,
      AMISTD_2, NAT_1, ARYTM_3, SUBSET_1, SCMFSA8B, AMISTD_1, SCMFSA_9,
      FUNCT_4, FUNCOP_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_1, NUMBERS, XXREAL_0,
      VALUED_1, RELOC, PARTFUN1, ARYTM_1, SCMFSA_7, COMPOS_1, SCMPDS_5,
      TURING_1, CARD_3, MEMSTR_0, STRUCT_0, GOBRD13, SCMPDS_4, AFINSQ_1;
 notations TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, PARTFUN1, FUNCOP_1,
      FUNCT_4, FUNCT_7, ORDINAL1, CARD_1, CARD_3, AFINSQ_1, NUMBERS, XXREAL_0,
      XCMPLX_0, NAT_1, NAT_D, XXREAL_2, VALUED_1, STRUCT_0, MEMSTR_0, COMPOS_0,
      AMISTD_1, EXTPRO_1, COMPOS_1, COMPOS_2, SCMFSA_1, SCMFSA_2, SCMFSA6A,
      SCMFSA8A;
 constructors SCMFSA_2, SCMFSA6A, SCMFSA_1, SCMFSA8A, XCMPLX_0, SUBSET_1,
      FUNCT_4, NAT_1, FUNCOP_1, CARD_3, DOMAIN_1, VALUED_1, PARTFUN1, FUNCT_7,
      AMISTD_1, PRE_POLY, SCMFSA10, COMPOS_2, XXREAL_2, RELSET_1, NAT_D,
      AMISTD_2;
 registrations CARD_1, ORDINAL1, AFINSQ_1, COMPOS_1, NAT_1, SCMFSA6A, FUNCT_4,
      FUNCOP_1, XXREAL_0, XREAL_0, VALUED_1, COMPOS_0, SCMFSA_2, FUNCT_7,
      SCMFSA10, AMISTD_1, COMPOS_2, CARD_3, FUNCT_1, MEMSTR_0, AMISTD_2,
      EXTPRO_1, STRUCT_0;
 requirements NUMERALS, SUBSET, ARITHM, REAL;


begin

definition let a be Int-Location, I be MacroInstruction of SCM+FSA;
 func if=0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 1
   a =0_goto  3 ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA;
end;

definition let a be Int-Location, I be MacroInstruction of SCM+FSA;
 func if>0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 2
   a >0_goto  3 ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA;
end;

theorem :: SCMFSA_X:1
  for I being MacroInstruction of SCM+FSA, a being Int-Location
   holds card if=0(a, I) = card I + 4;

theorem :: SCMFSA_X:2
  for I being MacroInstruction of SCM+FSA, a being Int-Location
   holds card if>0(a, I) = card I + 4;

definition
  let a be Int-Location;
  let I be MacroInstruction of SCM+FSA;
:: in these definitions 'Goto 0' is only a place holder
:: after relocation in changed to 'goto(card 3 + I)
:: and must be substituted by the real 'goto 0'
  func while=0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 3
  if=0(a, I ';' goto 0) +* (card I + 2, goto  0);
  func while>0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 4
  if>0(a, I ';' goto 0) +* (card I + 2, goto  0);
end;

theorem :: SCMFSA_X:3
  for I being MacroInstruction of SCM+FSA, a being Int-Location
  holds card while=0(a,I) = card I + 5;

theorem :: SCMFSA_X:4
  for I being MacroInstruction of SCM+FSA, a being Int-Location
  holds card while>0(a,I) = card I + 5;

theorem :: SCMFSA_X:5
  for a being Int-Location, I being MacroInstruction of SCM+FSA, k being Nat
  st k < 5 holds k in dom while=0(a,I);

theorem :: SCMFSA_X:6
  for a being Int-Location, I being MacroInstruction of SCM+FSA, k being Nat
  st k < 5 holds card I + k in dom while=0(a,I);

theorem :: SCMFSA_X:7
  for a being Int-Location, I being MacroInstruction of SCM+FSA, k being Nat
   st k < 5 holds  k in dom while>0(a,I);

theorem :: SCMFSA_X:8
  for a being Int-Location, I being MacroInstruction of SCM+FSA, k being Nat
   st k < 5 holds card I +k in dom while>0(a,I);

theorem :: SCMFSA_X:9
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
   1 in dom while=0(a,I) & 1 in dom while>0(a,I);

theorem :: SCMFSA_X:10
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while=0(a,I). 0 = a =0_goto  3 &
  while=0(a,I). 1 = goto 2 &
  while>0(a,I). 0 = a >0_goto  3 &
  while>0(a,I). 1 = goto  2;

theorem :: SCMFSA_X:11
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while=0(a,I).(card I +4) = halt SCM+FSA;

theorem :: SCMFSA_X:12
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while=0(a,I). 2 = goto  (card I +4);

::$CT

theorem :: SCMFSA_X:14
  for a being Int-Location, I being MacroInstruction of SCM+FSA,k being Nat
   st k < card I +5 holds  k in dom while=0(a,I);

theorem :: SCMFSA_X:15
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while=0(a,I). (card I + 2) = goto  0;

theorem :: SCMFSA_X:16
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while>0(a,I).(card I+4) = halt SCM+FSA;

theorem :: SCMFSA_X:17
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while>0(a,I).2 = goto  (card I +4);

::$CT

theorem :: SCMFSA_X:19
  for a being Int-Location, I being MacroInstruction of SCM+FSA, k being Nat
   st k < card I +5 holds  k in dom while>0(a,I);

theorem :: SCMFSA_X:20
  for a being Int-Location, I being MacroInstruction of SCM+FSA holds
  while>0(a,I). (card I + 2) = goto  0;

definition
  let a be Int-Location;
  let I be Program of SCM+FSA;
  func if<0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 5
  a =0_goto  (card I + 4) ";"
  (a >0_goto  (card I + 2) ";" I)
    ";" Stop SCM+FSA;
end;

theorem :: SCMFSA_X:21
  for I being Program of SCM+FSA, a being Int-Location holds card
  if<0(a,I) = card I + 5;

definition
  let a be Int-Location;
  let I be MacroInstruction of SCM+FSA;
  func while<0(a,I) -> Program of SCM+FSA equals
:: SCMFSA_X:def 6
   if<0(a,I ';' goto 0) +* (card I + 1, goto  0);
end;

theorem :: SCMFSA_X:22
  for I being MacroInstruction of SCM+FSA, a being Int-Location holds card
  while<0(a,I) = card I + 6;

theorem :: SCMFSA_X:23
 for I being MacroInstruction of SCM+FSA,
     i being No-StopCode Instruction of SCM+FSA,
     n being Nat st n + 1 < card I
  holds I +* (n,i) is MacroInstruction of SCM+FSA;

registration
 let I be MacroInstruction of SCM+FSA, a be Int-Location;
 cluster while=0(a,I) -> halt-ending unique-halt;
 cluster while>0(a,I) -> halt-ending unique-halt;
end;

begin :: Closedness

theorem :: SCMFSA_X:24
 for I being really-closed MacroInstruction of SCM+FSA,
     n,k being Nat st n < card I & k < card I
  holds I +* (n,goto k) is really-closed;

theorem :: SCMFSA_X:25
 for I being really-closed MacroInstruction of SCM+FSA
  holds I ';' goto 0 is really-closed;

theorem :: SCMFSA_X:26
for I being really-closed Program of SCM+FSA,
     k being Nat st k <= card I
  holds Macro goto k ';' I is really-closed;

theorem :: SCMFSA_X:27
 for I being really-closed MacroInstruction of SCM+FSA,
     k being Nat st k <= card I
  holds Goto k ";" I is really-closed;

theorem :: SCMFSA_X:28
 for I being really-closed Program of SCM+FSA
  holds Goto  (card I + 1) ";" I ";" Stop SCM+FSA
     is really-closed;

theorem :: SCMFSA_X:29
for I being really-closed MacroInstruction of SCM+FSA, a being Int-Location,
     k being Nat st k <= card I
  holds Macro(a=0_goto k) ';' I is really-closed;

theorem :: SCMFSA_X:30
for I being really-closed MacroInstruction of SCM+FSA, a being Int-Location,
     k being Nat st k <= card I
  holds Macro(a>0_goto k) ';' I is really-closed;

theorem :: SCMFSA_X:31
for I being really-closed MacroInstruction of SCM+FSA, a being Int-Location,
     k being Nat st k <= card I
  holds a=0_goto k ";" I is really-closed;

theorem :: SCMFSA_X:32
for I being really-closed MacroInstruction of SCM+FSA, a being Int-Location,
     k being Nat st k <= card I
  holds a>0_goto k ";" I is really-closed;

registration
 let I be really-closed MacroInstruction of SCM+FSA, a be Int-Location;
 cluster if=0(a,I) -> really-closed;
 cluster if>0(a,I) -> really-closed;
end;

registration
 let I be really-closed MacroInstruction of SCM+FSA, a be Int-Location;
 cluster while=0(a,I) -> really-closed;
 cluster while>0(a,I) -> really-closed;
end;

theorem :: SCMFSA_X:33
 for I,J,K being MacroInstruction of SCM+FSA holds
  I ";" J ';' K = I ";" (J ';' K);

theorem :: SCMFSA_X:34
 for I being MacroInstruction of SCM+FSA holds
 stop Directed I = I ";" Stop SCM+FSA;

theorem :: SCMFSA_X:35
 for I being MacroInstruction of SCM+FSA, a being Int-Location
 holds if=0(a,I ';' goto 0) =
  (a =0_goto  3 ";" Goto(card(I ';' goto 0) + 1))
      ";" I ';' goto 0 ";" Stop SCM+FSA;

theorem :: SCMFSA_X:36
 for I being MacroInstruction of SCM+FSA, a being Int-Location
 holds if>0(a,I ';' goto 0) =
  (a >0_goto  3 ";" Goto(card(I ';' goto 0) + 1))
      ";" I ';' goto 0 ";" Stop SCM+FSA;