thus STC N is with_explicit_jumps :: thesis: ( STC N is without_implicit_jumps & STC N is regular )

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 AMISTD_2:def 6 :: thesis: ( f in JUMP I implies ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) )
thus ( f in JUMP I implies ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) ) ; :: thesis: verum

end;

thus STC N is without_implicit_jumps :: thesis: STC N is regular

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 AMISTD_2:def 7 :: thesis: ( ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) implies f in JUMP I )
the Instructions of (STC N) = {[0 ,0 ],[1,0 ]} by AMISTD_1:def 11;
then ( I = [0 ,0 ] or I = [1,0 ] ) by TARSKI:def 2;
hence ( ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = NAT ) implies f in JUMP I ) by MCART_1:def 2, RELAT_1:60; :: thesis: verum

end;

let T be InsType of (STC N); :: according to AMISTD_2:def 11 :: thesis: AddressParts T is product-like
take {} ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product {}
thus AddressParts T = product {} by Th19, CARD_3:19; :: thesis: verum