let T be InsType of (SCM R); COMPOS_1:def 15 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 R) or [T,b2,b3] in the Instructions of (SCM R) )
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 R) or [T,f2,b1] in the Instructions of (SCM R) )
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 R) or [T,f2,p] in the Instructions of (SCM R) )
assume that
A1:
f1 in JumpParts T
and
A2:
f2 in product (product" (JumpParts T))
and
A3:
[T,f1,p] in the Instructions of (SCM R)
; [T,f2,p] in the Instructions of (SCM R)
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 )
by Lm2;
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 (SCM R)then A4:
JumpParts T = {0}
by Th32, Th33, Th34, Th35, Th36, Th37;
then A5:
product (product" (JumpParts T)) = {0}
by CARD_3:10, CARD_3:106;
f1 =
0
by A4, A1, TARSKI:def 1
.=
f2
by A2, A5, TARSKI:def 1
;
hence
[T,f2,p] in the
Instructions of
(SCM R)
by A3;
verum end; suppose A6:
T = 6
;
[T,f2,p] in the Instructions of (SCM R)reconsider J =
[T,f1,p] as
Instruction of
(SCM R) by A3;
A7:
InsCode J = 6
by A6, RECDEF_2:def 1;
then consider i1 being
Element of
NAT such that A8:
J = goto (
i1,
R)
by Th22;
A9:
p = {}
by A8, MCART_1:25;
A10:
dom f2 = dom (product" (JumpParts T))
by A2, CARD_3:9;
A12:
dom f2 = {1}
by A6, A10, Th38;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by A10, A2, CARD_3:9;
then reconsider l =
f2 . 1 as
Element of
NAT by A8, A6, A7, Th50;
set I =
[T,f2,{}];
[T,f2,{}] = goto (
l,
R)
by A6, A12, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I =
[T,f2,{}] as
Instruction of
(SCM R) ;
f2 = JumpPart I
by RECDEF_2:def 2;
hence
[T,f2,p] in the
Instructions of
(SCM R)
by A9;
verum end; suppose A13:
T = 7
;
[T,f2,p] in the Instructions of (SCM R)reconsider J =
[T,f1,p] as
Instruction of
(SCM R) by A3;
A14:
InsCode J = T
by RECDEF_2:def 1;
then consider a being
Data-Location of
R,
i1 being
Element of
NAT such that A15:
J = a =0_goto i1
by Th23, A13;
A16:
p = <*a*>
by A15, MCART_1:25;
A17:
dom f2 = dom (product" (JumpParts T))
by A2, CARD_3:9;
A19:
dom f2 = {1}
by A13, A17, Th39;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by A17, A2, CARD_3:9;
then reconsider l =
f2 . 1 as
Element of
NAT by A15, A14, Th51;
set I =
[T,f2,p];
[T,f2,p] = a =0_goto l
by A16, A13, A19, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I =
[T,f2,p] as
Instruction of
(SCM R) ;
A20:
f2 = JumpPart I
by RECDEF_2:def 2;
thus
[T,f2,p] in the
Instructions of
(SCM R)
by A20;
verum end;