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 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 Lm1;
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 (Trivial-AMI 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 (Trivial-AMI N) or [T,b₂,b₃] in the Instructions of (Trivial-AMI 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 (Trivial-AMI N) or [T,f2,b₁] in the Instructions of (Trivial-AMI 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 (Trivial-AMI N) or [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 A1: f1 in {0} by Lm2;
assume A2: 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 Lm2, 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 (Trivial-AMI N) or [T,f2,p] in the Instructions of (Trivial-AMI N) ) ; :: thesis: verum