Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-df3maxtru1 Structured version   Visualization version   GIF version

Theorem wl-df3maxtru1 34902
Description: Assuming "(n+1)-maxtru1" ↔ ¬ "(n+1)-mintru-2", we can deduce from the recursion formula given in wl-df-3mintru2 34894, 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.)

Assertion
Ref Expression
wl-df3maxtru1 (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 𝜒), (𝜓𝜒)))

Proof of Theorem wl-df3maxtru1
StepHypRef Expression
1 cadnot 1617 . 2 (¬ cadd(𝜑, 𝜓, 𝜒) ↔ cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒))
2 wl-df-3mintru2 34894 . 2 (cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)))
3 ifpn 1069 . . 3 (if-(𝜑, (𝜓 𝜒), (𝜓𝜒)) ↔ if-(¬ 𝜑, (𝜓𝜒), (𝜓 𝜒)))
4 nanor 1486 . . . . . 6 ((𝜓𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒))
54a1i 11 . . . . 5 (⊤ → ((𝜓𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒)))
6 df-nor 1522 . . . . . . 7 ((𝜓 𝜒) ↔ ¬ (𝜓𝜒))
7 ioran 981 . . . . . . 7 (¬ (𝜓𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
86, 7bitri 278 . . . . . 6 ((𝜓 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
98a1i 11 . . . . 5 (⊤ → ((𝜓 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒)))
105, 9ifpbi23d 1077 . . . 4 (⊤ → (if-(¬ 𝜑, (𝜓𝜒), (𝜓 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒))))
1110mptru 1545 . . 3 (if-(¬ 𝜑, (𝜓𝜒), (𝜓 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)))
123, 11bitr2i 279 . 2 (if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)) ↔ if-(𝜑, (𝜓 𝜒), (𝜓𝜒)))
131, 2, 123bitri 300 1 (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 𝜒), (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  wo 844  if-wif 1058  wnan 1482   wnor 1521  wtru 1539  caddwcad 1608
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 210  df-an 400  df-or 845  df-ifp 1059  df-3or 1085  df-3an 1086  df-nan 1483  df-xor 1503  df-nor 1522  df-tru 1541  df-cad 1609
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator