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

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