c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig TruthMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true' : bool.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true1 : ded true' eq 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view TruthMODView : Truth -> TruthMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true := true'.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig FalsityMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false' : bool.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false0 : ded false' eq 0.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view FalsityMODView : Falsity -> FalsityMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false := false'.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig NEGMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not' : elem (bool' → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not1 : ded ((A eq 0) imp ((not' @ A) eq 1)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not0 : ded ((A eq 1) imp ((not' @ A) eq 0)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not'' : bool -> bool
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [A] not' @ A.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not1' : ded (A eq 0) -> ded (not'' A) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE not1 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not0' : ded A eq 1 -> ded (not'' A) eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE not0 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view NEGMODView : NEG -> NEGMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not := [A : bool] not' @ A.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig DISJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or' : elem (bool' → bool' → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or1 : ded (((A eq 1) or (B eq 1)) imp (((or' @ A) @ B) eq 1)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or0 : ded (((A eq 0) and (B eq 0)) imp (((or' @ A) @ B) eq 0)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or'' : bool -> bool -> bool
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [A][B] or' @ A @ B. %infix left 10 or''.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or1' : ded (A eq 1) or (B eq 1) -> ded (A or'' B) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q : ded (A eq 1)] impE or1 p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r : ded (B eq 1)] impE or1 p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or0' : ded (A eq 0) and (B eq 0) -> ded (A or'' B) eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE or0 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view DISJMODView : DISJ -> DISJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or := [A][B] (or' @ A) @ B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig CONJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and' : elem (bool' → bool' → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1 : ded (((A eq 1) and (B eq 1)) imp (((and' @ A) @ B) eq 1)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and0 : ded (((A eq 0) or (B eq 0)) imp (((and' @ A) @ B) eq 0)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and'' : bool -> bool -> bool
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [A][B] and' @ A @ B. %infix left 10 and''.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1' : ded A eq 1 and B eq 1 -> ded (A and'' B) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE and1 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and0' : ded A eq 0 or B eq 0 -> ded (A and'' B) eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE and0 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view CONJMODView : CONJ -> CONJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and := [A][B] (and' @ A) @ B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig IMPMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMOD %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp' : elem (bool' → bool' → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp1 : ded (((A eq 0) or (B eq 1)) imp (((imp' @ A) @ B) eq 1)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp0 : ded (((A eq 1) and (B eq 0)) imp (((imp' @ A) @ B) eq 0)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp'' : bool -> bool -> bool
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [A][B] (imp' @ A) @ B. %infix right 15 imp''.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp1' : ded A eq 0 or B eq 1 -> ded (A imp'' B) eq 1
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE imp1 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp0' : ded A eq 1 and B eq 0 -> ded (A imp'' B) eq 0
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder = [p] impE imp0 p.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view IMPMODView : IMP -> IMPMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BaseMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp := [A][B] imp' @ A @ B.