Description: Using the recursion formula
"(n+1)-mintru-(m+1)" <-> if- ( ph , "n-mintru-m" , "n-mintru-(m+1)" )
for "2-mintru-1" (meaning "at least 1 out of 2 inputs is true") by plugging in n = 1, m = 0, and simplifying. The expression "1-mintru-0" is a base case (meaning at least zero inputs out of 1 are true), evaluating to T. , and wl-1mintru1 shows "1-mintru-1" is equivalent to the only input.
Negating an "n-mintru1" operation means: All n inputs ph .. th are false. This is also conveniently expressed as -. ( ph \/ .. \/ th ) , in accordance with the result here. (Contributed by Wolf Lammen, 10-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-2mintru1 | ⊢ ( if- ( 𝜓 , ⊤ , 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfifp3 | ⊢ ( if- ( 𝜓 , ⊤ , 𝜒 ) ↔ ( ( 𝜓 → ⊤ ) ∧ ( 𝜓 ∨ 𝜒 ) ) ) | |
2 | trud | ⊢ ( 𝜓 → ⊤ ) | |
3 | 2 | bitru | ⊢ ( ( 𝜓 → ⊤ ) ↔ ⊤ ) |
4 | 3 | anbi1i | ⊢ ( ( ( 𝜓 → ⊤ ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ⊤ ∧ ( 𝜓 ∨ 𝜒 ) ) ) |
5 | truan | ⊢ ( ( ⊤ ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜓 ∨ 𝜒 ) ) | |
6 | 1 4 5 | 3bitri | ⊢ ( if- ( 𝜓 , ⊤ , 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) |