Fix some atom of information. It’s contained in some of Lambda, X1, X2, and Lambda’. Call the corresponding four statements a,b,c,d. Then you assume “b&c implies a, c&d implies b, b&d implies c, a&d implies b or c.”.
These compress into “b&c implies a, d implies a=b=c.”; after concluding that, I read that you conclude “d&(b or c) implies a”, which seems to be a special case. My approach feels too gainfully simpler, so I’m checking in to ask whether it fails.
Fix some atom of information. It’s contained in some of Lambda, X1, X2, and Lambda’. Call the corresponding four statements a,b,c,d. Then you assume “b&c implies a, c&d implies b, b&d implies c, a&d implies b or c.”.
These compress into “b&c implies a, d implies a=b=c.”; after concluding that, I read that you conclude “d&(b or c) implies a”, which seems to be a special case. My approach feels too gainfully simpler, so I’m checking in to ask whether it fails.
Just pasting this into a calculator your expressions don’t seem to be equivalent:
first expression e1: (((b∧c)=>a) ∧ ((c ∧ d) ⇒ b) ∧ (d ∧ b ⇒ c) ∧ ((a ∧ d) =>(b or c)))
second expression e2: ((b∧c)=>a)∧(d =>((a=b)=c))
e1 = e2: (a ∧ b) ∨ (a ∧ c) ∨ (b ∧ c) ∨ ¬ d
e1 simplifies to (a ∧ b ∧ c) ∨ (¬ a ∧ ¬ b ∧ ¬ c) ∨ (¬ b ∧ ¬ d) ∨ (¬ c ∧ ¬ d)
For e2 I think you want ((b∧c)=>a)∧(d =>((a=b)∧(a=c)))
Oops!