Theorems about unless 3
Dôsledok 3.
[p unless q ? r] ? [p ? ?q unless q ? r]
Dôkaz: Predpokladajme „p unless q ? r”.
- antireflexivita: ?q unless q
- jednoduchá konjukcia: p ? ?q unless q ? r
Naopak, predpokladajme “p ? ?q unless q ? r”
- z dôsledku 1: p ? q unless q
- jednoduchá disjunkcia: p unless q ? r
Dôsledok 4. („Prešmyk“)
p ? q unless r / p unless q ? r
Dôkaz:
p ? q unless r /* predpoklad */
? q unless q /* antireflexívnost */
p ? ?q unless q ? r /* jednoduchá konjunkcia */
p unless q ? r /* z dôsledku 3. */
Dôsledok 5.
??j::pj unless pj ? qj? / ??j::pj ? unless ??j::pj????j::qj?
Dôkaz: indukciou, IP (N = 2) pouzitím konjukcie