login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

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))
fricas
x^2+y^2<1
2 2 (2) y + x < 1
Type: InEquality?(Polynomial(Integer))
fricas
a+b<=2
(3) b + a <= 2
Type: InEquality?(Polynomial(Integer))
fricas
sin(x)+y>=1+y
(4) sin(x) + y >= y + 1
Type: InEquality?(Expression(Integer))
fricas
eql(x,y)
(5) x = y
Type: InEquality?(Symbol)
fricas
neq(x,y)
(6) x ~= y
Type: InEquality?(Symbol)
fricas
P1:=sin(x)+y>=1+y
(7) sin(x) + y >= y + 1
Type: InEquality?(Expression(Integer))
fricas
lhs P1
(8) sin(x) + y
Type: Expression(Integer)
fricas
rhs P1
(9) y + 1
Type: Expression(Integer)
fricas
rel P1
(10) >=
Type: Symbol
fricas
converse P1
(11) y + 1 <= sin(x) + y
Type: InEquality?(Expression(Integer))

Propositions

fricas
assert(P1)
(12) {sin(x) + y >= y + 1}
Type: Prop(Expression(Integer))
fricas
R ==> EXPR INT
Type: Void
fricas
A:=assert(x::R + y + z >=1)
(14) {z + y + x >= 1}
Type: Prop(Expression(Integer))
fricas
B:=assert(z::R<1/2)
1 (15) {z < -} 2
Type: Prop(Expression(Integer))
fricas
C:=assert(x+y=4::R)
(16) {y + x = 4}
Type: Prop(Expression(Integer))
fricas
And(A,B)
1 (17) ({z + y + x >= 1} & {z < -}) 2
Type: Prop(Expression(Integer))
fricas
Or(A,B)
1 (18) ({z + y + x >= 1} | {z < -}) 2
Type: Prop(Expression(Integer))
fricas
Imp(A,C)
(19) ({z + y + x >= 1} => {y + x = 4})
Type: Prop(Expression(Integer))
fricas
Eqv(B,C)
1 (20) ({z < -} <=> {y + x = 4}) 2
Type: Prop(Expression(Integer))
fricas
Not(A)
(21) ~({z + y + x >= 1})
Type: Prop(Expression(Integer))
fricas
Not(C)
(22) ~({y + x = 4})
Type: Prop(Expression(Integer))
fricas
All(x,A)
(23) \x.[{z + y + x >= 1}]
Type: Prop(Expression(Integer))
fricas
All(y,Ex(z,A))
(24) \y.[?z.[{z + y + x >= 1}]]
Type: Prop(Expression(Integer))
fricas
All(x,All(y,Imp(assert(x=y),assert(y=x))))
(25) \x.[\y.[({x = y} => {y = x})]]
Type: Prop(Symbol)

NNF

fricas
m1:=assert(m>1::R)
(26) {m > 1}
Type: Prop(Expression(Integer))
fricas
m2:=assert(m<n::R)
(27) {m < n}
Type: Prop(Expression(Integer))
fricas
p:=Imp(And(m1,m2),Not(Ex(k,assert(k*m=n::R))))
(28) (({m > 1} & {m < n}) => ~(?k.[{k m = n}]))
Type: Prop(Expression(Integer))
fricas
Prime(n) == All(m,p)
Type: Void
fricas
Prime(n)
fricas
Compiling function Prime with type Variable(n) -> Prop(Expression(
      Integer)) 
(30) \m.[(({m > 1} & {m < n}) => ~(?k.[{k m = n}]))]
Type: Prop(Expression(Integer))
fricas
nnf Prime(n)
(31) \m.[(({m <= 1} | {m >= n}) | \k.[{k m ~= n}])]
Type: Prop(Expression(Integer))
fricas
nnf 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))
fricas
nnf Not(And(A,B))
1 (33) ({z + y + x < 1} | {z >= -}) 2
Type: Prop(Expression(Integer))

SUBSETS

fricas
setOfAll([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))
fricas
setOfAll([x,y],And(assert(x^2<y^2+1),assert(x+y>c)))
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 !!
  ( 13 subscribers )  
Please rate this page: