thus STC N is with_explicit_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 2 :: thesis: I is with_explicit_jumps
the Instructions of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then ( I = [0,0,0] or I = [1,0,0] ) by TARSKI:def 2;
hence JUMP I = rng (JumpPart I) by RECDEF_2:def 2, RELAT_1:38; :: according to AMISTD_2:def 1 :: 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 COMPOS_1:def 12 :: thesis: ( not InsCode I = InsCode J or dom (JumpPart I) = dom (JumpPart J) )
( JumpPart I = {} & JumpPart J = {} ) by Th17;
hence ( not InsCode I = InsCode J or 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 COMPOS_1:def 14 :: thesis: for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT )
JumpPart I = {} by Th17;
hence for b₁ being set holds
( not b₁ in dom (JumpPart I) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis: verum

end;

let T be InsType of (STC N); :: according to COMPOS_1:def 15 :: thesis: for b₁, b₂ being set
for b₃ being set holds
( not b₁ in JumpParts T or not b₂ in product (product" (JumpParts T)) or not [T,b₁,b₃] in the Instructions of (STC N) or [T,b₂,b₃] in the Instructions of (STC N) )
let f1, f2 be Function; :: thesis: for b₁ being set holds
( not f1 in JumpParts T or not f2 in product (product" (JumpParts T)) or not [T,f1,b₁] in the Instructions of (STC N) or [T,f2,b₁] in the Instructions of (STC N) )
let p be set ; :: thesis: ( not f1 in JumpParts T or 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) )
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 A1: f1 in {0} by Th19;
assume A2: 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:106;
then ( f1 = 0 & f2 = 0 ) by A1, A2, CARD_3:10, 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