let N be with_non-empty_elements set ; :: thesis: for i being Instruction of holds i is halting
let i be Instruction of ; :: thesis: i is halting
set M = Trivial-AMI N;
A1: the Instructions of (Trivial-AMI N) = {[0 ,{} ]} by AMI_1:def 2;
let s be State of ; :: according to AMI_1:def 8 :: thesis: Exec i,s = s
the Object-Kind of (Trivial-AMI N) = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) by AMI_1:def 2;
then the Execution of (Trivial-AMI N) . i = ([0 ,{} ] .--> (id (product the Object-Kind of (Trivial-AMI N)))) . i by AMI_1:def 2
.= id (product the Object-Kind of (Trivial-AMI N)) by A1, FUNCOP_1:13 ;
hence Exec i,s = s by FUNCT_1:35; :: thesis: verum