Solution (in retrospect this should’ve been posted a few years earlier):
let’Na’ = box N contains angry frog’Ng’ = N gold’Nf’ = N’s inscription false’Nt’ = N’s inscription trueconsistent states must have 1f 2t or 1t 2f, and 1a 2g or 1g 2athen:1a 1t, 2g 2f ⇒ 1t, 2f1a 1f, 2g 2t ⇒ 1f, 2t1g 1t, 2a 2f ⇒ 1t, 2t1g 1f, 2a 2t ⇒ 1f, 2f
Solution (in retrospect this should’ve been posted a few years earlier):
let
’Na’ = box N contains angry frog
’Ng’ = N gold
’Nf’ = N’s inscription false
’Nt’ = N’s inscription true
consistent states must have 1f 2t or 1t 2f, and 1a 2g or 1g 2a
then:
1a 1t, 2g 2f ⇒ 1t, 2f
1a 1f, 2g 2t ⇒ 1f, 2t
1g 1t, 2a 2f ⇒ 1t, 2t
1g 1f, 2a 2t ⇒ 1f, 2f