thus Trivial-AMI N is regular :: thesis: Trivial-AMI N is J/A-independent

proof

let I be Instruction of (Trivial-AMI 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 Lm3;
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 (Trivial-AMI 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 (Trivial-AMI N) holds
[T,f2,p] in the Instructions of (Trivial-AMI 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 (Trivial-AMI N) holds
[T,f2,p] in the Instructions of (Trivial-AMI N)
let p be set ; :: thesis: ( f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (Trivial-AMI N) implies [T,f2,p] in the Instructions of (Trivial-AMI N) )
assume f1 in JumpParts T ; :: thesis: ( not f2 in product (product" (JumpParts T)) or not [T,f1,p] in the Instructions of (Trivial-AMI N) or [T,f2,p] in the Instructions of (Trivial-AMI N) )
then A: f1 in {0 } by Lm4;
assume Z: f2 in product (product" (JumpParts T)) ; :: thesis: ( not [T,f1,p] in the Instructions of (Trivial-AMI N) or [T,f2,p] in the Instructions of (Trivial-AMI N) )
product" (JumpParts T) = {} by Lm4, 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 (Trivial-AMI N) or [T,f2,p] in the Instructions of (Trivial-AMI N) ) ; :: thesis: verum