login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit
 Topics FrontPage SandBox SandBoxProp <-- You are here. spad)abbrev domain INEQTY InEquality ++ Author: kfp ++ Date Created: Sun Oct 26 02:21:23 CEST 2014 ++ License: BSD (same as Axiom) ++ Date Last Updated: ++ Basic Operations: ++ Related Domains: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ Examples: ++ References: ++ ++ Description: ++ ++ InEquality(S:Comparable) : Exports == Implementation where OF ==> OutputForm Exports == Join(Comparable , CoercibleTo OutputForm) with "<" : (S,S) -> % ++ < means lesser than "<=" : (S,S) -> % ++ <= means lesser than or equal ">" : (S,S) -> % ++ > means greater than ">=" : (S,S) -> % ++ >= means greater than or equal eql : (S,S) -> % ++ = means equal neq : (S,S) -> % ++ neq means not equal. lhs : % -> S ++ lhs returns the left hand side of the inequality rhs : % -> S ++ rhs returns the right hand side of the inequality rel : % -> Symbol ++ rel returns the inequality (relation) symbol converse : % -> % ++ converse inequality coerce : % -> OF ++ coerce to output form Implementation == add Rep := Record(rel:Symbol , lhs : S, rhs : S) s:List(Symbol):=['<,'<=,'>,'>=,'=,'~=] l:S < r:S == [s.1, l, r]$Rep l:S <= r:S == [s.2, l, r]$Rep l:S > r:S == [s.3, l, r]$Rep l:S >= r:S == [s.4, l, r]$Rep eql(l:S,r:S) == [s.5, l, r]$Rep neq(l:S,r:S) == [s.6, l, r]$Rep lhs x == x.lhs rhs x == x.rhs rel x == x.rel converse x == x.rel = s.1 => [s.3, x.rhs, x.lhs]$Rep x.rel = s.2 => [s.4, x.rhs, x.lhs]$Rep x.rel = s.3 => [s.1, x.rhs, x.lhs]$Rep x.rel = s.4 => [s.2, x.rhs, x.lhs]$Rep x.rel = s.5 => [s.5, x.rhs, x.lhs]$Rep x.rel = s.6 => [s.6, x.rhs, x.lhs]$Rep coerce(x:%):OF == hconcat [x.lhs::OF," ", x.rel::OF, " ", x.rhs::OF] )abbrev domain PROP Prop ++ Prop is the domain of Propositions over a type T Prop(T:Comparable) : Exports == Implementation where S ==> Symbol PI ==> PositiveInteger EQT ==> InEquality(T) TT ==> Union(S,T,PI,EQT) Exports == with assert : InEquality(T) -> % ++ assert an equation of type InEquality(T) assert : Equation(T) -> % ++ assert an equation of type Equation(T) (convenience) And : (%,%) -> % ++ And means the logical connective 'and' Or : (%,%) -> % ++ Or means the logical connective 'or' Imp : (%,%) -> % ++ Imp means the logical connective 'implies' Eqv : (%,%) -> % ++ Eqv means the logical connective 'equivalent' Not : % -> % ++ Not means negation 'not' All : (Symbol,%) -> % ++ All means the universal quantifier 'forall' Ex : (Symbol,%) -> % ++ Ex means the existential quantifier 'exists' coerce : % -> OutputForm ++ coerce to output form qvars : % -> List(TT) ++ qvars lists all quantifier variables nnf : % -> % ++ nnf means negation normal form 'nnf' Implementation == add -- BinaryTree(TT) add Rep := BinaryTree(TT) -- map x in TT to Rep iD(x:TT):% == binaryTree(x)$Rep rs:List(Symbol):=['<,'<=,'>,'>=,'=,'~=] ----------------------- -- Op id's -- 1 ..... and -- 2 ..... or -- 3 ..... implies -- 4 ..... equivalent -- 5 ..... not -- 6 ..... forall -- 7 ..... exists -- 8,9 .... reserved -- 10 ..... equality -- 11 ..... neq -- 12 ..... lt -- 13 ..... leq -- 14 ..... gt -- 15 ..... geq ----------------------- -- assert an element of type Equation(T) assert(s:Equation(T)):% == binaryTree(iD lhs s,10,iD rhs s)$Rep assert(s:EQT):% == rel s = rs.1 => binaryTree(iD lhs s,12,iD rhs s)$Rep rel s = rs.2 => binaryTree(iD lhs s,13,iD rhs s)$Rep rel s = rs.3 => binaryTree(iD lhs s,14,iD rhs s)$Rep rel s = rs.4 => binaryTree(iD lhs s,15,iD rhs s)$Rep rel s = rs.5 => binaryTree(iD lhs s,10,iD rhs s)$Rep rel s = rs.6 => binaryTree(iD lhs s,11,iD rhs s)$Rep -- variable, the only nodes without left/right var(x:S):% == binaryTree(x)$Rep And(p:%,q:%):% == binaryTree(p,1,q)$Rep Or (p:%,q:%):% == binaryTree(p,2,q)$Rep Imp(p:%,q:%):% == binaryTree(p,3,q)$Rep Eqv(p:%,q:%):% == binaryTree(p,4,q)$Rep Not(p:%):% == binaryTree(p,5,empty())$Rep All(x:S,p:%):% == binaryTree(var x,6,p)$Rep Ex (x:S,p:%):% == binaryTree(var x,7,p)$Rep coerce(p) == OF ==> OutputForm lp:OF:="(" rp:OF:=")" lb:OF:="{" rb:OF:="}" lk:OF:="[" rk:OF:="]" of:OF:="" s0:OF:="." s1:OF:=" & " s2:OF:=" | " s3:OF:=" => " s4:OF:=" <=> " s5:OF:="~" s6:OF:="\" s7:OF:="?" s10:OF:=" = " s11:OF:=" ~= " s12:OF:=" < " s13:OF:=" <= " s14:OF:=" > " s15:OF:=" >= " empty? p => of val:= value p val=1 => of:=hconcat [of,lp,coerce(left p),s1,coerce(right p),rp] val=2 => of:=hconcat [of,lp,coerce(left p),s2,coerce(right p),rp] val=3 => of:=hconcat [of,lp,coerce(left p),s3,coerce(right p),rp] val=4 => of:=hconcat [of,lp,coerce(left p),s4,coerce(right p),rp] val=5 => of:=hconcat [of,s5,lp,coerce(left p),rp] val=6 => of:=hconcat [of,s6,coerce(left p),s0,lk,coerce(right p),rk] val=7 => of:=hconcat [of,s7,coerce(left p),s0,lk,coerce(right p),rk] val=10=> of:=hconcat [of,lb,coerce(left p),s10,coerce(right p),rb] val=11=> of:=hconcat [of,lb,coerce(left p),s11,coerce(right p),rb] val=12=> of:=hconcat [of,lb,coerce(left p),s12,coerce(right p),rb] val=13=> of:=hconcat [of,lb,coerce(left p),s13,coerce(right p),rb] val=14=> of:=hconcat [of,lb,coerce(left p),s14,coerce(right p),rb] val=15=> of:=hconcat [of,lb,coerce(left p),s15,coerce(right p),rb] of:=hconcat[of,val::OF] of --local mvNot(p:%):% == val := value p val=1 => Or(Not(left p),Not(right p))::Rep val=2 => And(Not(left p),Not(right p))::Rep val=3 => And(left p, Not(right p))::Rep val=4 => Not(Or(And(left p,right p),And(Not(left p),Not(right p)))) val=5 => (left p)::Rep val=6 => Ex(value(left p)::S, Not(right p))::Rep val=7 => All(value(left p)::S, Not(right p))::Rep val=10 => binaryTree(left p,11,right p)$Rep val=11 => binaryTree(left p,10,right p)$Rep val=12 => binaryTree(left p,15,right p)$Rep val=13 => binaryTree(left p,14,right p)$Rep val=14 => binaryTree(left p,13,right p)$Rep val=15 => binaryTree(left p,12,right p)$Rep p::Rep nnf(p:%):% == empty? p => p::Rep val := value p val=1 => And(nnf(left p),nnf(right p)) val=2 => Or(nnf(left p),nnf(right p)) val=3 => nnf(Or(Not(left p),right p)) val=4 => nnf(And(Or(left p,Not(right p)),Or(Not(left p),right p))) val=5 => nnf(mvNot(left p)) val=6 => All(value(left p)::S, nnf(right p)) val=7 => Ex(value(left p)::S, nnf(right p)) p::Rep qvars(p:%):List(TT) == L:List(TT):=[] empty? p => []::List(TT) val := value p if (val case S) then L:=append(L,[val]) else L:=append(L,qvars(left p)) L:=append(L,qvars(right p)) L )abbrev domain SUBSET SubsetOf ++ Author: kfp ++ Date Created: Mon Nov 03 20:41:24 CET 2014 ++ License: BSD (same as Axiom) ++ Date Last Updated: ++ Basic Operations: ++ Related Domains: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ Examples: ++ References: ++ ++ Description: ++ ++ SubsetOf(T:Comparable) : Exports == Implementation where OF ==> OutputForm Exports == Join(Comparable , CoercibleTo OutputForm) with setOfAll : (List Symbol, Prop T ) -> % member? : (List T,%) -> Boolean coerce : % -> OutputForm Implementation == Prop(T) add Rep := Record(s:List Symbol, p:Prop T) setOfAll(ls,P) == [ls,P]::Rep member?(t,ss) == false coerce(ss:%):OF == r:=ss::Rep sym:OF:=(r.s)::OF prop:OF:=(r.p)::OF hconcat ["Set of all "::OF, sym," such that "::OF, prop] spad Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8617047757752040298-25px001.spad using old system compiler. INEQTY abbreviates domain InEquality ------------------------------------------------------------------------ initializing NRLIB INEQTY for InEquality compiling into NRLIB INEQTY compiling exported < : (S,S) -> $Time: 0.01 SEC. compiling exported <= : (S,S) ->$ Time: 0 SEC. compiling exported > : (S,S) -> $Time: 0 SEC. compiling exported >= : (S,S) ->$ Time: 0 SEC. compiling exported eql : (S,S) -> $Time: 0 SEC. compiling exported neq : (S,S) ->$ Time: 0 SEC. compiling exported lhs : $-> S INEQTY;lhs;$S;7 is replaced by QVELTx1 Time: 0.01 SEC. compiling exported rhs : $-> S INEQTY;rhs;$S;8 is replaced by QVELTx2 Time: 0 SEC. compiling exported rel : $-> Symbol INEQTY;rel;$S;9 is replaced by QVELTx0 Time: 0 SEC. compiling exported converse : $->$ Time: 0.01 SEC. compiling exported coerce : $-> OutputForm Time: 0 SEC. (time taken in buildFunctor: 0) ;;; *** |InEquality| REDEFINED ;;; *** |InEquality| REDEFINED Time: 0 SEC. Cumulative Statistics for Constructor InEquality Time: 0.03 seconds finalizing NRLIB INEQTY Processing InEquality for Browser database: --------constructor--------- --------(< (% S S))--------- --------(<= (% S S))--------- --------(> (% S S))--------- --------(>= (% S S))--------- --------(eql (% S S))--------- --->-->InEquality((eql (% S S))): Improper first word in comments: = "= means equal" --------(neq (% S S))--------- --------(lhs (S %))--------- --------(rhs (S %))--------- --------(rel ((Symbol) %))--------- --------(converse (% %))--------- --------(coerce ((OutputForm) %))--------- ; compiling file "/var/aw/var/LatexWiki/INEQTY.NRLIB/INEQTY.lsp" (written 07 NOV 2014 05:10:59 AM): ; /var/aw/var/LatexWiki/INEQTY.NRLIB/INEQTY.fasl written ; compilation finished in 0:00:00.046 ------------------------------------------------------------------------ InEquality is now explicitly exposed in frame initial InEquality will be automatically loaded when needed from /var/aw/var/LatexWiki/INEQTY.NRLIB/INEQTY PROP abbreviates domain Prop ------------------------------------------------------------------------ initializing NRLIB PROP for Prop compiling into NRLIB PROP Local variable Rep type redefined: (Join (BinaryTreeCategory (Union (Symbol) T$ (PositiveInteger) (InEquality T$))) (CATEGORY domain (SIGNATURE binaryTree ($ (Union (Symbol) T$(PositiveInteger) (InEquality T$)))) (SIGNATURE binaryTree ( (Union (Symbol) T$(PositiveInteger) (InEquality T$)) $)))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: rel (Symbol)) (: lhs S) (: rhs S)) (Symbol) S S)) (SIGNATURE ~= ((Boolean) (Record (: rel (Symbol)) (: lhs S) (: rhs S)) (Record (: rel (Symbol)) (: lhs S) (: rhs S)))) (SIGNATURE coerce ((OutputForm) (Record (: rel (Symbol)) (: lhs S) (: rhs S)))) (SIGNATURE elt ((Symbol) (Record (: rel (Symbol)) (: lhs S) (: rhs S)) rel)) (SIGNATURE elt (S (Record (: rel (Symbol)) (: lhs S) (: rhs S)) lhs)) (SIGNATURE elt (S (Record (: rel (Symbol)) (: lhs S) (: rhs S)) rhs)) (SIGNATURE setelt! ((Symbol) (Record (: rel (Symbol)) (: lhs S) (: rhs S)) rel (Symbol))) (SIGNATURE setelt! (S (Record (: rel (Symbol)) (: lhs S) (: rhs S)) lhs S)) (SIGNATURE setelt! (S (Record (: rel (Symbol)) (: lhs S) (: rhs S)) rhs S)) (SIGNATURE copy ((Record (: rel (Symbol)) (: lhs S) (: rhs S)) (Record (: rel (Symbol)) (: lhs S) (: rhs S)))))) compiling local iD : Union(Symbol,T$,PositiveInteger,InEquality T$) ->$ Time: 0 SEC. compiling exported assert : Equation T$->$ Time: 0.01 SEC. compiling exported assert : InEquality T$->$ Time: 0 SEC. compiling local var : Symbol -> $Time: 0 SEC. compiling exported And : ($,$) ->$ Time: 0.01 SEC. compiling exported Or : ($,$) -> $Time: 0 SEC. compiling exported Imp : ($,$) ->$ Time: 0 SEC. compiling exported Eqv : ($,$) -> $Time: 0 SEC. compiling exported Not :$ -> $Time: 0 SEC. compiling exported All : (Symbol,$) -> $Time: 0 SEC. compiling exported Ex : (Symbol,$) -> $Time: 0 SEC. compiling exported coerce :$ -> OutputForm processing macro definition OF ==> OutputForm Time: 0.02 SEC. compiling local mvNot : $->$ Time: 0.01 SEC. compiling exported nnf : $->$ Time: 0 SEC. compiling exported qvars : $-> List Union(Symbol,T$,PositiveInteger,InEquality T$) Time: 0.01 SEC. (time taken in buildFunctor: 0) ;;; *** |Prop| REDEFINED ;;; *** |Prop| REDEFINED Time: 0 SEC. Cumulative Statistics for Constructor Prop Time: 0.06 seconds finalizing NRLIB PROP Processing Prop for Browser database: --------constructor--------- --------(< (% S S))--------- --------(<= (% S S))--------- --------(> (% S S))--------- --------(>= (% S S))--------- --------(eql (% S S))--------- --->-->Prop((eql (% S S))): Improper first word in comments: = "= means equal" --------(neq (% S S))--------- --------(lhs (S %))--------- --------(rhs (S %))--------- --------(rel ((Symbol) %))--------- --------(converse (% %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(assert (% (InEquality T$)))--------- --------(assert (% (Equation T$)))--------- --------(And (% % %))--------- --------(Or (% % %))--------- --------(Imp (% % %))--------- --------(Eqv (% % %))--------- --------(Not (% %))--------- --------(All (% (Symbol) %))--------- --------(Ex (% (Symbol) %))--------- --------(coerce ((OutputForm) %))--------- --------(qvars ((List (Union (Symbol) T$ (PositiveInteger) (InEquality T$))) %))--------- --------(nnf (% %))--------- --->-->Prop(): Spurious comments: Prop is the domain of Propositions over a type \spad{T} ; compiling file "/var/aw/var/LatexWiki/PROP.NRLIB/PROP.lsp" (written 07 NOV 2014 05:10:59 AM): ; /var/aw/var/LatexWiki/PROP.NRLIB/PROP.fasl written ; compilation finished in 0:00:00.159 ------------------------------------------------------------------------ Prop is now explicitly exposed in frame initial Prop will be automatically loaded when needed from /var/aw/var/LatexWiki/PROP.NRLIB/PROP SUBSET abbreviates domain SubsetOf ------------------------------------------------------------------------ initializing NRLIB SUBSET for SubsetOf compiling into NRLIB SUBSET Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: s (List (Symbol))) (: p (Prop T$))) (List (Symbol)) (Prop T$))) (SIGNATURE ~= ((Boolean) (Record (: s (List (Symbol))) (: p (Prop T$))) (Record (: s (List (Symbol))) (: p (Prop T$))))) (SIGNATURE coerce ((OutputForm) (Record (: s (List (Symbol))) (: p (Prop T$))))) (SIGNATURE elt ((List (Symbol)) (Record (: s (List (Symbol))) (: p (Prop T$))) s)) (SIGNATURE elt ((Prop T$) (Record (: s (List (Symbol))) (: p (Prop T$))) p)) (SIGNATURE setelt! ((List (Symbol)) (Record (: s (List (Symbol))) (: p (Prop T$))) s (List (Symbol)))) (SIGNATURE setelt! ((Prop T$) (Record (: s (List (Symbol))) (: p (Prop T$))) p (Prop T$))) (SIGNATURE copy ((Record (: s (List (Symbol))) (: p (Prop T$))) (Record (: s (List (Symbol))) (: p (Prop T$))))))) to (Join (BinaryTreeCategory (Union (Symbol) T$ (PositiveInteger) (InEquality T$))) (CATEGORY domain (SIGNATURE binaryTree ($ (Union (Symbol) T$(PositiveInteger) (InEquality T$)))) (SIGNATURE binaryTree ( (Union (Symbol) T$(PositiveInteger) (InEquality T$)) $)))) compiling exported setOfAll : (List Symbol,Prop T$) -> $SUBSET;setOfAll;LP$;1 is replaced by CONS Time: 0 SEC. compiling exported member? : (List T$,$) -> Boolean SUBSET;member?;L$B;2 is replaced by QUOTE Time: 0 SEC. compiling exported coerce :$ -> OutputForm Time: 0 SEC. (time taken in buildFunctor: 0) ;;; *** |SubsetOf| REDEFINED ;;; *** |SubsetOf| REDEFINED Time: 0.01 SEC. Warnings: [1] coerce: s has no value [2] coerce: p has no value Cumulative Statistics for Constructor SubsetOf Time: 0.01 seconds --------------non extending category---------------------- .. SubsetOf(#1) of cat (|Join| (|Comparable|) (|CoercibleTo| (|OutputForm|)) (CATEGORY |domain| (SIGNATURE |setOfAll| ($(|List| (|Symbol|)) (|Prop| |#1|))) (SIGNATURE |member?| ((|Boolean|) (|List| |#1|)$)) (SIGNATURE |coerce| ((|OutputForm|) $)))) has no assert : InEquality(#1) -> % finalizing NRLIB SUBSET Processing SubsetOf for Browser database: --------constructor--------- --------(< (% S S))--------- --------(<= (% S S))--------- --------(> (% S S))--------- --------(>= (% S S))--------- --------(eql (% S S))--------- --->-->SubsetOf((eql (% S S))): Improper first word in comments: = "= means equal" --------(neq (% S S))--------- --------(lhs (S %))--------- --------(rhs (S %))--------- --------(rel ((Symbol) %))--------- --------(converse (% %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(assert (% (InEquality T$)))--------- --------(assert (% (Equation T$)))--------- --------(And (% % %))--------- --------(Or (% % %))--------- --------(Imp (% % %))--------- --------(Eqv (% % %))--------- --------(Not (% %))--------- --------(All (% (Symbol) %))--------- --------(Ex (% (Symbol) %))--------- --------(coerce ((OutputForm) %))--------- --------(qvars ((List (Union (Symbol) T$ (PositiveInteger) (InEquality T$))) %))--------- --------(nnf (% %))--------- --------constructor--------- --->-->SubsetOf((setOfAll (% (List (Symbol)) (Prop T$)))): Not documented!!!! --->-->SubsetOf((member? ((Boolean) (List T\$) %))): Not documented!!!! --->-->SubsetOf((coerce ((OutputForm) %))): Not documented!!!! --->-->SubsetOf(): Spurious comments: Prop is the domain of Propositions over a type \spad{T} --->-->SubsetOf(): Spurious comments: \blankline \blankline ; compiling file "/var/aw/var/LatexWiki/SUBSET.NRLIB/SUBSET.lsp" (written 07 NOV 2014 05:11:00 AM): ; /var/aw/var/LatexWiki/SUBSET.NRLIB/SUBSET.fasl written ; compilation finished in 0:00:00.012 ------------------------------------------------------------------------ SubsetOf is now explicitly exposed in frame initial SubsetOf will be automatically loaded when needed from /var/aw/var/LatexWiki/SUBSET.NRLIB/SUBSET InEq? fricas)set output tex off  fricas)set output algebra on x>0 (1) x > 0 Type: InEquality?(Polynomial(Integer)) fricasx^2+y^2<1 2 2 (2) y + x < 1 Type: InEquality?(Polynomial(Integer)) fricasa+b<=2 (3) b + a <= 2 Type: InEquality?(Polynomial(Integer)) fricassin(x)+y>=1+y (4) sin(x) + y >= y + 1 Type: InEquality?(Expression(Integer)) fricaseql(x,y) (5) x = y Type: InEquality?(Symbol) fricasneq(x,y) (6) x ~= y Type: InEquality?(Symbol) fricasP1:=sin(x)+y>=1+y (7) sin(x) + y >= y + 1 Type: InEquality?(Expression(Integer)) fricaslhs P1 (8) sin(x) + y Type: Expression(Integer) fricasrhs P1 (9) y + 1 Type: Expression(Integer) fricasrel P1 (10) >= Type: Symbol fricasconverse P1 (11) y + 1 <= sin(x) + y Type: InEquality?(Expression(Integer)) Propositions fricasassert(P1) (12) {sin(x) + y >= y + 1} Type: Prop(Expression(Integer)) fricasR ==> EXPR INT Type: Void fricasA:=assert(x::R + y + z >=1) (14) {z + y + x >= 1} Type: Prop(Expression(Integer)) fricasB:=assert(z::R<1/2) 1 (15) {z < -} 2 Type: Prop(Expression(Integer)) fricasC:=assert(x+y=4::R) (16) {y + x = 4} Type: Prop(Expression(Integer)) fricasAnd(A,B) 1 (17) ({z + y + x >= 1} & {z < -}) 2 Type: Prop(Expression(Integer)) fricasOr(A,B) 1 (18) ({z + y + x >= 1} | {z < -}) 2 Type: Prop(Expression(Integer)) fricasImp(A,C) (19) ({z + y + x >= 1} => {y + x = 4}) Type: Prop(Expression(Integer)) fricasEqv(B,C) 1 (20) ({z < -} <=> {y + x = 4}) 2 Type: Prop(Expression(Integer)) fricasNot(A) (21) ~({z + y + x >= 1}) Type: Prop(Expression(Integer)) fricasNot(C) (22) ~({y + x = 4}) Type: Prop(Expression(Integer)) fricasAll(x,A) (23) \x.[{z + y + x >= 1}] Type: Prop(Expression(Integer)) fricasAll(y,Ex(z,A)) (24) \y.[?z.[{z + y + x >= 1}]] Type: Prop(Expression(Integer)) fricasAll(x,All(y,Imp(assert(x=y),assert(y=x)))) (25) \x.[\y.[({x = y} => {y = x})]] Type: Prop(Symbol) NNF fricasm1:=assert(m>1::R) (26) {m > 1} Type: Prop(Expression(Integer)) fricasm2:=assert(m 1} & {m < n}) => ~(?k.[{k m = n}])) Type: Prop(Expression(Integer)) fricasPrime(n) == All(m,p) Type: Void fricasPrime(n) fricasCompiling function Prime with type Variable(n) -> Prop(Expression( Integer)) (30) \m.[(({m > 1} & {m < n}) => ~(?k.[{k m = n}]))] Type: Prop(Expression(Integer)) fricasnnf Prime(n) (31) \m.[(({m <= 1} | {m >= n}) | \k.[{k m ~= n}])] Type: Prop(Expression(Integer)) fricasnnf Not Imp(And(A,B),Not Or(Not C,B)) 1 1 (32) (({z + y + x >= 1} & {z < -}) & ({y + x ~= 4} | {z < -})) 2 2 Type: Prop(Expression(Integer)) fricasnnf Not(And(A,B)) 1 (33) ({z + y + x < 1} | {z >= -}) 2 Type: Prop(Expression(Integer)) SUBSETS fricassetOfAll([x,y,z],assert(x^2+y^2+z^2<=1)) 2 2 2 (34) Set of all [x,y,z] such that {z + y + x <= 1} Type: SubsetOf?(Polynomial(Integer)) fricassetOfAll([x,y],And(assert(x^2c))) 2 2 (35) Set of all [x,y] such that ({x < y + 1} & {y + x > c}) Type: SubsetOf?(Polynomial(Integer)) -- continue with NatDed?/Solve/RSPACE/Cell/Interval/Surface(k) , requires: CAD

 Subject:   Be Bold !! ( 15 subscribers )