check that MCS invariants imply orphanage invariants

[lsf37]

The "Orphanage" theory in the Refine session was added to make sure that thread states correspond to the scheduler queues, i.e. that no running threads can become orphaned by being left out of the scheduler queues.

AFAIR, the standard MCS invariants already include this property (and on the abstract spec level already, because these queues are now visible there), but I'm not sure we state this in a form that is obviously equivalent with no_orphans.

For reference no_orphans is

 ∀ tcb_ptr.
         tcb_ptr : all_active_tcb_ptrs s
         ⟶
         tcb_ptr = ksCurThread s ∨ tcb_ptr : all_queued_tcb_ptrs s ∨
         ksSchedulerAction s = SwitchToThread tcb_ptr

This issue is for checking what the actual status is and potentially adding a lemma to the abstract invariants in MCS that show something like invs s ==> no_orphans s