take Trivial-AMI IL,N ; :: thesis: ( Trivial-AMI IL,N is halting & Trivial-AMI IL,N is realistic & Trivial-AMI IL,N is steady-programmed & Trivial-AMI IL,N is programmable & Trivial-AMI IL,N is with_explicit_jumps & Trivial-AMI IL,N is without_implicit_jumps & Trivial-AMI IL,N is Exec-preserving )
thus ( Trivial-AMI IL,N is halting & Trivial-AMI IL,N is realistic & Trivial-AMI IL,N is steady-programmed & Trivial-AMI IL,N is programmable & Trivial-AMI IL,N is with_explicit_jumps & Trivial-AMI IL,N is without_implicit_jumps & Trivial-AMI IL,N is Exec-preserving ) ; :: thesis: verum