let IL be non empty set ; :: thesis: for N being with_non-empty_elements set holds Trivial-AMI IL,N is halting
let N be with_non-empty_elements set ; :: thesis: Trivial-AMI IL,N is halting
set T = Trivial-AMI IL,N;
{[0 ,{} ]} = the Instructions of (Trivial-AMI IL,N) by Def2;
then reconsider I = [0 ,{} ] as Instruction of (Trivial-AMI IL,N) by TARSKI:def 1;
take I ; :: according to AMI_1:def 9 :: thesis: I is halting
let s be State of (Trivial-AMI IL,N); :: according to AMI_1:def 8 :: thesis: Exec I,s = s
set f = (IL --> {[0 ,{} ]}) +* (IL .--> IL);
A1: (I .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL))))) . I = id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL))) by FUNCOP_1:87;
A2: product the Object-Kind of (Trivial-AMI IL,N) = product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)) by Def2;
thus Exec I,s = (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) . s by A1, Def2
.= s by A2, FUNCT_1:35 ; :: thesis: verum