let i be Element of SCM+FSA-Instr ; :: thesis: for ii being Element of SCM-Instr st i = ii holds
JumpParts (InsCode i) = JumpParts (InsCode ii)
let ii be Element of SCM-Instr ; :: thesis: ( i = ii implies JumpParts (InsCode i) = JumpParts (InsCode ii) )
assume A1: i = ii ; :: thesis: JumpParts (InsCode i) = JumpParts (InsCode ii)
thus JumpParts (InsCode i) c= JumpParts (InsCode ii) :: according to XBOOLE_0:def 10 :: thesis: JumpParts (InsCode ii) c= JumpParts (InsCode i)
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in JumpParts (InsCode i) or e in JumpParts (InsCode ii) )
assume e in JumpParts (InsCode i) ; :: thesis: e in JumpParts (InsCode ii)
then consider I being Element of SCM+FSA-Instr such that
A2: e = JumpPart I and
A3: InsCode I = InsCode i ;
InsCode I <= 8 by A1, A3, SCM_INST:10;
then reconsider II = I as Element of SCM-Instr by Th2;
InsCode II = InsCode ii by A1, A3;
hence e in JumpParts (InsCode ii) by A2; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in JumpParts (InsCode ii) or e in JumpParts (InsCode i) )
assume e in JumpParts (InsCode ii) ; :: thesis: e in JumpParts (InsCode i)
then consider II being Element of SCM-Instr such that
A4: e = JumpPart II and
A5: InsCode II = InsCode ii ;
A6: SCM-Instr c= SCM+FSA-Instr by Th1;
II in SCM+FSA-Instr by A6;
then reconsider I = II as Element of SCM+FSA-Instr ;
InsCode I = InsCode i by A1, A5;
hence e in JumpParts (InsCode i) by A4; :: thesis: verum