consider a, b being read-write Int-Location ;
( a := b is good & a := b is parahalting ) ;
hence ex b₁ being Instruction of SCM+FSA st
( b₁ is good & b₁ is parahalting ) ; :: thesis: verum