- R соңғы шартының функциясы бетінде қарастырылатын предикаттар түрлендірушісімен бірнеше анықталған қасиеттерге ие.
Қасиет 1. Кез келген S конструкциясы үшін
WP (S,F)=F
Айталық, бұл теңдік орындалмасын. Мұндай WP (S,F) шартын қанағаттандыратын ең болмаса бір жағдай табылар еді. Бұл жағдайда Sконструкциясының бастапқы жағдайы ретінде аламыз. Анықтамаға сәйкесS-і іске қосу F предикатын қанағаттандырады соңғы жағдайға әкеледі. Бірақ бұл жерде қарама-қайшылық туады, F предикатының анықтамасы бойынша F-і қанағаттандыратын жағдайжоқ, осылайша (4) қатынасты дәлелдейді.
Қасиет 2. Кез-келген S конструкциясы және барлық жағдайлар үшін (5)Q=>R қатынасы орындалатын Q, R соңғы шарттары үшін мына қатынас орындалады.
WP(S,Q)=> WP(S,R)(6)
Шындығында, WP(S,Q) –і үшін қанағаттандыратын кез келген бастапқы жағдайда жүйе жұмысының ақырғы жағдайы үшін анықтама бойынша Q орындалады. (5) қатынасын ескерсекR-ң де орындалатындығы келіп шығады. Демек, берілген бастапқы жағдай бір мезгілде WP(S,R) шартын да қанағаттандыратын болады, (6)-да көрсетілгендей қасиет-2 бұл монотондық қасиет.
- Қасиет 3. Кез келген S конструкциясы және Q және R соңғы шарттар үшін WP(S,Q) andWP(S,R) = WP(S,Q and R)(7) ќатынасы орындалады. [and =]
Жағдайлар кеңестігінің кез келген нүктесінде(7) –ң сол жағынан оң жағы келіп шығады, өйткені WP(S,Q) және WP(S,R) –ді қанағаттандыратын кез келген бастапқы жағдайлар үшін Q және R-ді қанағаттандыратын жағдайдың болатындығын білеміз. Одан әрі анықтамаға сәйкес барлық жағдайлар үшін
(Q and R)=>Q
ќасиет 2-ні ескеріп барлық жағдайлар үшінWP(S,Q and R )=> WP(S,Q)
дәл осылай барлық жағдайлар үшінWP(S,Q and R )=> WP(S,R) бола алады. Бірақ A=>B және A=>C болса, ондаA=>(B and C) деуімізге болады. Сондықтан жағдайлар кеңіәстігінің кез келген нүктесінде (7) –ң оң жағынан сол жағы келіп шығады. Екі жақта барлық жерде бірінен — бірі келіп шығатындықтан олар тең болу керек. Осылай 3-қасиетдәлелденеді.
- Қасиет 4. Кез келген Sконструкциясы үшін және кез келген Q және R соңғы шарттар үшін(WP(S,Q or R )=> WP(S,R))=> WP(S,Q or R ) (8) қатынасы барлық жағдайлар үшін ақиқат болады.
Анықтамаға сәйкес барлық жағдайлар үшін WP(S,Q )=> WP(S,Q or R) дәл осылай WP(S,R )=> WP(S,Q or R) барлық жағдайда A=>C және B=>C үшін (A or B)=>C деуге болады. Осылай (8) қатынастың ақиқат екендігі дәлелденеді.
Қасиет 4’. Кез келген детерминерленген S конструкциясы кез келген Q және Rсоңғы шарттар үшін
(WP(S,Q ) or WP (S,R))=WP(S,Q or R) (8)
Бұл қатынастың енді оң жағынан сол жағы келіп шығатынын көрсету қажет. WP(S,Q or R ) алғы шартын қанағаттандыратын қайсы бір бастапқы жағдайда қарастырайық, бұл бастапқы жағдайға жалғыз ғана ақырғы жағдай сәйкес келеді. Ол Q- ді R-ді не екеуінде қанағаттандыруы мүмкін, бұдан шығатыны бастапқы жағдай WP(S,Q) –ді не WP(S,R)-ді не екеуінде, яғни ол WP(S,Q) or WP(S,R)-ді қанағаттандыруы керек. Сонымен 4’-қасиет дәлелденді. [детерминерленген машина үшін конструкцияны іске қосқанда кейінгі оқиғалар толығымен оның бастапқы жағдайымен анықталады. Бірдей бастапқы жағдайда екі мәрте қайталап іске түсірсек, бірдей оқиғалар жүреді деп айта алмаймыз. Мүмкін болған оқиғалар класының қайсы бір оқиғасы жүреді]. F арқылы жағдайлар кеңестігінің барлық нүктесінде жалған болатын предикатын белгілейміз; ол бос жиынға сәйкес келеді.