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 ]}) +* (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 AMI_1:def 11; :: thesis: ( STC N is definite & STC N is realistic & STC N is steady-programmed )
A3: the Instructions of (STC N) = {[1,0 ],[0 ,0 ]} by Def11;
thus STC N is definite :: thesis: ( STC N is realistic & STC N is steady-programmed )

proof

let l be Instruction-Location of STC N; :: according to AMI_1:def 14 :: thesis: ObjectKind l = the Instructions of (STC N)
A4: l in NAT by AMI_1:def 4;
dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then A5: not l in dom (NAT .--> NAT ) by TARSKI:def 1;
thus ObjectKind l = ((NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT )) . l by Def11
.= (NAT --> {[1,0 ],[0 ,0 ]}) . l by A5, FUNCT_4:12
.= the Instructions of (STC N) by A3, A4, 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 AMI_1:def 21 :: thesis: contradiction
hence contradiction by Def11; :: thesis: verum

end;

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

proof

let s be State of ; :: according to AMI_1:def 13 :: thesis: for b₁ being Element of the Instructions of (STC N)
for b₂ being Instruction-Location of STC N holds (Exec b₁,s) . b₂ = s . b₂
let i be Instruction of ; :: thesis: for b₁ being Instruction-Location of STC N holds (Exec i,s) . b₁ = s . b₁
let l be Instruction-Location of STC N; :: 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 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by Def11;
l in NAT by AMI_1:def 4;
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 ] or i = [0 ,0 ] ) by A3, TARSKI:def 2;

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

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

now

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

end;

then the Execution of (STC N) . i = ([1,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 A6
.= s . l by A8, FUNCT_4:12 ;
:: thesis: verum

end;

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

then A11: i in {[0 ,0 ]} by TARSKI:def 1;
then i in dom ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by FUNCOP_1:19;
then the Execution of (STC N) . i = ([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 ;
hence (Exec i,s) . l = s . l by FUNCT_1:35; :: thesis: verum

end;

end;

end;