let N be non empty with_non-empty_elements 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 Instructions 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 Object-Kind of (Trivial-AMI N) by CARD_3:107;
the Object-Kind of (Trivial-AMI N) = NAT .--> NAT by EXTPRO_1:def 1;
then the Execution of (Trivial-AMI N) . i = ([0,{},{}] .--> (id (product the Object-Kind of (Trivial-AMI N)))) . i by EXTPRO_1:def 1
.= id (product the Object-Kind of (Trivial-AMI N)) by A1, FUNCOP_1:7 ;
then ( the Execution of (Trivial-AMI N) . i) . s = s by FUNCT_1:18;
hence Exec (i,s) = s ; :: thesis: verum