thus Trivial-AMI N is with_explicit_jumps :: thesis: Trivial-AMI N is without_implicit_jumps

proof

let I be Instruction of (Trivial-AMI N); :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
let f be set ; :: according to TARSKI:def 3,AMISTD_2:def 6 :: thesis: ( not f in JUMP I or f in rng (JumpPart I) )
thus ( not f in JUMP I or f in rng (JumpPart I) ) ; :: thesis: verum

end;

thus Trivial-AMI N is without_implicit_jumps :: thesis: verum

proof

let I be Instruction of (Trivial-AMI N); :: according to AMISTD_2:def 9 :: thesis: I is without_implicit_jumps
let f be set ; :: according to TARSKI:def 3,AMISTD_2:def 7 :: thesis: ( not f in rng (JumpPart I) or f in JUMP I )
the Instructions of (Trivial-AMI N) = {[0 ,0 ,{} ]} by AMI_1:def 2;
then I = [0 ,0 ,0 ] by TARSKI:def 1;
hence ( not f in rng (JumpPart I) or f in JUMP I ) by RECDEF_2:def 2, RELAT_1:60; :: thesis: verum

end;