let T be InsType of (SCM-Instr R); :: 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 R or [T,b2,b3] in SCM-Instr R ) )
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 R or [T,f2,b1] in SCM-Instr R ) )
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 R or [T,f2,b1] in SCM-Instr R )
let p be object ; :: thesis: ( not [T,f1,p] in SCM-Instr R or [T,f2,p] in SCM-Instr R )
assume A3: [T,f1,p] in SCM-Instr R ; :: thesis: [T,f2,p] in SCM-Instr R
reconsider II = [T,f1,p] as Element of SCM-Instr R by A3;
A4: InsCode II = T ;
InsCode II <= 7 by Lm1;
then not not InsCode II = 0 & ... & not InsCode II = 7 by NAT_1:60;
per cases then ( T = 0 or not not T = 1 & ... & not T = 4 or T = 5 or T = 6 or T = 7 ) ;
suppose T = 0 ; :: thesis: [T,f2,p] in SCM-Instr R
then II in {[0,{},{}]} by A4, Th7;
then II = [0,{},{}] by TARSKI:def 1;
then JumpPart II = {} ;
then A5: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A5, A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; :: thesis: verum
end;
suppose not not T = 1 & ... & not T = 4 ; :: thesis: [T,f2,p] in SCM-Instr R
then II in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by A4, Th7;
then ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( II = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
then JumpPart II = {} ;
then A6: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A6, A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; :: thesis: verum
end;
suppose T = 5 ; :: thesis: [T,f2,p] in SCM-Instr R
then II in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } by A4, Th7;
then ex a being Element of SCM-Data-Loc ex r being Element of R st II = [5,{},<*a,r*>] ;
then JumpPart II = {} ;
then A7: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A7, A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; :: thesis: verum
end;
suppose A8: T = 6 ; :: thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
InsCode J = 6 by A8;
then J in { [6,<*i*>,{}] where i is Nat : verum } by Th7;
then consider i1 being Nat such that
A9: J = [6,<*i1*>,{}] ;
A10: p = {} by A9, XTUPLE_0:3;
f1 = <*i1*> by A9, XTUPLE_0:3;
then A11: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def 12;
set I = [T,f2,{}];
A12: [T,f2,{}] = [6,<*l*>,{}] by A8, A11, FINSEQ_1:2, FINSEQ_1:def 8;
[6,<*l*>,{}] in { [6,<*n*>,{}] where n is Nat : verum } ;
then [6,<*l*>,{}] in ({[0,{},{}]} \/ { [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*n*>,{}] where n is Nat : verum } by XBOOLE_0:def 3;
then [6,<*l*>,{}] in (({[0,{},{}]} \/ { [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*n*>,{}] where n is Nat : verum } ) \/ { [7,<*n*>,<*a*>] where n is Nat, a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;
then [6,<*l*>,{}] in SCM-Instr R by XBOOLE_0:def 3;
then reconsider I = [T,f2,{}] as Element of SCM-Instr R by A12;
f2 = JumpPart I ;
hence [T,f2,p] in SCM-Instr R by A10; :: thesis: verum
end;
suppose A13: T = 7 ; :: thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
InsCode J = T ;
then J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } by A13, Th7;
then consider i1 being Nat, a being Element of SCM-Data-Loc such that
A14: J = [7,<*i1*>,<*a*>] ;
A15: p = <*a*> by A14, XTUPLE_0:3;
f1 = <*i1*> by A14, XTUPLE_0:3;
then A16: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def 12;
set I = [T,f2,p];
A17: [T,f2,p] = [T,<*l*>,<*a*>] by A15, A16, FINSEQ_1:2, FINSEQ_1:def 8;
[(InsCode [T,f2,p]),<*l*>,<*a*>] in { [7,<*n*>,<*c*>] where n is Nat, c is Element of SCM-Data-Loc : verum } by A13;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in (({[0,{},{}]} \/ { [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a7*>] where i is Nat, a7 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in ((({[0,{},{}]} \/ { [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a7*>] where i is Nat, a7 is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a7,r7*>] where a7 is Element of SCM-Data-Loc , r7 is Element of R : verum } by XBOOLE_0:def 3;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in SCM-Instr R ;
then reconsider I = [T,f2,p] as Element of SCM-Instr R by A17;
InsCode I = T ;
then I in { [7,<*i2*>,<*b*>] where i2 is Nat, b is Element of SCM-Data-Loc : verum } by A13, Th7;
then consider i2 being Nat, b being Element of SCM-Data-Loc such that
A18: I = [7,<*i2*>,<*b*>] ;
7 = InsCode I by A18
.= T ;
then A19: I = [T,<*i2*>,<*b*>] by A18;
thus [T,f2,p] in SCM-Instr R by A19; :: thesis: verum
end;
end;