take Trivial-AMI N ; :: thesis: ( Trivial-AMI N is without_implicit_jumps & Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is halting & Trivial-AMI N is realistic )
thus ( Trivial-AMI N is without_implicit_jumps & Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is halting & Trivial-AMI N is realistic ) ; :: thesis: verum