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