let T be InsType of (SCM R); AMISTD_2:def 12 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
Z1:
f1 in JumpParts T
and
Z2:
f2 in product (product" (JumpParts T))
and
Z3:
[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 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 (SCM R)then A:
JumpParts T = {0 }
by Th32, Th33, Th34, Th35, Th36, Th37;
then
product" (JumpParts T) = {}
by CARD_3:156;
then B:
product (product" (JumpParts T)) = {0 }
by CARD_3:19;
f1 =
0
by A, Z1, TARSKI:def 1
.=
f2
by Z2, B, TARSKI:def 1
;
hence
[T,f2,p] in the
Instructions of
(SCM R)
by Z3;
verum end; suppose S:
T = 6
;
[T,f2,p] in the Instructions of (SCM R)reconsider J =
[T,f1,p] as
Instruction of
(SCM R) 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,
R
by Th22;
P:
p = {}
by B7, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
then U2:
for
x being
set st
x in dom f2 holds
f2 . x in (product" (JumpParts T)) . x
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 U2;
then
f2 . 1
in NAT
by B7, S, SS, Th50;
then reconsider l =
f2 . 1 as
Element of
NAT ;
W:
f2 = <*l*>
by XX, FINSEQ_1:4, FINSEQ_1:def 8;
set I =
[T,f2,{} ];
[T,f2,{} ] = goto l,
R
by S, W;
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 P;
verum end; suppose S:
T = 7
;
[T,f2,p] in the Instructions of (SCM R)reconsider J =
[T,f1,p] as
Instruction of
(SCM R) by Z3;
SS:
InsCode J = T
by RECDEF_2:def 1;
then consider a being
Data-Location of
R,
i1 being
Element of
NAT such that B7:
J = a =0_goto i1
by Th23, S;
P:
p = <*a*>
by B7, MCART_1:28;
U1:
dom f2 = dom (product" (JumpParts T))
by Z2, CARD_3:18;
then U2:
for
x being
set st
x in dom f2 holds
f2 . x in (product" (JumpParts T)) . x
by Z2, CARD_3:18;
XX:
dom f2 = {1}
by S, U1, Th39;
then
1
in dom f2
by TARSKI:def 1;
then
f2 . 1
in (product" (JumpParts T)) . 1
by U2;
then
f2 . 1
in NAT
by B7, SS, Th51;
then reconsider l =
f2 . 1 as
Element of
NAT ;
W:
f2 = <*l*>
by XX, FINSEQ_1:4, FINSEQ_1:def 8;
set I =
[T,f2,p];
[T,f2,p] = a =0_goto l
by P, S, W;
then reconsider I =
[T,f2,p] as
Instruction of
(SCM R) ;
A5:
f2 = JumpPart I
by RECDEF_2:def 2;
A6:
InsCode I = T
by RECDEF_2:def 1;
consider b being
Data-Location of
R,
i2 being
Element of
NAT such that A7:
I = b =0_goto i2
by S, A6, Th23;
R:
<*i2*> = f2
by A5, A7, RECDEF_2:def 2;
[T,<*i2*>,p] = a =0_goto i2
by B7, S, MCART_1:28;
hence
[T,f2,p] in the
Instructions of
(SCM R)
by R;
verum end;