thus Trivial-AMI N is with_explicit_jumps :: thesis: ( Trivial-AMI N is without_implicit_jumps & Trivial-AMI N is regular )

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 AMISTD_2:def 6 :: thesis: ( f in JUMP I implies ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) )
thus ( f in JUMP I implies ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) ) ; :: thesis: verum

end;

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

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 AMISTD_2:def 7 :: thesis: ( ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) implies f in JUMP I )
the Instructions of (Trivial-AMI N) = {[0 ,{} ]} by AMI_1:def 2;
then I = [0 ,0 ] by TARSKI:def 1;
hence ( ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) implies f in JUMP I ) by MCART_1:def 2, RELAT_1:60; :: thesis: verum

end;

let T be InsType of (Trivial-AMI N); :: according to AMISTD_2:def 11 :: thesis: AddressParts T is product-like
take {} ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product {}
thus AddressParts T = product {} by Lm4, CARD_3:19; :: thesis: verum