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 AMI_1:def 2;
let s be State of (Trivial-AMI N); :: according to AMI_1:def 8 :: thesis: Exec i,s = s
reconsider s = s as Element of product the Object-Kind of (Trivial-AMI N) by PBOOLE:155;
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 ;
then (the Execution of (Trivial-AMI N) . i) . s = s by FUNCT_1:35;
hence Exec i,s = s ; :: thesis: verum