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