thus SCM is regular :: thesis:

proof

let I be Instruction of SCM; :: according to COMPOS_1:def 14 :: thesis:
set T = InsCode I;
A1: JumpPart I in JumpParts (InsCode I) ;

per cases by Th7;

suppose InsCode I = 0 ; :: thesis:

then I = halt SCM by AMI_5:7;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 1 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th19;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 2 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th20;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 3 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th21;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 4 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th22;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 5 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th23;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose A2: InsCode I = 6 ; :: thesis:

then consider i2 being Element of NAT such that
A3: I = SCM-goto i2 by AMI_5:13;
let k be set ; :: thesis:
assume A4: k in dom (JumpPart I) ; :: thesis:
for f being Function st f in JumpParts (InsCode I) holds
k in dom f

proof

let f be Function; :: thesis:
assume f in JumpParts (InsCode I) ; :: thesis:
then consider J being Instruction of SCM such that
A5: f = JumpPart J and
A6: InsCode J = InsCode I ;
thus k in dom f by A4, A5, A6, COMPOS_1:def 12; :: thesis:

end;

then k in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then k in {1} by A2, Th24;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A3, Th37; :: thesis:

end;

suppose A7: InsCode I = 7 ; :: thesis:

then consider i1 being Element of NAT , a being Data-Location such that
A8: I = a =0_goto i1 by AMI_5:14;
let k be set ; :: thesis:
assume A9: k in dom (JumpPart I) ; :: thesis:
for f being Function st f in JumpParts (InsCode I) holds
k in dom f

proof

let f be Function; :: thesis:
assume f in JumpParts (InsCode I) ; :: thesis:
then consider J being Instruction of SCM such that
A10: f = JumpPart J and
A11: InsCode J = InsCode I ;
thus k in dom f by A9, A10, A11, COMPOS_1:def 12; :: thesis:

end;

then k in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then k in {1} by A7, Th25;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A8, Th38; :: thesis:

end;

suppose A12: InsCode I = 8 ; :: thesis:

then consider i1 being Element of NAT , a being Data-Location such that
A13: I = a >0_goto i1 by AMI_5:15;
let k be set ; :: thesis:
assume A14: k in dom (JumpPart I) ; :: thesis:
for f being Function st f in JumpParts (InsCode I) holds
k in dom f

proof

let f be Function; :: thesis:
assume f in JumpParts (InsCode I) ; :: thesis:
then consider J being Instruction of SCM such that
A15: f = JumpPart J and
A16: InsCode J = InsCode I ;
thus k in dom f by A14, A15, A16, COMPOS_1:def 12; :: thesis:

end;

then k in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then k in {1} by A12, Th26;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A13, Th40; :: thesis:

end;

end;

end;

let T be InsType of SCM; :: according to COMPOS_1:def 15 :: thesis:
let f1, f2 be Function; :: thesis:
let p be set ; :: thesis:
assume that
A17: f1 in JumpParts T and
A18: f2 in product (product" (JumpParts T)) and
A19: [T,f1,p] in the Instructions of SCM ; :: thesis:

per cases by Th7;

suppose ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) ; :: thesis:

then A20: JumpParts T = {0} by Th18, Th19, Th20, Th21, Th22, Th23;
f1 = 0 by A20, A17, TARSKI:def 1
.= f2 by A18, A20, CARD_3:10, CARD_3:106, TARSKI:def 1 ;
hence [T,f2,p] in the Instructions of SCM by A19; :: thesis:

end;

suppose A21: T = 6 ; :: thesis:

reconsider J = [T,f1,p] as Instruction of SCM by A19;
A22: InsCode J = 6 by A21, RECDEF_2:def 1;
then consider i1 being Element of NAT such that
A23: J = SCM-goto i1 by AMI_5:13;
A24: p = {} by A23, MCART_1:25;
A25: dom f2 = dom (product" (JumpParts T)) by A18, CARD_3:9;
A26: dom f2 = {1} by A21, A25, Th24;
then 1 in dom f2 by TARSKI:def 1;
then f2 . 1 in (product" (JumpParts T)) . 1 by A25, A18, CARD_3:9;
then reconsider l = f2 . 1 as Element of NAT by A23, A21, A22, Th37;
set I = [T,f2,{}];
[T,f2,{}] = SCM-goto l by A21, A26, FINSEQ_1:2, 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 A24; :: thesis:

end;

suppose A27: T = 7 ; :: thesis:

reconsider J = [T,f1,p] as Instruction of SCM by A19;
A28: InsCode J = T by RECDEF_2:def 1;
then consider i1 being Element of NAT , a being Data-Location such that
A29: J = a =0_goto i1 by A27, AMI_5:14;
A30: p = <*a*> by A29, MCART_1:25;
A31: dom f2 = dom (product" (JumpParts T)) by A18, CARD_3:9;
A32: dom f2 = {1} by A27, A31, Th25;
then 1 in dom f2 by TARSKI:def 1;
then f2 . 1 in (product" (JumpParts T)) . 1 by A31, A18, CARD_3:9;
then reconsider l = f2 . 1 as Element of NAT by A29, A28, Th38;
set I = [T,f2,p];
[T,f2,p] = a =0_goto l by A30, A27, A32, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I = [T,f2,p] as Instruction of SCM ;
A33: InsCode I = T by RECDEF_2:def 1;
consider i2 being Element of NAT , b being Data-Location such that
A34: I = b =0_goto i2 by A27, A33, AMI_5:14;
thus [T,f2,p] in the Instructions of SCM by A34; :: thesis:

end;

suppose A35: T = 8 ; :: thesis:

reconsider J = [T,f1,p] as Instruction of SCM by A19;
A36: InsCode J = T by RECDEF_2:def 1;
then consider i1 being Element of NAT , a being Data-Location such that
A37: J = a >0_goto i1 by A35, AMI_5:15;
A38: p = <*a*> by A37, MCART_1:25;
A39: dom f2 = dom (product" (JumpParts T)) by A18, CARD_3:9;
A40: dom f2 = {1} by A35, A39, Th26;
then 1 in dom f2 by TARSKI:def 1;
then f2 . 1 in (product" (JumpParts T)) . 1 by A39, A18, CARD_3:9;
then reconsider l = f2 . 1 as Element of NAT by A37, A36, Th40;
set I = [T,f2,p];
[T,f2,p] = a >0_goto l by A38, A35, A40, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I = [T,f2,p] as Instruction of SCM ;
A41: InsCode I = T by RECDEF_2:def 1;
consider i2 being Element of NAT , b being Data-Location such that
A42: I = b >0_goto i2 by A35, A41, AMI_5:15;
thus [T,f2,p] in the Instructions of SCM by A42; :: thesis:

end;

end;