HOL Lightは，あるtermが別のtermと等価である（:numなどの場合は=，:boolの場合はで結ばれる）ことを，体系的な変形を経て示す為，様々なconversionsを提供します． conversionはterm -> thm typeの関数で，typeはARITH_RULEやMESON[]などのproverと同じで…

量化子のネストにおいて変数の依存関係に注意が必要であることは，連続と一様連続との違いを持ち出すまでもなく，明らかでしょう． さて，先に述べたトートロジーprover TAUTでは，自明でない量化された式の評価はできません，HOL Light には，model elimina…