set IT = STC N;
set Ok = the Object-Kind of (STC N);
A1: NAT in {NAT } by TARSKI:def 1;
dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then A2: NAT in dom (NAT .--> NAT ) by TARSKI:def 1;
the Object-Kind of (STC N) . NAT = ((NAT --> {[1,0 ,0 ],[0 ,0 ,0 ]}) +* (NAT .--> NAT )) . NAT by Def11
.= (NAT .--> NAT ) . NAT by A2, FUNCT_4:14
.= NAT by A1, FUNCOP_1:13 ;
then ObjectKind (IC (STC N)) = NAT by Def11;
hence STC N is IC-Ins-separated by COMPOS_1:def 6; :: thesis: ( STC N is definite & STC N is realistic & STC N is steady-programmed )
A3: the Instructions of (STC N) = {[1,0 ,0 ],[0 ,0 ,0 ]} by Def11;
thus STC N is definite :: thesis: ( STC N is realistic & STC N is steady-programmed )

proof

let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of (STC N) . l = the Instructions of (STC N)
dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then A5: not l in dom (NAT .--> NAT ) by TARSKI:def 1;
thus the Object-Kind of (STC N) . l = ((NAT --> {[1,0 ,0 ],[0 ,0 ,0 ]}) +* (NAT .--> NAT )) . l by Def11
.= (NAT --> {[1,0 ,0 ],[0 ,0 ,0 ]}) . l by A5, FUNCT_4:12
.= the Instructions of (STC N) by A3, FUNCOP_1:13 ; :: thesis: verum

end;

thus STC N is realistic :: thesis: STC N is steady-programmed

proof

assume the Instruction-Counter of (STC N) in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
hence contradiction by Def11; :: thesis: verum

end;

thus STC N is steady-programmed :: thesis: verum

proof

let s be State of (STC N); :: according to AMI_1:def 13 :: thesis: for b₁ being Element of the Instructions of (STC N)
for b₂ being Element of NAT holds (Exec b₁,s) . b₂ = s . b₂
let i be Instruction of (STC N); :: thesis: for b₁ being Element of NAT holds (Exec i,s) . b₁ = s . b₁
let l be Element of NAT ; :: thesis: (Exec i,s) . l = s . l
consider f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) such that
A6: for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT ))) and
A7: the Execution of (STC N) = ([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by Def11;
B6: for s being State of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT )))

proof

let s be State of (STC N); :: thesis: f . s = s +* (NAT .--> (succ (s . NAT )))
reconsider s = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
f . s = s +* (NAT .--> (succ (s . NAT ))) by A6;
hence f . s = s +* (NAT .--> (succ (s . NAT ))) ; :: thesis: verum

end;

reconsider ss = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
not l in {NAT } by TARSKI:def 1;
then A8: not l in dom (NAT .--> (succ (s . NAT ))) by FUNCOP_1:19;

per cases ( i = [1,0 ,0 ] or i = [0 ,0 ,0 ] ) by A3, TARSKI:def 2;

suppose A9: i = [1,0 ,0 ] ; :: thesis: (Exec i,s) . l = s . l

then A10: i in {[1,0 ,0 ]} by TARSKI:def 1;

now

assume i in dom ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) ; :: thesis: contradiction
then i in {[0 ,0 ,0 ]} by FUNCOP_1:19;
then i = [0 ,0 ,0 ] by TARSKI:def 1;
hence contradiction by A9, MCART_1:28; :: thesis: verum

end;

then the Execution of (STC N) . i = ([1,0 ,0 ] .--> f) . i by A7, FUNCT_4:12
.= f by A10, FUNCOP_1:13 ;
hence (Exec i,s) . l = (s +* (NAT .--> (succ (s . NAT )))) . l by B6
.= s . l by A8, FUNCT_4:12 ;
:: thesis: verum

end;

suppose i = [0 ,0 ,0 ] ; :: thesis: (Exec i,s) . l = s . l

then A11: i in {[0 ,0 ,0 ]} by TARSKI:def 1;
then i in dom ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by FUNCOP_1:19;
then the Execution of (STC N) . i = ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) . i by A7, FUNCT_4:14
.= id (product the Object-Kind of (STC N)) by A11, FUNCOP_1:13 ;
then (the Execution of (STC N) . i) . ss = ss by FUNCT_1:35;
hence (Exec i,s) . l = s . l ; :: thesis: verum

end;

end;

end;