thus STC N is with_explicit_jumps :: thesis: ( STC N is without_implicit_jumps & STC N is homogeneous & STC N is regular & STC N is J/A-independent )

proof

let I be Instruction of (STC N); :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
let f be set ; :: according to TARSKI:def 3,AMISTD_2:def 6 :: thesis: ( not f in JUMP I or f in rng (JumpPart I) )
thus ( not f in JUMP I or f in rng (JumpPart I) ) ; :: thesis: verum

end;

thus STC N is without_implicit_jumps :: thesis: ( STC N is homogeneous & STC N is regular & STC N is J/A-independent )

proof

let I be Instruction of (STC N); :: according to AMISTD_2:def 9 :: thesis: I is without_implicit_jumps
let f be set ; :: according to TARSKI:def 3,AMISTD_2:def 7 :: thesis: ( not f in rng (JumpPart I) or f in JUMP I )
the Instructions of (STC N) = {[0 ,0 ,0 ],[1,0 ,0 ]} by AMISTD_1:def 11;
then ( I = [0 ,0 ,0 ] or I = [1,0 ,0 ] ) by TARSKI:def 2;
hence ( not f in rng (JumpPart I) or f in JUMP I ) by RECDEF_2:def 2, RELAT_1:60; :: thesis: verum

end;

thus STC N is homogeneous :: thesis: ( STC N is regular & STC N is J/A-independent )

proof

let I, J be Instruction of (STC N); :: according to AMISTD_2:def 4 :: thesis: ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) )
( JumpPart I = {} & JumpPart J = {} ) by Th17;
hence ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) ) ; :: thesis: verum

end;

thus STC N is regular :: thesis: STC N is J/A-independent

proof

let I be Instruction of (STC N); :: according to AMISTD_2:def 11 :: thesis: for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT
JumpPart I = {} by Th17;
hence for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT ; :: thesis: verum

end;

let T be InsType of (STC N); :: according to AMISTD_2:def 12 :: thesis: for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (STC N) holds
[T,f2,p] in the Instructions of (STC N)
let f1, f2 be Function; :: thesis: for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (STC N) holds
[T,f2,p] in the Instructions of (STC N)
let p be set ; :: thesis: ( f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (STC N) implies [T,f2,p] in the Instructions of (STC N) )
assume f1 in JumpParts T ; :: thesis: ( not f2 in product (product" (JumpParts T)) or not [T,f1,p] in the Instructions of (STC N) or [T,f2,p] in the Instructions of (STC N) )
then A: f1 in {0 } by Th19;
assume Z: f2 in product (product" (JumpParts T)) ; :: thesis: ( not [T,f1,p] in the Instructions of (STC N) or [T,f2,p] in the Instructions of (STC N) )
product" (JumpParts T) = {} by Th19, CARD_3:156;
then ( f1 = 0 & f2 = 0 ) by A, Z, CARD_3:19, TARSKI:def 1;
hence ( not [T,f1,p] in the Instructions of (STC N) or [T,f2,p] in the Instructions of (STC N) ) ; :: thesis: verum