let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for I being Instruction of (Trivial-AMI IL,N) holds AddressPart I = 0
let IL be non empty set ; :: thesis: for I being Instruction of (Trivial-AMI IL,N) holds AddressPart I = 0
let I be Instruction of (Trivial-AMI IL,N); :: thesis: AddressPart I = 0
the Instructions of (Trivial-AMI IL,N) = {[0 ,{} ]} by AMI_1:def 2;
then I = [0 ,0 ] by TARSKI:def 1;
hence AddressPart I = 0 by MCART_1:def 2; :: thesis: verum