module Tautology-Hard imports libstratego-lib signature constructors tt : Prop ff : Prop and : Prop * Prop -> Prop xor : Prop * Prop -> Prop 'not : Prop -> Prop or : Prop * Prop -> Prop implies : Prop * Prop -> Prop iff : Prop * Prop -> Prop a : Prop b : Prop c : Prop d : Prop e : Prop a1 : Prop a2 : Prop a3 : Prop a4 : Prop a5 : Prop a6 : Prop a7 : Prop a8 : Prop a9 : Prop a10 : Prop a11 : Prop a12 : Prop a13 : Prop a14 : Prop a15 : Prop a16 : Prop a17 : Prop a18 : Prop strategies main = ( implies( and( iff( iff( or(a1(), a2()) , or( 'not(a3()) , iff( xor(a4(), a5()) , 'not('not('not(a6()))) ) ) ) , 'not( and( and(a7(), a8()) , 'not( xor( xor( or( a9() , and(a10(), a11()) ) , a2() ) , and( and( a11() , xor( a2() , iff(a5(), a5()) ) ) , xor( xor(a7(), a7()) , iff(a9(), a4()) ) ) ) ) ) ) ) , implies( iff( iff( or(a1(), a2()) , or( 'not(a3()) , iff( xor(a4(), a5()) , 'not('not('not(a6()))) ) ) ) , 'not( and( and(a7(), a8()) , 'not( xor( xor( or( a9() , and(a10(), a11()) ) , a2() ) , and( and( a11() , xor( a2() , iff(a5(), a5()) ) ) , xor( xor(a7(), a7()) , iff(a9(), a4()) ) ) ) ) ) ) ) , 'not( and( implies( and(a1(), a2()) , 'not( xor( or( or( xor( implies( and(a3(), a4()) , implies(a5(), a6()) ) , or(a7(), a8()) ) , xor( iff(a9(), a10()) , a11() ) ) , xor( xor(a2(), a2()) , a7() ) ) , iff( or(a4(), a9()) , xor('not(a6()), a6()) ) ) ) ) , 'not( iff( 'not(a11()) , 'not(a9()) ) ) ) ) ) ) , 'not( and( implies( and(a1(), a2()) , 'not( xor( or( or( xor( implies( and(a3(), a4()) , implies(a5(), a6()) ) , or(a7(), a8()) ) , xor( iff(a9(), a10()) , a11() ) ) , xor( xor(a2(), a2()) , a7() ) ) , iff( or(a4(), a9()) , xor('not(a6()), a6()) ) ) ) ) , 'not( iff( 'not(a11()) , 'not(a9()) ) ) ) ) ) ; implies( and( 'not( and( xor( a1() , xor( or(a2(), a3()) , a4() ) ) , xor( iff( xor( 'not(a5()) , or( xor( iff(a6(), a7()) , iff(a8(), a9()) ) , and(a10(), a9()) ) ) , iff( 'not('not(a2())) , implies( or(a9(), a6()) , or(a10(), a5()) ) ) ) , 'not( or( a9() , implies( 'not(a8()) , or(a4(), a9()) ) ) ) ) ) ) , implies( 'not( and( xor( a1() , xor( or(a2(), a3()) , a4() ) ) , xor( iff( xor( 'not(a5()) , or( xor( iff(a6(), a7()) , iff(a8(), a9()) ) , and(a10(), a9()) ) ) , iff( 'not('not(a2())) , implies( or(a9(), a6()) , or(a10(), a5()) ) ) ) , 'not( or( a9() , implies( 'not(a8()) , or(a4(), a9()) ) ) ) ) ) ) , 'not( implies( implies( and( or( a1() , xor( xor(a2(), a3()) , 'not(a4()) ) ) , 'not( xor( a5() , and(a6(), a7()) ) ) ) , implies( xor( implies(a8(), a9()) , a10() ) , xor( and( a4() , or(a4(), a1()) ) , a2() ) ) ) , or( or( xor( or(a4(), a7()) , a2() ) , and(a8(), a1()) ) , 'not('not('not(a6()))) ) ) ) ) ) , 'not( implies( implies( and( or( a1() , xor( xor(a2(), a3()) , 'not(a4()) ) ) , 'not( xor( a5() , and(a6(), a7()) ) ) ) , implies( xor( implies(a8(), a9()) , a10() ) , xor( and( a4() , or(a4(), a1()) ) , a2() ) ) ) , or( or( xor( or(a4(), a7()) , a2() ) , and(a8(), a1()) ) , 'not('not('not(a6()))) ) ) ) ) ; implies( and( 'not( and( xor( a1() , xor( or(a2(), a3()) , a4() ) ) , xor( iff( xor( 'not(a5()) , or( xor( iff(a6(), a7()) , iff(a8(), a9()) ) , and(a10(), a11()) ) ) , implies( or( a4() , and( a3() , iff(a1(), a2()) ) ) , 'not('not(a4())) ) ) , xor( implies( implies(a6(), a1()) , 'not(a1()) ) , 'not(a9()) ) ) ) ) , implies( 'not( and( xor( a1() , xor( or(a2(), a3()) , a4() ) ) , xor( iff( xor( 'not(a5()) , or( xor( iff(a6(), a7()) , iff(a8(), a9()) ) , and(a10(), a11()) ) ) , implies( or( a4() , and( a3() , iff(a1(), a2()) ) ) , 'not('not(a4())) ) ) , xor( implies( implies(a6(), a1()) , 'not(a1()) ) , 'not(a9()) ) ) ) ) , 'not( implies( implies( and( or( a1() , xor( xor(a2(), a3()) , 'not(a4()) ) ) , 'not( xor( a5() , and(a6(), a7()) ) ) ) , implies( xor( implies(a8(), a9()) , a10() ) , xor( and( a11() , implies(a2(), a8()) ) , a8() ) ) ) , 'not( or( implies( or( a5() , or( a8() , and(a8(), a9()) ) ) , 'not(a2()) ) , 'not(a7()) ) ) ) ) ) ) , 'not( implies( implies( and( or( a1() , xor( xor(a2(), a3()) , 'not(a4()) ) ) , 'not( xor( a5() , and(a6(), a7()) ) ) ) , implies( xor( implies(a8(), a9()) , a10() ) , xor( and( a11() , implies(a2(), a8()) ) , a8() ) ) ) , 'not( or( implies( or( a5() , or( a8() , and(a8(), a9()) ) ) , 'not(a2()) ) , 'not(a7()) ) ) ) ) ) ; id) ; 0 rewrite = \ and(P, tt()) -> P \ <+ \ and(P, ff()) -> ff() \ <+ \ and(P, P) -> P \ <+ \ xor(P, ff()) -> P \ <+ \ xor(P, P) -> ff() \ <+ \ and(P, xor(Q, R)) -> xor( and(P, Q) , and(P, R) ) \ <+ \ 'not(P) -> xor(P, tt()) \ <+ \ or(P, Q) -> xor( and(P, Q) , xor(P, Q) ) \ <+ \ implies(P, Q) -> 'not( xor(P, and(P, Q)) ) \ <+ \ iff(P, Q) -> 'not(xor(P, Q)) \ <+ \ and(tt(), P) -> P \ <+ \ and(ff(), P) -> ff() \ <+ \ and(P, P) -> P \ <+ \ xor(ff(), P) -> P \ <+ \ xor(P, P) -> ff() \ <+ \ and(xor(Q, R), P) -> xor( and(P, Q) , and(P, R) ) \ <+ \ or(Q, P) -> xor( and(P, Q) , xor(P, Q) ) \ <+ \ iff(Q, P) -> 'not(xor(P, Q)) \ <+ fail rewrite-all = not(is-list) ; (flatten-subterms <+ ?input ; (![] ; try( ![<\ and(P, tt()) -> P \> input|] ) ; try( ![<\ and(P, ff()) -> ff() \> input|] ) ; try( ![<\ and(P, P) -> P \> input|] ) ; try( ![<\ xor(P, ff()) -> P \> input|] ) ; try( ![<\ xor(P, P) -> ff() \> input|] ) ; try( ![<\ and(P, xor(Q, R)) -> xor( and(P, Q) , and(P, R) ) \> input|] ) ; try( ![<\ 'not(P) -> xor(P, tt()) \> input|] ) ; try( ![<\ or(P, Q) -> xor( and(P, Q) , xor(P, Q) ) \> input|] ) ; try( ![<\ implies(P, Q) -> 'not( xor(P, and(P, Q)) ) \> input|] ) ; try( ![<\ iff(P, Q) -> 'not(xor(P, Q)) \> input|] ) ; try( ![<\ and(tt(), P) -> P \> input|] ) ; try( ![<\ and(ff(), P) -> ff() \> input|] ) ; try( ![<\ and(P, P) -> P \> input|] ) ; try( ![<\ xor(ff(), P) -> P \> input|] ) ; try( ![<\ xor(P, P) -> ff() \> input|] ) ; try( ![<\ and(xor(Q, R), P) -> xor( and(P, Q) , and(P, R) ) \> input|] ) ; try( ![<\ or(Q, P) -> xor( and(P, Q) , xor(P, Q) ) \> input|] ) ; try( ![<\ iff(Q, P) -> 'not(xor(P, Q)) \> input|] ) ; id) ; make-set ; not([]) ; try(?[])) flatten-subterms = one(is-list) ; ?name#() ; rec rec ( {?[args|tail] ; all-tails := tail ; <(flatten-list ; make-set)> args ; mapconcat( {head: ?head ; ])> all-tails } ) <+ ?[arg1|tail] ; all-tails := tail ; map(![arg1|]) <+ \ [] -> [[]] \} ) ; map(!name#()) rec-normal-form-main = debug(!"Normal form of: ") ; rec-normal-form ; debug(!"is: ") rec-normal-form = memo(innermost(rewrite)) rec-all-normal-forms = debug(!"All normal forms of: ") ; innermost(rewrite-all) ; (is-list <+ ![]) ; flatten-list ; make-set ; debug(!"are: ") rec-rewrites-to = debug(!"Rewrites to: ") ; (rec-normal-form, id) ; if eq then rec-rewrites-yes else Fst ; rec-rewrites-no end rec-equals = debug(!"Equals: ") ; if eq then rec-rewrites-yes else (rec-normal-form, id) ; if eq then rec-rewrites-yes else (id, rec-normal-form) ; if eq then rec-rewrites-yes else rec-rewrites-no end end end rec-rewrites-yes = !"yes" ; say(id) rec-rewrites-no = debug(!"no: ") ; !"no" repeat-memo(the-s) : term -> term' where repeat(Memo1) ; the-s => term' ; rules ( Memo1 : term -> term' )