x := (t,A) in ElementaryInstructions A by Th68;
hence x := (t,A) is absolutely-terminating by AOFA_000:95; :: thesis: verum