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; ( STC N is definite & STC N is realistic )
A3:
the Instructions of (STC N) = {[1,0,0],[0,0,0]}
by Def11;
thus
STC N is definite
STC N is realistic proof
let l be
Element of
NAT ;
COMPOS_1:def 8 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
;
verum
end;
assume
the Instruction-Counter of (STC N) in NAT
; COMPOS_1:def 12 contradiction
hence
contradiction
by Def11; verum