thus
SCM+FSA is regular
SCM+FSA is J/A-independent
let T be InsType of SCM+FSA; COMPOS_1:def 36 for b1, b2 being set
for b3 being set holds
( not b1 in JumpParts T or not b2 in product (product" (JumpParts T)) or not [T,b1,b3] in the Instructions of SCM+FSA or [T,b2,b3] in the Instructions of SCM+FSA )
let f1, f2 be Function; for b1 being set holds
( not f1 in JumpParts T or not f2 in product (product" (JumpParts T)) or not [T,f1,b1] in the Instructions of SCM+FSA or [T,f2,b1] in the Instructions of SCM+FSA )
let p be set ; ( not f1 in JumpParts T or not f2 in product (product" (JumpParts T)) or not [T,f1,p] in the Instructions of SCM+FSA or [T,f2,p] in the Instructions of SCM+FSA )
assume that
Z1:
f1 in JumpParts T
and
Z2:
f2 in product (product" (JumpParts T))
and
Z3:
[T,f1,p] in the Instructions of SCM+FSA
; [T,f2,p] in the Instructions of SCM+FSA
per cases
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 9 or T = 10 or T = 11 or T = 12 or T = 6 or T = 7 or T = 8 )
by Lm4;
suppose
(
T = 0 or
T = 1 or
T = 2 or
T = 3 or
T = 4 or
T = 5 or
T = 9 or
T = 10 or
T = 11 or
T = 12 )
;
[T,f2,p] in the Instructions of SCM+FSAthen A:
JumpParts T = {0}
by Th30, Th31, Th32, Th33, Th34, Th35, Th39, Th40, Th41, Th42;
then f1 =
0
by Z1, TARSKI:def 1
.=
f2
by Z2, A, CARD_3:19, CARD_3:156, TARSKI:def 1
;
hence
[T,f2,p] in the
Instructions of
SCM+FSA
by Z3;
verum end; suppose S:
T = 6
;
[T,f2,p] in the Instructions of SCM+FSAreconsider J =
[T,f1,p] as
Instruction of
SCM+FSA by Z3;
SS:
InsCode J = 6
by S, RECDEF_2:def 1;
then consider i1 being
Element of
NAT such that B7:
J = goto i1
by SCMFSA_2:59;
P:
p = {}
by B7, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th36;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by U1, Z2, CARD_3:18;
then reconsider l =
f2 . 1 as
Element of
NAT by B7, S, SS, Th53;
set I =
[T,f2,{}];
[T,f2,{}] = goto l
by S, XX, FINSEQ_1:4, FINSEQ_1:def 8;
then reconsider I =
[T,f2,{}] as
Instruction of
SCM+FSA ;
f2 = JumpPart I
by RECDEF_2:def 2;
hence
[T,f2,p] in the
Instructions of
SCM+FSA
by P;
verum end; suppose S:
T = 7
;
[T,f2,p] in the Instructions of SCM+FSAreconsider J =
[T,f1,p] as
Instruction of
SCM+FSA by Z3;
SS:
InsCode J = T
by RECDEF_2:def 1;
then consider i1 being
Element of
NAT ,
a being
Int-Location such that B7:
J = a =0_goto i1
by S, SCMFSA_2:60;
consider A being
Data-Location such that WW:
(
a = A &
a =0_goto i1 = A =0_goto i1 )
by SCMFSA_2:def 17;
P:
p = <*a*>
by B7, WW, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th37;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by U1, Z2, CARD_3:18;
then reconsider l =
f2 . 1 as
Element of
NAT by B7, SS, Th54;
set I =
[T,f2,p];
f2 = <*l*>
by XX, FINSEQ_1:4, FINSEQ_1:def 8;
then
[T,f2,p] = a =0_goto l
by S, P, Th15;
then reconsider I =
[T,f2,p] as
Instruction of
SCM+FSA ;
A6:
InsCode I = T
by RECDEF_2:def 1;
consider i2 being
Element of
NAT ,
b being
Int-Location such that A7:
I = b =0_goto i2
by S, A6, SCMFSA_2:60;
thus
[T,f2,p] in the
Instructions of
SCM+FSA
by A7;
verum end; suppose S:
T = 8
;
[T,f2,p] in the Instructions of SCM+FSAreconsider J =
[T,f1,p] as
Instruction of
SCM+FSA by Z3;
SS:
InsCode J = T
by RECDEF_2:def 1;
then consider i1 being
Element of
NAT ,
a being
Int-Location such that B7:
J = a >0_goto i1
by S, SCMFSA_2:61;
consider A being
Data-Location such that WW:
(
a = A &
a >0_goto i1 = A >0_goto i1 )
by SCMFSA_2:def 18;
P:
p = <*a*>
by B7, WW, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th38;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by U1, Z2, CARD_3:18;
then reconsider l =
f2 . 1 as
Element of
NAT by B7, SS, Th56;
set I =
[T,f2,p];
f2 = <*l*>
by XX, FINSEQ_1:4, FINSEQ_1:def 8;
then
[T,f2,p] = a >0_goto l
by S, P, Th16;
then reconsider I =
[T,f2,p] as
Instruction of
SCM+FSA ;
A6:
InsCode I = T
by RECDEF_2:def 1;
consider i2 being
Element of
NAT ,
b being
Int-Location such that A7:
I = b >0_goto i2
by S, A6, SCMFSA_2:61;
thus
[T,f2,p] in the
Instructions of
SCM+FSA
by A7;
verum end;