take Trivial-AMI N ; :: thesis: Trivial-AMI N is halting
thus Trivial-AMI N is halting ; :: thesis: verum