:: On SCM+FSA Programs
:: by Andrzej Trybulec
::
:: Received May 19, 2013
:: Copyright (c) 2014-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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, XCMPLX_0, NAT_1, SCMFSA6A,
FUNCT_4, FUNCOP_1, XXREAL_0, RELSET_1, XREAL_0, VALUED_1, FINSET_1,
XBOOLE_0, COMPOS_0, SCMFSA_2, FUNCT_7, SCMFSA10, AMISTD_1, COMPOS_2,
CARD_3, FUNCT_1, INT_1, SCMFSA6B, SCMFSA6C, MEMSTR_0, AMISTD_2, EXTPRO_1,
STRUCT_0, AMI_3, SCMFSA_M;
requirements NUMERALS, BOOLE, 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;