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 .--> NAT;
A1: product the Object-Kind of (Trivial-AMI N) = product (NAT .--> NAT) by Def1;
reconsider ss = s as Element of product the Object-Kind of (Trivial-AMI N) by CARD_3:107;
the Instructions of (Trivial-AMI N) = {[0,{},{}]} by Def1;
then ( (i .--> (id (product (NAT .--> NAT)))) . i = id (product (NAT .--> NAT)) & i = [0,{},{}] ) by FUNCOP_1:72, TARSKI:def 1;
hence Exec (i,s) = (id (product (NAT .--> NAT))) . ss by Def1
.= s by A1, FUNCT_1:18 ;
:: thesis: verum