thus SCM+FSA is regular :: thesis:

proof

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

per cases by Lm1;

suppose InsCode I = 0 ; :: thesis:

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

end;

suppose InsCode I = 1 ; :: thesis:

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

end;

suppose InsCode I = 2 ; :: thesis:

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

end;

suppose InsCode I = 3 ; :: thesis:

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

end;

suppose InsCode I = 4 ; :: thesis:

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

end;

suppose InsCode I = 5 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th35;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) 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 = goto i2 by SCMFSA_2:35;
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+FSA 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, Th36;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A3, Th53; :: thesis:

end;

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

then consider i1 being Element of NAT , a being Int-Location such that
A8: I = a =0_goto i1 by SCMFSA_2:36;
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+FSA 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, Th37;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A8, Th54; :: thesis:

end;

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

then consider i1 being Element of NAT , a being Int-Location such that
A13: I = a >0_goto i1 by SCMFSA_2:37;
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+FSA 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, Th38;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A13, Th56; :: thesis:

end;

suppose InsCode I = 9 ; :: thesis:

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

end;

suppose InsCode I = 10 ; :: thesis:

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

end;

suppose InsCode I = 11 ; :: thesis:

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

end;

suppose InsCode I = 12 ; :: thesis:

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

end;

end;

end;

let T be InsType of SCM+FSA; :: 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+FSA ; :: thesis:

per cases by Lm1;

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 ) ; :: thesis:

then A20: JumpParts T = {0} by Th30, Th31, Th32, Th33, Th34, Th35, Th39, Th40, Th41, Th42;
then f1 = 0 by 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+FSA by A19; :: thesis:

end;

suppose A21: T = 6 ; :: thesis:

reconsider J = [T,f1,p] as Instruction of SCM+FSA by A19;
A22: InsCode J = 6 by A21, RECDEF_2:def 1;
then consider i1 being Element of NAT such that
A23: J = goto i1 by SCMFSA_2:35;
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, Th36;
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, Th53;
set I = [T,f2,{}];
[T,f2,{}] = goto l by A21, A26, FINSEQ_1:2, 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 A24; :: thesis:

end;

suppose A27: T = 7 ; :: thesis:

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

end;

suppose A36: T = 8 ; :: thesis:

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

end;

end;