Description: In the recursive scheme
"(n+1)-xor" <-> if- ( ph , -. "n-xor" , "n-xor" )
we set n = 0 to formally arrive at an expression for "1-xor". The base case "0-xor" is replaced with F. , as a sequence of 0 inputs never has an odd number being part of it. (Contributed by Wolf Lammen, 11-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-1xor | |- ( if- ( ps , -. F. , F. ) <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tbtru | |- ( ps <-> ( ps <-> T. ) ) |
|
2 | 1 | biimpi | |- ( ps -> ( ps <-> T. ) ) |
3 | notfal | |- ( -. F. <-> T. ) |
|
4 | 2 3 | bitr4di | |- ( ps -> ( ps <-> -. F. ) ) |
5 | nbfal | |- ( -. ps <-> ( ps <-> F. ) ) |
|
6 | 5 | biimpi | |- ( -. ps -> ( ps <-> F. ) ) |
7 | 4 6 | casesifp | |- ( ps <-> if- ( ps , -. F. , F. ) ) |
8 | 7 | bicomi | |- ( if- ( ps , -. F. , F. ) <-> ps ) |