let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for s being State of (Trivial-AMI IL,N)
for i being Instruction of (Trivial-AMI IL,N) holds Exec i,s = s
let N be with_non-empty_elements set ; :: thesis: for s being State of (Trivial-AMI IL,N)
for i being Instruction of (Trivial-AMI IL,N) holds Exec i,s = s
set T = Trivial-AMI IL,N;
let s be State of (Trivial-AMI IL,N); :: thesis: for i being Instruction of (Trivial-AMI IL,N) holds Exec i,s = s
let i be Instruction of (Trivial-AMI IL,N); :: 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;
the Instructions of (Trivial-AMI IL,N) = {[0 ,{} ]} by Def2;
then A2: i = [0 ,{} ] by TARSKI:def 1;
A3: 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, A2, Def2
.= s by A3, FUNCT_1:35 ; :: thesis: verum