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