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

proof

let I be Instruction of (Trivial-AMI N); :: according to AMISTD_2:def 2 :: thesis: I is with_explicit_jumps

the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def 1;

then I = [0,0,0] by TARSKI:def 1;

hence JUMP I = rng (JumpPart I) ; :: according to AMISTD_2:def 1 :: thesis: verum

end;the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def 1;

then I = [0,0,0] by TARSKI:def 1;

hence JUMP I = rng (JumpPart I) ; :: according to AMISTD_2:def 1 :: thesis: verum