let N be with_non-empty_elements set ; :: thesis: for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec i,s = s
set T = Trivial-AMI N;
let s be State of (Trivial-AMI N); :: thesis: for i being Instruction of (Trivial-AMI N) holds Exec i,s = s
let i be Instruction of (Trivial-AMI N); :: thesis: Exec i,s = s
set f = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT );
A1: product the Object-Kind of (Trivial-AMI N) = product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )) by Def2;
reconsider ss = s as Element of product the Object-Kind of (Trivial-AMI N) by PBOOLE:155;
the Instructions of (Trivial-AMI N) = {[0 ,{} ,{} ]} by Def2;
then ( (i .--> (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ))))) . i = id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ))) & i = [0 ,{} ,{} ] ) by FUNCOP_1:87, TARSKI:def 1;
hence Exec i,s = (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )))) . ss by Def2
.= s by A1, FUNCT_1:35 ;
:: thesis: verum