take Trivial-AMI N ; :: thesis: ( Trivial-AMI N is halting & Trivial-AMI N is steady-programmed & Trivial-AMI N is realistic & Trivial-AMI N is strict )
thus ( Trivial-AMI N is halting & Trivial-AMI N is steady-programmed & Trivial-AMI N is realistic & Trivial-AMI N is strict ) ; :: thesis: verum