let I be Instruction of Trivial-COM; :: thesis: JumpPart I = 0
the Instructions of Trivial-COM = {[0,0,0]} by Def1;
then I = [0,0,0] by TARSKI:def 1;
hence JumpPart I = 0 by RECDEF_2:def 2; :: thesis: verum