thus
SCM is regular
SCM is J/A-independent
let T be InsType of SCM; 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 or [T,b2,b3] in the Instructions of SCM )
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 or [T,f2,b1] in the Instructions of SCM )
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 or [T,f2,p] in the Instructions of SCM )
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
; [T,f2,p] in the Instructions of SCM
per cases
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
by Lm3;
suppose
(
T = 0 or
T = 1 or
T = 2 or
T = 3 or
T = 4 or
T = 5 )
;
[T,f2,p] in the Instructions of SCMthen A:
JumpParts T = {0}
by Th16, Th17, Th18, Th19, Th20, Th21;
f1 =
0
by A, 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
by Z3;
verum end; suppose S:
T = 6
;
[T,f2,p] in the Instructions of SCMreconsider J =
[T,f1,p] as
Instruction of
SCM by Z3;
SS:
InsCode J = 6
by S, RECDEF_2:def 1;
then consider i1 being
Element of
NAT such that B7:
J = SCM-goto i1
by AMI_5:52;
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, Th22;
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, Th35;
set I =
[T,f2,{}];
[T,f2,{}] = SCM-goto l
by S, XX, FINSEQ_1:4, FINSEQ_1:def 8;
then reconsider I =
[T,f2,{}] as
Instruction of
SCM ;
f2 = JumpPart I
by RECDEF_2:def 2;
hence
[T,f2,p] in the
Instructions of
SCM
by P;
verum end; suppose S:
T = 7
;
[T,f2,p] in the Instructions of SCMreconsider J =
[T,f1,p] as
Instruction of
SCM by Z3;
SS:
InsCode J = T
by RECDEF_2:def 1;
then consider i1 being
Element of
NAT ,
a being
Data-Location such that B7:
J = a =0_goto i1
by S, AMI_5:53;
P:
p = <*a*>
by B7, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th23;
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, Th36;
set I =
[T,f2,p];
[T,f2,p] = a =0_goto l
by P, S, XX, FINSEQ_1:4, FINSEQ_1:def 8;
then reconsider I =
[T,f2,p] as
Instruction of
SCM ;
A6:
InsCode I = T
by RECDEF_2:def 1;
consider i2 being
Element of
NAT ,
b being
Data-Location such that A7:
I = b =0_goto i2
by S, A6, AMI_5:53;
thus
[T,f2,p] in the
Instructions of
SCM
by A7;
verum end; suppose S:
T = 8
;
[T,f2,p] in the Instructions of SCMreconsider J =
[T,f1,p] as
Instruction of
SCM by Z3;
SS:
InsCode J = T
by RECDEF_2:def 1;
then consider i1 being
Element of
NAT ,
a being
Data-Location such that B7:
J = a >0_goto i1
by S, AMI_5:54;
P:
p = <*a*>
by B7, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th24;
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, Th38;
set I =
[T,f2,p];
[T,f2,p] = a >0_goto l
by P, S, XX, FINSEQ_1:4, FINSEQ_1:def 8;
then reconsider I =
[T,f2,p] as
Instruction of
SCM ;
A6:
InsCode I = T
by RECDEF_2:def 1;
consider i2 being
Element of
NAT ,
b being
Data-Location such that A7:
I = b >0_goto i2
by S, A6, AMI_5:54;
thus
[T,f2,p] in the
Instructions of
SCM
by A7;
verum end;