:: On SCM+FSA Programs
:: by Andrzej Trybulec
::
:: Received May 19, 2013
:: Copyright (c) 2014-2026 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;
definitions COMPOS_1, AMISTD_1, TARSKI;
equalities SCMFSA6A, COMPOS_1, FUNCOP_1, VALUED_1, SCMFSA8A, AMISTD_1,
MEMSTR_0, COMPOS_2;
expansions COMPOS_1;
theorems AFINSQ_1, SCMFSA6A, SCMFSA8A, FUNCT_4, FUNCOP_1, ZFMISC_1, XREAL_1,
XXREAL_0, NAT_1, COMPOS_1, TARSKI, SCMFSA7B, COMPOS_0, VALUED_1,
PARTFUN1, XBOOLE_0, SCMFSA_4, FUNCT_7, AMISTD_1, SCMFSA10, MEMSTR_0,
ORDINAL1, SCMFSA_2, FUNCT_1, CARD_3, AMISTD_2, XREAL_0, COMPOS_2;
begin
definition let a be Int-Location, I be MacroInstruction of SCM+FSA;
func if=0(a,I) -> Program of SCM+FSA equals
a =0_goto 3 ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA;
correctness;
end;
definition let a be Int-Location, I be MacroInstruction of SCM+FSA;
func if>0(a,I) -> Program of SCM+FSA equals
a >0_goto 3 ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA;
correctness;
end;
Lm1: card Stop SCM+FSA = 1 by AFINSQ_1:34;
Lm2: (Stop SCM+FSA).0 = halt SCM+FSA;
Lm3: 0 in dom Stop SCM+FSA by COMPOS_1:3;
theorem Th1:
for I being MacroInstruction of SCM+FSA, a being Int-Location
holds card if=0(a, I) = card I + 4
proof
let I be MacroInstruction of SCM+FSA, a be Int-Location;
thus card if=0(a, I)
= card(a =0_goto 3 ";" Goto(card I + 1) ";" I) + 1 by Lm1,SCMFSA6A:21
.= card(a =0_goto 3 ";" Goto(card I + 1)) + card I + 1 by SCMFSA6A:21
.= 2 + card Goto(card I + 1) + card I + 1 by SCMFSA6A:33
.= 2 + 1 + card I + 1 by SCMFSA8A:15
.= card I + 4;
end;
theorem Th2:
for I being MacroInstruction of SCM+FSA, a being Int-Location
holds card if>0(a, I) = card I + 4
proof
let I be MacroInstruction of SCM+FSA, a be Int-Location;
thus card if>0(a, I)
= card(a >0_goto 3 ";" Goto(card I + 1) ";" I) + 1 by Lm1,SCMFSA6A:21
.= card(a >0_goto 3 ";" Goto(card I + 1)) + card I + 1 by SCMFSA6A:21
.= 2 + card Goto(card I + 1) + card I + 1 by SCMFSA6A:33
.= 2 + 1 + card I + 1 by SCMFSA8A:15
.= card I + 4;
end;
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
if=0(a, I ';' goto 0) +* (card I + 2, goto 0);
correctness;
func while>0(a,I) -> Program of SCM+FSA equals
if>0(a, I ';' goto 0) +* (card I + 2, goto 0);
correctness;
end;
theorem Th3:
for I being MacroInstruction of SCM+FSA, a being Int-Location
holds card while=0(a,I) = card I + 5
proof
let I be MacroInstruction of SCM+FSA, a be Int-Location;
thus card while=0(a,I) = card if=0(a,I ';' goto 0) by FUNCT_7:30
.= card(I ';' goto 0) + 4 by Th1
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
end;
theorem Th4:
for I being MacroInstruction of SCM+FSA, a being Int-Location
holds card while>0(a,I) = card I + 5
proof
let I be MacroInstruction of SCM+FSA, a be Int-Location;
thus card while>0(a,I) = card if>0(a,I ';' goto 0) by FUNCT_7:30
.= card(I ';' goto 0) + 4 by Th2
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
end;
theorem Th5:
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
A1: 5 <= card I + 5 by NAT_1:11;
A2: card while=0(a,I) = card I + 5 by Th3;
assume k < 5;
then k < card I + 5 by A1,XXREAL_0:2;
hence thesis by A2,AFINSQ_1:66;
end;
theorem Th6:
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
assume
A1: k < 5;
card while=0(a,I) = card I + 5 by Th3;
hence thesis by A1,AFINSQ_1:66,XREAL_1:6;
end;
theorem Th7:
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
A1: 5 <= card I + 5 by NAT_1:11;
A2: card while>0(a,I) = card I + 5 by Th4;
assume k < 5;
then k < card I + 5 by A1,XXREAL_0:2;
hence thesis by A2,AFINSQ_1:66;
end;
theorem Th8:
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
assume
A1: k < 5;
card while>0(a,I) = card I + 5 by Th4;
hence thesis by A1,AFINSQ_1:66,XREAL_1:6;
end;
theorem
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) by Th5,Th7;
theorem
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
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set i = a =0_goto 3;
A1: dom Macro i = { 0, 1} by COMPOS_1:61;
then
A2: 0 in dom Macro i by TARSKI:def 2;
A3: 1 in dom Macro i by A1,TARSKI:def 2;
A4: if=0(a, I1)
= i ";" Goto(card I1 + 1) ";" (I1 ";" Stop SCM+FSA) by SCMFSA6A:25
.= Macro i ";" ((Goto(card I1 + 1) ";" (I1 ";" Stop SCM+FSA)))
by SCMFSA6A:25;
A5: 1 <> card I + 2 by NAT_1:11;
thus while=0(a,I). 0 =if=0(a,I1). 0 by FUNCT_7:32
.= (Directed Macro i). 0 by A4,A2,SCMFSA8A:14
.= a =0_goto 3 by SCMFSA7B:1;
thus while=0(a,I). 1 =if=0(a,I1). 1 by FUNCT_7:32,A5
.= (Directed Macro i). 1 by A4,A3,SCMFSA8A:14
.= goto 2 by SCMFSA7B:2;
set i = a >0_goto 3;
A6: if>0(a, I1)
= i ";" Goto(card I1 + 1) ";" (I1 ";" Stop SCM+FSA) by SCMFSA6A:25
.= Macro i ";" ((Goto(card I1 + 1) ";" (I1 ";" Stop SCM+FSA)))
by SCMFSA6A:25;
A7: dom Macro i = { 0, 1} by COMPOS_1:61;
then
A8: 0 in dom Macro i by TARSKI:def 2;
A9: 1 in dom Macro i by A7,TARSKI:def 2;
thus while>0(a,I). 0 = if>0(a,I1 ). 0 by FUNCT_7:32
.= (Directed Macro i). 0 by A6,A8,SCMFSA8A:14
.= a >0_goto 3 by SCMFSA7B:1;
thus while>0(a,I). 1 = if>0(a,I1). 1 by FUNCT_7:32,A5
.= (Directed Macro i). 1 by A6,A9,SCMFSA8A:14
.= goto 2 by SCMFSA7B:2;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while=0(a,I).(card I +4) = halt SCM+FSA
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set i = a =0_goto 3;
set c5 = card I + 4;
A1: c5 = card I + 1 + 3
.= card I1 + 3 by COMPOS_2:11;
set Mi= Macro i ";" Goto (card I1 + 1) ";" I1;
0 + c5 in { il+c5 where il is Nat: il in dom J} by Lm3;
then
A2: c5 in dom Shift(J,c5) by VALUED_1:def 12;
then
A3: Shift(J,c5)/.c5 = Shift(J,c5).(0 +c5) by PARTFUN1:def 6
.= halt SCM+FSA by Lm2,Lm3,VALUED_1:def 12;
A4: c5 in dom while=0(a,I) & dom while=0(a,I) = dom if=0(a,I1)
by Th6,FUNCT_7:30;
card if=0(a, I1) = card Mi + card J by SCMFSA6A:21;
then
A5: card Mi = card if=0(a,I1)-card J
.= card I1 + 4 - 1 by Th1,Lm1
.= c5 by A1;
then
A6: not c5 in dom Mi;
dom if=0(a,I1) = dom Mi \/ dom Reloc(J, c5) by A5,SCMFSA6A:39;
then
A7: c5 in dom Reloc(J, c5) by A4,A6,XBOOLE_0:def 3;
A8: Reloc(J,c5) = IncAddr(Shift(J,c5),c5) by COMPOS_1:34;
A9: c5 <> card I + 2;
thus while=0(a,I).(card I + 4)
= (Mi ";" J).c5 by FUNCT_7:32,A9
.= (Reloc(J,c5)).c5 by A5,A7,SCMFSA6A:40
.= IncAddr( halt SCM+FSA, c5 ) by A2,A3,A8,COMPOS_1:def 21
.= halt SCM+FSA by COMPOS_0:4;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while=0(a,I). 2 = goto (card I +4)
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set i = a =0_goto 3;
set Mi=Macro i;
set G=Goto (card I1 + 1);
set J2= (I1 ";" Stop SCM+FSA);
set J1=G ";" J2;
A1: 0 in dom G by SCMFSA8A:31;
A2: G. 0 = goto (card I1 +1);
dom J1 = dom G \/ dom Reloc(J2, card G) by SCMFSA6A:39;
then
A3: 0 in dom J1 by A1,XBOOLE_0:def 3;
then 0 + 2 in { il+2 where il is Nat: il in dom J1};
then
A4: 2 in dom Shift(J1,2) by VALUED_1:def 12;
then
A5: Shift(J1,2)/.2 =Shift(J1,2).( 0 +2) by PARTFUN1:def 6
.=J1. 0 by A3,VALUED_1:def 12
.=(Directed G). 0 by SCMFSA8A:14,31
.=goto(card I1 + 1) by A1,A2,SCMFSA8A:16;
A6: card Mi = 2 by COMPOS_1:56;
then
A7: not 2 in dom Mi;
A8: 2 in dom while=0(a,I) & dom while=0(a,I) = dom if=0(a,I1)
by Th5,FUNCT_7:30;
A9: if=0(a, I1)
= i ";" Goto (card I1 + 1) ";" (I1 ";" Stop SCM+FSA) by SCMFSA6A:25
.= Mi ";" J1 by SCMFSA6A:25;
then
dom if=0(a,I1) = dom Mi \/ dom Reloc(J1, 2) by A6,SCMFSA6A:39;
then
A10: 2 in dom Reloc(J1, 2) by A8,A7,XBOOLE_0:def 3;
A11: Reloc(J1,2) = IncAddr(Shift(J1,2),2) by COMPOS_1:34;
0 + 2 <> card I + 2;
hence while=0(a,I). 2 = (Mi ";" J1).2 by A9,FUNCT_7:32
.= (Reloc(J1,2)). 2 by A10,SCMFSA6A:40,A6
.= IncAddr(goto (card I1 +1),2) by A4,A5,A11,COMPOS_1:def 21
.= goto (card I1 +1 + 2) by SCMFSA_4:1
.= goto (card I + 1 +1 + 2) by COMPOS_2:11
.= goto (card I+ 4);
end;
::$CT
theorem
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
assume
A1: k < card I +5;
card while=0(a,I) = card I + 5 by Th3;
hence thesis by A1,AFINSQ_1:66;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while=0(a,I). (card I + 2) = goto 0
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set Lc4= card I + 2;
Lc4 in dom while=0(a,I) & dom while=0(a,I) = dom if=0(a,I1)
by Th6,FUNCT_7:30;
hence while=0(a,I).Lc4 =goto 0 by FUNCT_7:31;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while>0(a,I).(card I+4) = halt SCM+FSA
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set i = a >0_goto 3;
set c5 = card I + 4;
set Mi= Macro i ";" Goto (card I1 + 1) ";" I1;
0 + c5 in { il+c5 where il is Nat: il in dom J} by Lm3;
then
A1: c5 in dom Shift(J,c5) by VALUED_1:def 12;
then
A2: Shift(J,c5)/.c5 = Shift(J,c5).( 0 +c5) by PARTFUN1:def 6
.= halt SCM+FSA by Lm2,Lm3,VALUED_1:def 12;
A3: c5 in dom while>0(a,I) & dom while>0(a,I) = dom if>0(a,I1)
by Th8,FUNCT_7:30;
card if>0(a, I1) = card Mi + card J by SCMFSA6A:21;
then
A4: card Mi = card if>0(a,I1)-card J
.= card I1 + 4 - 1 by Th2,Lm1
.= card I + 1 + 4 - 1 by COMPOS_2:11
.= c5;
then
A5: not c5 in dom Mi;
dom if>0(a,I1) = dom Mi \/ dom Reloc(J, c5) by A4,SCMFSA6A:39;
then
A6: c5 in dom Reloc(J, c5) by A3,A5,XBOOLE_0:def 3;
A7: Reloc(J,c5) = IncAddr(Shift(J,c5),c5) by COMPOS_1:34;
c5 <> card I + 2;
hence while>0(a,I).c5 = (Mi ";" J).c5 by FUNCT_7:32
.= (Reloc(J,c5)).c5 by A6,SCMFSA6A:40,A4
.= IncAddr( halt SCM+FSA, c5 ) by A1,A2,A7,COMPOS_1:def 21
.= halt SCM+FSA by COMPOS_0:4;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while>0(a,I).2 = goto (card I +4)
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set i = a >0_goto 3;
set Mi=Macro i;
set G=Goto(card I1+1);
set J2= I1 ";" Stop SCM+FSA;
set J1=G ";" J2;
A1: 0 in dom G by SCMFSA8A:31;
A2: G. 0 = goto (card I1+1);
dom J1 = dom G \/ dom Reloc(J2, card G) by SCMFSA6A:39;
then
A3: 0 in dom J1 by A1,XBOOLE_0:def 3;
then 0 + 2 in { il+2 where il is Nat: il in dom J1};
then
A4: 2 in dom Shift(J1,2) by VALUED_1:def 12;
then
A5: Shift(J1,2)/.2 =Shift(J1,2).( 0 +2) by PARTFUN1:def 6
.=J1. 0 by A3,VALUED_1:def 12
.=(Directed G). 0 by A1,SCMFSA8A:14
.=goto (card I1 + 1) by A1,A2,SCMFSA8A:16;
A6: card Mi = 2 by COMPOS_1:56;
then
A7: not 2 in dom Mi;
A8: 2 in dom while>0(a,I) & dom while>0(a,I) = dom if>0(a,I1)
by Th7,FUNCT_7:30;
A9: if>0(a, I1)
= i ";" Goto (card I1 + 1) ";" (I1 ";" Stop SCM+FSA) by SCMFSA6A:25
.= Mi ";" J1 by SCMFSA6A:25;
then
dom if>0(a,I1) = dom Mi \/ dom Reloc(J1, 2) by SCMFSA6A:39,A6;
then
A10: 2 in dom Reloc(J1, 2) by A8,A7,XBOOLE_0:def 3;
A11: Reloc(J1,2) = IncAddr(Shift(J1,2),2) by COMPOS_1:34;
0+2 <> card I + 2;
hence while>0(a,I).2 = (Mi ";" J1).2 by A9,FUNCT_7:32
.= (Reloc(J1,2)).2 by A10,SCMFSA6A:40,A6
.= IncAddr(goto (card I1 +1),2) by A4,A5,A11,COMPOS_1:def 21
.= goto (card I1+ 1 +2) by SCMFSA_4:1
.= goto (card I+1+ 1 +2) by COMPOS_2:11
.= goto (card I+ 4);
end;
::$CT
theorem
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)
proof
let a be Int-Location, I be MacroInstruction of SCM+FSA,k be Nat;
assume
A1: k < card I +5;
card while>0(a,I) = card I + 5 by Th4;
hence thesis by A1,AFINSQ_1:66;
end;
theorem
for a being Int-Location, I being MacroInstruction of SCM+FSA holds
while>0(a,I). (card I + 2) = goto 0
proof
set J = Stop SCM+FSA;
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
set I1= I ';' goto 0;
set Lc4= card I + 2;
Lc4 in dom while>0(a,I) & dom while>0(a,I) = dom if>0(a,I1)
by Th8,FUNCT_7:30;
hence while>0(a,I).Lc4 = goto 0 by FUNCT_7:31;
end;
definition
let a be Int-Location;
let I be Program of SCM+FSA;
func if<0(a,I) -> Program of SCM+FSA equals
a =0_goto (card I + 4) ";"
(a >0_goto (card I + 2) ";" I)
";" Stop SCM+FSA;
coherence;
end;
theorem Th19:
for I being Program of SCM+FSA, a being Int-Location holds card
if<0(a,I) = card I + 5
proof
let I be Program of SCM+FSA, a be Int-Location;
thus card if<0(a,I)
= card (a =0_goto (card I + 4) ";"
(a >0_goto (card I + 2) ";" I)) + 1 by Lm1,SCMFSA6A:21
.= 2 + card(a >0_goto (card I + 2)";" I) + 1 by SCMFSA6A:33
.= 2 + (card I + 2) + 1 by SCMFSA6A:33
.= card I + 5;
end;
definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
func while<0(a,I) -> Program of SCM+FSA equals
if<0(a,I ';' goto 0) +* (card I + 1, goto 0);
correctness;
end;
theorem
for I being MacroInstruction of SCM+FSA, a being Int-Location holds card
while<0(a,I) = card I + 6
proof
let I be MacroInstruction of SCM+FSA, a be Int-Location;
thus card while<0(a,I) = card if<0(a,I ';' goto 0) by FUNCT_7:30
.= card(I ';' goto 0) + 5 by Th19
.= card I +1+5 by COMPOS_2:11
.= card I + 6;
end;
theorem Th21:
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
proof let I be MacroInstruction of SCM+FSA,
i be No-StopCode Instruction of SCM+FSA,
n be Nat such that
A1: n + 1 < card I;
set F = I +*(n,i);
A2: dom F = dom I by FUNCT_7:30;
then
A3: LastLoc F = LastLoc I;
A4: n + 1 < card F by A1,A2;
A5: card F >= 0+1 by NAT_1:13;
LastLoc F = card F -' 1 by AFINSQ_1:70
.= card F - 1 by A5,XREAL_1:233;
then n + 1 - 1 < LastLoc F by A4,XREAL_1:14;
then n < LastLoc I by A3;
then F.LastLoc F = I.LastLoc I by A3,FUNCT_7:32
.= halt SCM+FSA by COMPOS_1:def 14;
then
A6: F is halt-ending;
F is unique-halt
proof let f be Nat such that
A7: F.f = halt SCM+FSA and
A8: f in dom F;
now assume
A9: I.f <> halt SCM+FSA;
per cases;
suppose f = n;
then F.f = i by FUNCT_7:31,A8,A2;
hence contradiction by A7,COMPOS_0:def 12;
end;
suppose f <> n;
then F.f = I.f
by FUNCT_7:32;
hence contradiction by A9,A7;
end;
end;
hence f = LastLoc F by A2,A8,A3,COMPOS_1:def 15;
end;
hence thesis by A6;
end;
registration
let I be MacroInstruction of SCM+FSA, a be Int-Location;
cluster while=0(a,I) -> halt-ending unique-halt;
coherence
proof set W = if=0(a, I ';' goto 0);
card W = card(I ';' goto 0) + 4 by Th1
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
then card I + 3 < card W by XREAL_1:8;
then card I + 2 + 1 < card W;
hence thesis by Th21;
end;
cluster while>0(a,I) -> halt-ending unique-halt;
coherence
proof set W = if>0(a, I ';' goto 0);
card W = card(I ';' goto 0) + 4 by Th2
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
then card I + 3 < card W by XREAL_1:8;
then card I + 2 + 1 < card W;
hence thesis by Th21;
end;
end;
begin :: Closedness
theorem Th22:
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
proof let I being really-closed MacroInstruction of SCM+FSA,
n,k being Nat such that
A1: n < card I and
A2: k < card I;
set F = I +* (n,goto k);
A3: n in dom I by A1,AFINSQ_1:66;
A4: k in dom I by A2,AFINSQ_1:66;
A5: dom F = dom I by FUNCT_7:30;
let l be Nat such that
A6: l in dom F;
A7: F/.l = F.l by A6,PARTFUN1:def 6;
per cases;
suppose n = l;
then F.l = goto k by A3,FUNCT_7:31;
then NIC (F/.l, l) = {k} by A7,SCMFSA10:33;
hence NIC (F/.l, l) c= dom F by A5,ZFMISC_1:31,A4;
end;
suppose n <> l;
then F.l = I.l by FUNCT_7:32;
then F/.l = I.l by A6,PARTFUN1:def 6
.= I/.l by A6,A5,PARTFUN1:def 6;
hence NIC (F/.l, l) c= dom F by A5,A6,AMISTD_1:def 9;
end;
end;
theorem Th23:
for I being really-closed MacroInstruction of SCM+FSA
holds I ';' goto 0 is really-closed
proof let I be really-closed MacroInstruction of SCM+FSA;
A1: dom Macro goto 0 = { 0,1 } by COMPOS_1:61;
A2: 1 in dom Macro goto 0 & 0 in dom Macro goto 0 by COMPOS_1:60;
set F = Macro goto 0;
Macro goto 0 is really-closed
proof let l be Nat;
assume
A3: l in dom F;
then per cases by A1,TARSKI:def 2;
suppose
A4: l = 0;
then F/.l = F.l by A2,PARTFUN1:def 6
.= goto 0 by A4,COMPOS_1:58;
then NIC(F/.l,l) = {0} by SCMFSA10:33;
hence NIC(F/.l, l) c= dom F by A2,ZFMISC_1:31;
end;
suppose
A5: l = 1;
then F/.l = F.l by A2,PARTFUN1:def 6
.= halt SCM+FSA by A5,COMPOS_1:59;
then NIC(F/.l,l) = {l} by AMISTD_1:2;
hence NIC(F/.l, l) c= dom F by A3,ZFMISC_1:31;
end;
end;
then I ';' Macro goto 0 is really-closed;
hence I ';' goto 0 is really-closed;
end;
theorem Th24:
for I being really-closed Program of SCM+FSA,
k being Nat st k <= card I
holds Macro goto k ';' I is really-closed
proof let I be really-closed Program of SCM+FSA, l being Nat;
assume
A1: l <= card I;
set F = Macro goto l; set G = I; set S = SCM+FSA;
set P = F ';' I, k = card F -' 1;
let f be Nat such that
A2: f in dom P;
A3: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A4: dom Reloc(G,k) = {(m+k) where m is Nat: m in dom IncAddr(G,k)}
by VALUED_1:def 12;
let x be object;
assume x in NIC(P/.f,f);
then consider s2 being Element of product the_Values_of S
such that
A5: x = IC Exec(P/.f,s2) and
A6: IC s2 = f;
A7: P/.f = P.f by A2,PARTFUN1:def 6;
per cases by A2,A3,XBOOLE_0:def 3;
suppose
A8: f in dom CutLastLoc F;
then
A9: f < card CutLastLoc F by AFINSQ_1:66;
card CutLastLoc F = card F - 1 by VALUED_1:38
.= 2 - 1 by COMPOS_1:56;
then
A10: f = 0 by A9,NAT_1:14;
dom CutLastLoc F misses dom Reloc(G,card F -' 1) by COMPOS_1:18;
then
A11: not f in dom Reloc(G,k) by A8,XBOOLE_0:3;
P/.f = (CutLastLoc F).0 by A10,FUNCT_4:11,A11,A7
.= goto l;
then
A12: x = l by SCMFSA_2:69,A5;
card P = card F + card I - 1 by COMPOS_1:20
.= 2 + card I - 1 by COMPOS_1:56
.= card I + 1;
then card I < card P by XREAL_1:29;
then l < card P by A1,XXREAL_0:2;
hence x in dom P by AFINSQ_1:66,A12;
end;
suppose
A13: f in dom Reloc(G,k);
then consider m being Nat such that
A14: f = m+k and
A15: m in dom IncAddr(G,k) by A4;
A16: m in dom G by A15,COMPOS_1:def 21;
then
A17: NIC(G/.m,m) c= dom G by AMISTD_1:def 9;
A18: Values IC S = NAT by MEMSTR_0:def 6;
reconsider m as Element of NAT by ORDINAL1:def 12;
reconsider v = IC S .--> m as PartState of S by A18;
set s1 = s2 +* v;
A19: P/.f = Reloc(G,k).f by A7,A13,FUNCT_4:13
.= IncAddr(G,k).m by A14,A15,VALUED_1:def 12;
A20: (IC S .--> m).IC S = m by FUNCOP_1:72;
A21: IC S in {IC S} by TARSKI:def 1;
A22: dom (IC S .--> m) = {IC S};
reconsider w = IC S .--> (IC s1 + k) as PartState of S by A18;
A23: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by PARTFUN1:def 2;
A24: dom s2 = the carrier of S by PARTFUN1:def 2;
for a being object st a in dom s2 holds
s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
proof
let a be object such that a in dom s2;
A25: dom (IC S .--> (IC s1 + k)) = {IC S};
per cases;
suppose
A26: a = IC S;
hence s2.a = IC s1 + k by A6,A14,A22,A20,A21,FUNCT_4:13
.= (IC S .--> (IC s1 + k)).a by A26,FUNCOP_1:72
.= (s1 +* (IC S .--> (IC s1 + k))).a by A21,A25,A26,FUNCT_4:13;
end;
suppose
A27: a <> IC S;
then
A28: not a in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
not a in dom (IC S .--> m) by A27,TARSKI:def 1;
then s1.a = s2.a by FUNCT_4:11;
hence thesis by A28,FUNCT_4:11;
end;
end;
then
A29: s2 = IncIC(s1,k) by A23,A24,FUNCT_1:2;
set s3 = s1;
A30: IC s3 = m by A20,A21,A22,FUNCT_4:13;
reconsider s3 as Element of product the_Values_of S by CARD_3:107;
reconsider k,m as Element of NAT;
A31: x = IC Exec(IncAddr(G/.m,k),s2) by A5,A16,A19,COMPOS_1:def 21
.= IC Exec(G/.m, s3) + k by A29,AMISTD_2:7;
IC Exec(G/.m, s3) in NIC(G/.m,m) by A30;
then IC Exec(G/.m, s3) in dom G by A17;
then IC Exec(G/.m, s3) in dom IncAddr(G,k) by COMPOS_1:def 21;
then x in dom Reloc(G,k) by A4,A31;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
theorem Th25:
for I being really-closed MacroInstruction of SCM+FSA,
k being Nat st k <= card I
holds Goto k ";" I is really-closed
proof let I be really-closed MacroInstruction of SCM+FSA, k being Nat;
Goto k ";" I = Macro(goto k) ';' I by SCMFSA8A:43;
hence thesis by Th24;
end;
theorem Th26:
for I being really-closed Program of SCM+FSA
holds Goto (card I + 1) ";" I ";" Stop SCM+FSA
is really-closed
proof let I be really-closed Program of SCM+FSA;
A1: card(I ";" Stop SCM+FSA)= card I + card Stop SCM+FSA by SCMFSA6A:21
.= card I +1 by COMPOS_1:4;
Goto(card I + 1) ";" I ";" Stop SCM+FSA
= Goto(card I + 1) ";" (I ";" Stop SCM+FSA) by SCMFSA6A:25;
hence thesis by Th25,A1;
end;
theorem Th27:
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
proof let I be really-closed MacroInstruction of SCM+FSA,
a be Int-Location, l being Nat;
assume
A1: l <= card I;
set F = Macro(a=0_goto l); set G = I; set S = SCM+FSA;
set P = F ';' I, k = card F -' 1;
let f be Nat such that
A2: f in dom P;
A3: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A4: dom Reloc(G,k) = {(m+k) where m is Nat: m in dom IncAddr(G,k)}
by VALUED_1:def 12;
let x be object;
assume x in NIC(P/.f,f);
then consider s2 being Element of product the_Values_of S
such that
A5: x = IC Exec(P/.f,s2) and
A6: IC s2 = f;
A7: P/.f = P.f by A2,PARTFUN1:def 6;
per cases by A2,A3,XBOOLE_0:def 3;
suppose
A8: f in dom CutLastLoc F;
then
A9: f < card CutLastLoc F by AFINSQ_1:66;
card CutLastLoc F = card F - 1 by VALUED_1:38
.= 2 - 1 by COMPOS_1:56;
then
A10: f = 0 by A9,NAT_1:14;
dom CutLastLoc F misses dom Reloc(G,card F -' 1) by COMPOS_1:18;
then
A11: not f in dom Reloc(G,k) by A8,XBOOLE_0:3;
P/.f = (CutLastLoc F).0 by A10,FUNCT_4:11,A11,A7
.= a=0_goto l;
then
A12: x = IC Exec(a=0_goto l,s2) by A5;
s2.a = 0 or s2.a <> 0;
then x = l or x = IC s2 + 1 by SCMFSA_2:70,A12;
then per cases;
suppose
A13: x = l;
card P = card F + card I - 1 by COMPOS_1:20
.= 2 + card I - 1 by COMPOS_1:56
.= card I + 1;
then card I < card P by XREAL_1:29;
then l < card P by A1,XXREAL_0:2;
hence x in dom P by AFINSQ_1:66,A13;
end;
suppose x = IC s2 + 1;
then
A14: x = f + 1 by A6;
f < card F - 1 by A9,VALUED_1:38;
then f + 1 < card F by XREAL_1:20;
then
A15: x in dom F by A14,AFINSQ_1:66;
dom F c= dom P by COMPOS_1:21;
hence thesis by A15;
end;
end;
suppose
A16: f in dom Reloc(G,k);
then consider m being Nat such that
A17: f = m+k and
A18: m in dom IncAddr(G,k) by A4;
A19: m in dom G by A18,COMPOS_1:def 21;
then
A20: NIC(G/.m,m) c= dom G by AMISTD_1:def 9;
A21: Values IC S = NAT by MEMSTR_0:def 6;
reconsider m as Element of NAT by ORDINAL1:def 12;
reconsider v = IC S .--> m as PartState of S by A21;
set s1 = s2 +* v;
A22: P/.f = Reloc(G,k).f by A7,A16,FUNCT_4:13
.= IncAddr(G,k).m by A17,A18,VALUED_1:def 12;
A23: (IC S .--> m).IC S = m by FUNCOP_1:72;
A24: IC S in {IC S} by TARSKI:def 1;
A25: dom (IC S .--> m) = {IC S};
reconsider w = IC S .--> (IC s1 + k) as PartState of S by A21;
A26: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by PARTFUN1:def 2;
A27: dom s2 = the carrier of S by PARTFUN1:def 2;
for a being object st a in dom s2 holds
s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
proof
let a be object such that a in dom s2;
A28: dom (IC S .--> (IC s1 + k)) = {IC S};
per cases;
suppose
A29: a = IC S;
hence s2.a = IC s1 + k by A6,A17,A25,A23,A24,FUNCT_4:13
.= (IC S .--> (IC s1 + k)).a by A29,FUNCOP_1:72
.= (s1 +* (IC S .--> (IC s1 + k))).a by A24,A28,A29,FUNCT_4:13;
end;
suppose
A30: a <> IC S;
then
A31: not a in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
not a in dom (IC S .--> m) by A30,TARSKI:def 1;
then s1.a = s2.a by FUNCT_4:11;
hence thesis by A31,FUNCT_4:11;
end;
end;
then
A32: s2 = IncIC(s1,k) by A26,A27,FUNCT_1:2;
set s3 = s1;
A33: IC s3 = m by A23,A24,A25,FUNCT_4:13;
reconsider s3 as Element of product the_Values_of S by CARD_3:107;
reconsider k,m as Element of NAT;
A34: x = IC Exec(IncAddr(G/.m,k),s2) by A5,A19,A22,COMPOS_1:def 21
.= IC Exec(G/.m, s3) + k by A32,AMISTD_2:7;
IC Exec(G/.m, s3) in NIC(G/.m,m) by A33;
then IC Exec(G/.m, s3) in dom G by A20;
then IC Exec(G/.m, s3) in dom IncAddr(G,k) by COMPOS_1:def 21;
then x in dom Reloc(G,k) by A4,A34;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
Lm4:
for i being No-StopCode Instruction of SCM+FSA holds
Directed Macro i = Macro i ';' Goto 1
proof let i be No-StopCode Instruction of SCM+FSA;
set A = { i, halt SCM+FSA };
A1: card Macro i = 2 by COMPOS_1:56;
then card Macro i - 1 = 1;
then
A2: card Macro i -' 1 = 1 by XREAL_0:def 2;
A3: card Load i = 1 by AFINSQ_1:34;
A4: i <> halt SCM+FSA by COMPOS_0:def 12;
rng Load i = {i} by AFINSQ_1:33;
then not halt SCM+FSA in rng Load i by TARSKI:def 1,A4;
then
A5: (Load i) +~ (halt SCM+FSA,goto 2) = CutLastLoc Macro i by FUNCT_4:103;
A6: Shift(Stop SCM+FSA,1) +~ (halt SCM+FSA,goto 2)
= Shift((Stop SCM+FSA) +~ (halt SCM+FSA,goto 2),1) by VALUED_1:67
.= Shift(<%goto(1+1)%>,1) by AFINSQ_1:90
.= Reloc(Goto 1,1) by SCMFSA8A:44;
thus Directed Macro i
= (Load i +* Shift(Stop SCM+FSA,1)) +~ (halt SCM+FSA,goto 2)
by A3,AFINSQ_1:77,A1
.= Macro i ';' Goto 1 by A5,A6,A2,FUNCT_7:117;
end;
Lm5:
for I being Program of SCM+FSA, k be Nat holds
stop(I ';' Goto k) = I ';' Macro(goto k)
proof let I be Program of SCM+FSA, k be Nat;
A1: IncAddr(Macro(goto k),card I -' 1)
= IncAddr(Goto k,card I -' 1) ^ Stop SCM+FSA by COMPOS_1:76;
thus stop(I ';' Goto k)
= ((CutLastLoc I) ^ IncAddr(Goto k,card I -' 1)) ^ Stop SCM+FSA
by COMPOS_1:75
.= (CutLastLoc I) ^ IncAddr(Macro(goto k),card I -' 1) by A1,AFINSQ_1:27
.= I ';' Macro(goto k) by COMPOS_1:75;
end;
theorem Th28:
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
proof let I be really-closed MacroInstruction of SCM+FSA,
a be Int-Location, l being Nat;
assume
A1: l <= card I;
set F = Macro(a>0_goto l); set G = I; set S = SCM+FSA;
set P = F ';' I, k = card F -' 1;
let f be Nat such that
A2: f in dom P;
A3: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A4: dom Reloc(G,k) = {(m+k) where m is Nat: m in dom IncAddr(G,k)}
by VALUED_1:def 12;
let x be object;
assume x in NIC(P/.f,f);
then consider s2 being Element of product the_Values_of S
such that
A5: x = IC Exec(P/.f,s2) and
A6: IC s2 = f;
A7: P/.f = P.f by A2,PARTFUN1:def 6;
per cases by A2,A3,XBOOLE_0:def 3;
suppose
A8: f in dom CutLastLoc F;
then
A9: f < card CutLastLoc F by AFINSQ_1:66;
card CutLastLoc F = card F - 1 by VALUED_1:38
.= 2 - 1 by COMPOS_1:56;
then
A10: f = 0 by A9,NAT_1:14;
dom CutLastLoc F misses dom Reloc(G,card F -' 1) by COMPOS_1:18;
then
A11: not f in dom Reloc(G,k) by A8,XBOOLE_0:3;
P/.f = (CutLastLoc F).0 by A10,FUNCT_4:11,A11,A7
.= a>0_goto l;
then
A12: x = IC Exec(a>0_goto l,s2) by A5;
s2.a = 0 or s2.a <> 0;
then x = l or x = IC s2 + 1 by SCMFSA_2:71,A12;
then per cases;
suppose
A13: x = l;
card P = card F + card I - 1 by COMPOS_1:20
.= 2 + card I - 1 by COMPOS_1:56
.= card I + 1;
then card I < card P by XREAL_1:29;
then l < card P by A1,XXREAL_0:2;
hence x in dom P by AFINSQ_1:66,A13;
end;
suppose x = IC s2 + 1;
then
A14: x = f + 1 by A6;
f < card F - 1 by A9,VALUED_1:38;
then f + 1 < card F by XREAL_1:20;
then
A15: x in dom F by A14,AFINSQ_1:66;
dom F c= dom P by COMPOS_1:21;
hence thesis by A15;
end;
end;
suppose
A16: f in dom Reloc(G,k);
then consider m being Nat such that
A17: f = m+k and
A18: m in dom IncAddr(G,k) by A4;
A19: m in dom G by A18,COMPOS_1:def 21;
then
A20: NIC(G/.m,m) c= dom G by AMISTD_1:def 9;
A21: Values IC S = NAT by MEMSTR_0:def 6;
reconsider m as Element of NAT by ORDINAL1:def 12;
reconsider v = IC S .--> m as PartState of S by A21;
set s1 = s2 +* v;
A22: P/.f = Reloc(G,k).f by A7,A16,FUNCT_4:13
.= IncAddr(G,k).m by A17,A18,VALUED_1:def 12;
A23: (IC S .--> m).IC S = m by FUNCOP_1:72;
A24: IC S in {IC S} by TARSKI:def 1;
A25: dom (IC S .--> m) = {IC S};
reconsider w = IC S .--> (IC s1 + k) as PartState of S by A21;
A26: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by PARTFUN1:def 2;
A27: dom s2 = the carrier of S by PARTFUN1:def 2;
for a being object st a in dom s2 holds
s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
proof
let a be object such that a in dom s2;
A28: dom (IC S .--> (IC s1 + k)) = {IC S};
per cases;
suppose
A29: a = IC S;
hence s2.a = IC s1 + k by A6,A17,A25,A23,A24,FUNCT_4:13
.= (IC S .--> (IC s1 + k)).a by A29,FUNCOP_1:72
.= (s1 +* (IC S .--> (IC s1 + k))).a by A24,A28,A29,FUNCT_4:13;
end;
suppose
A30: a <> IC S;
then
A31: not a in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
not a in dom (IC S .--> m) by A30,TARSKI:def 1;
then s1.a = s2.a by FUNCT_4:11;
hence thesis by A31,FUNCT_4:11;
end;
end;
then
A32: s2 = IncIC(s1,k) by A26,A27,FUNCT_1:2;
set s3 = s1;
A33: IC s3 = m by A23,A24,A25,FUNCT_4:13;
reconsider s3 as Element of product the_Values_of S by CARD_3:107;
reconsider k,m as Element of NAT;
A34: x = IC Exec(IncAddr(G/.m,k),s2) by A5,A19,A22,COMPOS_1:def 21
.= IC Exec(G/.m, s3) + k by A32,AMISTD_2:7;
IC Exec(G/.m, s3) in NIC(G/.m,m) by A33;
then IC Exec(G/.m, s3) in dom G by A20;
then IC Exec(G/.m, s3) in dom IncAddr(G,k) by COMPOS_1:def 21;
then x in dom Reloc(G,k) by A4,A34;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
theorem Th29:
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
proof let I be really-closed MacroInstruction of SCM+FSA, a being Int-Location,
k being Nat such that
A1: k <= card I;
A2: a=0_goto k ";" I
= stop(Macro(a=0_goto k) ';' Goto 1) ';' I by Lm4
.= Macro(a=0_goto k) ';' Macro(goto 1) ';' I by Lm5
.= Macro(a=0_goto k) ';' (Macro(goto 1) ';' I) by COMPOS_1:29;
A3: card(Macro(goto 1) ';' I) = card Macro(goto 1) + card I - 1 by COMPOS_1:20
.= 2 + card I - 1 by COMPOS_1:56;
card I <= card I + 1 by NAT_1:11;
then
A4: k <= card(Macro(goto 1) ';' I) by A3,A1,XXREAL_0:2;
0+1 <= card I by NAT_1:13;
then Macro(goto 1) ';' I is really-closed by Th24;
hence a=0_goto k ";" I is really-closed by A4,A2,Th27;
end;
theorem Th30:
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
proof let I be really-closed MacroInstruction of SCM+FSA, a being Int-Location,
k being Nat such that
A1: k <= card I;
A2: a>0_goto k ";" I = stop(Macro(a>0_goto k) ';' Goto 1) ';' I by Lm4
.= Macro(a>0_goto k) ';' Macro(goto 1) ';' I by Lm5
.= Macro(a>0_goto k) ';' (Macro(goto 1) ';' I) by COMPOS_1:29;
A3: card(Macro(goto 1) ';' I) = card Macro(goto 1) + card I - 1 by COMPOS_1:20
.= 2 + card I - 1 by COMPOS_1:56;
card I <= card I + 1 by NAT_1:11;
then
A4: k <= card(Macro(goto 1) ';' I) by A3,A1,XXREAL_0:2;
0+1 <= card I by NAT_1:13;
then Macro(goto 1) ';' I is really-closed by Th24;
hence a>0_goto k ";" I is really-closed by A4,A2,Th28;
end;
registration
let I be really-closed MacroInstruction of SCM+FSA, a be Int-Location;
cluster if=0(a,I) -> really-closed;
coherence
proof
A1: if=0(a,I)
= a =0_goto 3 ";" Goto(card I + 1) ";" (I ";" Stop SCM+FSA)
by SCMFSA6A:25
.= a =0_goto 3 ";" (Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a =0_goto 3 ";" (Goto(card I + 1) ";" I ";" Stop SCM+FSA)
by SCMFSA6A:25;
A2: card(Goto(card I + 1) ";" I ";" Stop SCM+FSA)
= card(Goto(card I + 1) ";" I) + 1 by Lm1,SCMFSA6A:21
.= card(Goto(card I + 1) ";" I) + 1
.= card Goto(card I + 1) + card I + 1 by SCMFSA6A:21
.= 1 + card I + 1 by SCMFSA8A:15
.= card I + 2;
0+ 1 <= card I by NAT_1:13;
then
A3: 1 + 2 <= card I + 2 by XREAL_1:7;
Goto(card I + 1) ";" I ";" Stop SCM+FSA is really-closed by Th26;
hence thesis by A3,Th29,A1,A2;
end;
cluster if>0(a,I) -> really-closed;
coherence
proof
A4: if>0(a,I)
= a >0_goto 3 ";" Goto(card I + 1) ";" (I ";" Stop SCM+FSA)
by SCMFSA6A:25
.= a >0_goto 3 ";" (Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a >0_goto 3 ";" (Goto(card I + 1) ";" I ";" Stop SCM+FSA)
by SCMFSA6A:25;
A5: card(Goto(card I + 1) ";" I ";" Stop SCM+FSA)
= card(Goto(card I + 1) ";" I) + card Stop SCM+FSA by SCMFSA6A:21
.= card(Goto(card I + 1) ";" I) + 1 by COMPOS_1:4
.= card Goto(card I + 1) + card I + 1 by SCMFSA6A:21
.= 1 + card I + 1 by SCMFSA8A:15
.= card I + 2;
0+1 <= card I by NAT_1:13;
then
A6: 1 + 2 <= card I + 2 by XREAL_1:7;
Goto(card I + 1) ";" I ";" Stop SCM+FSA is really-closed by Th26;
hence thesis by A6,Th30,A4,A5;
end;
end;
registration
let I be really-closed MacroInstruction of SCM+FSA, a be Int-Location;
cluster while=0(a,I) -> really-closed;
coherence
proof
reconsider IG = I ';' goto 0
as really-closed MacroInstruction of SCM+FSA by Th23;
reconsider W = if=0(a, IG) as really-closed MacroInstruction of SCM+FSA;
card W = card(I ';' goto 0) + 4 by Th1
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
then
A1: card I + 2 < card W by XREAL_1:8;
W +* (card I + 2, goto 0) is really-closed by Th22,A1;
hence thesis;
end;
cluster while>0(a,I) -> really-closed;
coherence
proof
reconsider IG = I ';' goto 0
as really-closed MacroInstruction of SCM+FSA by Th23;
reconsider W = if>0(a, IG) as really-closed MacroInstruction of SCM+FSA;
card W = card(I ';' goto 0) + 4 by Th2
.= card I + 1 + 4 by COMPOS_2:11
.= card I + 5;
then
A2: card I + 2 < card W by XREAL_1:8;
W +* (card I + 2, goto 0) is really-closed by Th22,A2;
hence thesis;
end;
end;
theorem
for I,J,K being MacroInstruction of SCM+FSA holds
I ";" J ';' K = I ";" (J ';' K) by COMPOS_1:29;
theorem
for I being MacroInstruction of SCM+FSA holds
stop Directed I = I ";" Stop SCM+FSA;
theorem
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 by COMPOS_1:29;
theorem
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 by COMPOS_1:29;