현재 프로그램의 정확성을 알기 위해 Hoare 논리를 연구 중입니다. 특히, 나는 Hoare logic을 읽고 있어요 그리고 나는 동안 규칙에서 다음 예제를 분석하고 있습니다 : 
Hoare의 논리에서 {x <= 10^x <10}이 {x <= 10} 대신 {x <10}으로 단순화 된 이유는 무엇입니까?
단순화 단계에 대해 무엇을 알고 싶은 것입니다 : {x <= 10^x < 10}이 {x < 10} 대신 {x <= 10} 단순화 왜?
조건문은 "조건 1 AND 조건 2"입니다. 여기서 조건 2 (<)는 조건 1 (<=)보다 제한적입니다.
확실히 (AND로 인해) 두 가지를 모두 만족하는 항목은 더 제한적인 항목을 충족해야합니다.
따라서 더 제한적인 조건 만 사용하면됩니다. 다른 조건은 불필요합니다.
다른 방법으로 넣어 : <=와 < 사이의 유일한 차이는 == 경우입니다. == 사례를 만족하는 항목은 더 제한적인 < 사례를 충족시킬 수 없으므로이를 확인하지 않습니다.
순수한 수학/논리 질문에 대해서는 https://math.stackexchange.com/을 확인하십시오.
새로운 태블릿을 선택하고 (1) 큰 화면과 (2) 20cm보다 큰 화면을 갖고 싶다고 가정 해 보겠습니다. 첫 번째 조건은 두 번째 조건이 참일 때만 유효하기 때문에 첫 번째 조건을 명확하게 파기 할 수 있습니다.
"큰 화면"조건은 x <= 10이고 "20cm보다 큰 화면"은 x < 10입니다. 두 경우를 모두 만족하는도 x < 10을 만족합니다. 보다 "편안한"상태 인 x <= 10은 버려 질 수 있습니다.
'x = 10' 인 경우를 고려하십시오. 이것은 원래 조건이나 단순화 된 버전을 충족시키지 못하지만 귀하의 요구를 충족시킵니다. 'x <= 10/\ x <10'은'(x <10 \/x = 10)/\ x <10'과 ('<='의 def에 의해) (x = 10/\ x <10)'(x = 10/\ x <10)'(배포본)은'x <10 \/\/_ | _' (둘 다 작거나 같을 수는 없습니다)는'x <10' (분리의 동일성)과 같습니다. –