let N be with_zero set ; :: thesis: for i being Instruction of (Trivial-AMI N) holds i is halting
let i be Instruction of (Trivial-AMI N); :: thesis: i is halting
set M = Trivial-AMI N;
A1: the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by EXTPRO_1:def 1;
let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def 3 :: thesis: Exec (i,s) = s
reconsider s = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107;
A2: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by EXTPRO_1:def 1;
the Execution of (Trivial-AMI N) . i = ([0,{},{}] .--> (id (product (the_Values_of (Trivial-AMI N))))) . i by A2, EXTPRO_1:def 1
.= id (product (the_Values_of (Trivial-AMI N))) by A1 ;
then ( the Execution of (Trivial-AMI N) . i) . s = s ;
hence Exec (i,s) = s ; :: thesis: verum