take
Trivial-AMI N
; :: thesis: ( Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is halting )

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

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