let T be InsType of SCM-Instr; :: according to COMPOS_0:def 7 :: thesis: for b1, b2 being set holds
( not b1 in JumpParts T or not proj1 b1 = proj1 b2 or for b3 being object holds
( not [T,b1,b3] in SCM-Instr or [T,b2,b3] in SCM-Instr ) )
let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b1 being object holds
( not [T,f1,b1] in SCM-Instr or [T,f2,b1] in SCM-Instr ) )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; :: thesis: for b1 being object holds
( not [T,f1,b1] in SCM-Instr or [T,f2,b1] in SCM-Instr )
let p be object ; :: thesis: ( not [T,f1,p] in SCM-Instr or [T,f2,p] in SCM-Instr )
assume A3: [T,f1,p] in SCM-Instr ; :: thesis: [T,f2,p] in SCM-Instr
not not T = 0 & ... & not T = 8 by Lm4;
per cases then ( T = 0 or not not T = 1 & ... & not T = 5 or T = 6 or T = 7 or T = 8 ) ;
suppose T = 0 ; :: thesis: [T,f2,p] in SCM-Instr
then JumpParts T = {{}} by Lm5;
then f1 = {} by A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr by A3; :: thesis: verum
end;
suppose not not T = 1 & ... & not T = 5 ; :: thesis: [T,f2,p] in SCM-Instr
then A4: JumpParts T = {{}} by Lm6;
f1 = {} by A4, A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr by A3; :: thesis: verum
end;
suppose A5: T = 6 ; :: thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
InsCode J = 6 by A5;
then J in { [K,<*i1*>,{}] where K is Element of Segm 9, i1 is Nat : K = 6 } by Th9;
then consider K being Element of Segm 9, i1 being Nat such that
A6: ( J = [K,<*i1*>,{}] & K = 6 ) ;
A7: p = {} by A6, XTUPLE_0:3;
f1 = <*i1*> by A6, XTUPLE_0:3;
then A8: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Nat ;
set I = [T,f2,{}];
[T,f2,{}] = [6,<*l*>,{}] by A5, A8, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I = [T,f2,{}] as Element of SCM-Instr by Th2;
f2 = JumpPart I ;
hence [T,f2,p] in SCM-Instr by A7; :: thesis: verum
end;
suppose A9: ( T = 7 or T = 8 ) ; :: thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
InsCode J = T ;
then J in { [K,<*i1*>,<*a*>] where K is Element of Segm 9, i1 is Nat, a is Element of SCM-Data-Loc : K in {7,8} } by A9, Th9;
then consider K being Element of Segm 9, i1 being Nat, a being Element of SCM-Data-Loc such that
A10: J = [K,<*i1*>,<*a*>] and
K in {7,8} ;
A11: p = <*a*> by A10, XTUPLE_0:3;
f1 = <*i1*> by A10, XTUPLE_0:3;
then A12: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Nat ;
set I = [T,f2,p];
A13: T in {7,8} by A9, TARSKI:def 2;
[T,f2,p] = [T,<*l*>,<*a*>] by A11, A12, FINSEQ_1:2, FINSEQ_1:def 8;
then reconsider I = [T,f2,p] as Element of SCM-Instr by A13, Th3;
InsCode I = T ;
then I in { [L,<*i2*>,<*b*>] where L is Element of Segm 9, i2 is Nat, b is Element of SCM-Data-Loc : L in {7,8} } by A9, Th9;
then consider L being Element of Segm 9, i2 being Nat, b being Element of SCM-Data-Loc such that
A14: I = [L,<*i2*>,<*b*>] and
L in {7,8} ;
L = InsCode I by A14
.= T ;
then A15: I = [T,<*i2*>,<*b*>] by A14;
thus [T,f2,p] in SCM-Instr by A15; :: thesis: verum
end;
end;