![]() |
Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-df3maxtru1 | Structured version Visualization version GIF version |
Description: Assuming
"(n+1)-maxtru1" ↔ ¬
"(n+1)-mintru-2", we can deduce from
the recursion formula given in wl-df-3mintru2 37016, that a similiar one
"(n+1)-maxtru1" ↔ if-(𝜑,-. "n-mintru-1" , "n-maxtru1" ) is valid for expressing 'at most one input is true'. This can also be rephrased as a mutual exclusivity of propositional expressions (no two of a sequence of inputs can simultaniously be true). Of course, this suggests that all inputs depend on variables 𝜂, 𝜁... Whatever wellformed expression we plugin for these variables, it will render at most one of the inputs true. The here introduced mutual exclusivity is possibly useful for case studies, where we want the cases be sort of 'disjoint'. One can further imagine that a complete case scenario demands that the 'at most' is sharpened to 'exactly one'. This does not impose any difficulty here, as one of the inputs will then be the negation of all others be or'ed. As one input is determined, 'at most one' is sufficient to describe the general form here. Since cadd is an alias for 'at least 2 out of three are true', its negation is under focus here. (Contributed by Wolf Lammen, 23-Jun-2024.) |
Ref | Expression |
---|---|
wl-df3maxtru1 | ⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cadnot 1608 | . 2 ⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒)) | |
2 | wl-df-3mintru2 37016 | . 2 ⊢ (cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒))) | |
3 | ifpn 1071 | . . 3 ⊢ (if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)) ↔ if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒))) | |
4 | nanor 1488 | . . . . . 6 ⊢ ((𝜓 ⊼ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒)) | |
5 | 4 | a1i 11 | . . . . 5 ⊢ (⊤ → ((𝜓 ⊼ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒))) |
6 | df-nor 1522 | . . . . . . 7 ⊢ ((𝜓 ⊽ 𝜒) ↔ ¬ (𝜓 ∨ 𝜒)) | |
7 | ioran 981 | . . . . . . 7 ⊢ (¬ (𝜓 ∨ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒)) | |
8 | 6, 7 | bitri 274 | . . . . . 6 ⊢ ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒)) |
9 | 8 | a1i 11 | . . . . 5 ⊢ (⊤ → ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))) |
10 | 5, 9 | ifpbi23d 1077 | . . . 4 ⊢ (⊤ → (if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)))) |
11 | 10 | mptru 1540 | . . 3 ⊢ (if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒))) |
12 | 3, 11 | bitr2i 275 | . 2 ⊢ (if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒))) |
13 | 1, 2, 12 | 3bitri 296 | 1 ⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 ∨ wo 845 if-wif 1060 ⊼ wnan 1484 ⊽ wnor 1521 ⊤wtru 1534 caddwcad 1599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ifp 1061 df-3or 1085 df-3an 1086 df-nan 1485 df-xor 1505 df-nor 1522 df-tru 1536 df-cad 1600 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |