@@ -100,8 +100,8 @@ function assumeEquality(proposition: Expression): AssumeResult {
100100 const unknowns = proposition . unknowns ;
101101 if ( unknowns . length === 0 ) {
102102 const val = proposition . evaluate ( ) ;
103- if ( isSymbol ( val ) && val . symbol === 'True' ) return 'tautology' ;
104- if ( isSymbol ( val ) && val . symbol === 'False' ) return 'contradiction' ;
103+ if ( isSymbol ( val , 'True' ) ) return 'tautology' ;
104+ if ( isSymbol ( val , 'False' ) ) return 'contradiction' ;
105105 console . log ( proposition . canonical . evaluate ( ) ) ;
106106 return 'not-a-predicate' ;
107107 }
@@ -254,8 +254,8 @@ function assumeInequality(proposition: Expression): AssumeResult {
254254 // Case 2
255255 const result = ce . box ( [ op === '<' ? 'Less' : 'LessEqual' , p , 0 ] ) . evaluate ( ) ;
256256
257- if ( isSymbol ( result ) && result . symbol === 'True' ) return 'tautology' ;
258- if ( isSymbol ( result ) && result . symbol === 'False' ) return 'contradiction' ;
257+ if ( isSymbol ( result , 'True' ) ) return 'tautology' ;
258+ if ( isSymbol ( result , 'False' ) ) return 'contradiction' ;
259259
260260 const unknowns = result . unknowns ;
261261 if ( unknowns . length === 0 ) return 'not-a-predicate' ;
@@ -274,7 +274,7 @@ function assumeInequality(proposition: Expression): AssumeResult {
274274 const originalOp = proposition . operator ;
275275 const propOp1 = proposition . op1 ;
276276 const propOp2 = proposition . op2 ;
277- const isSymbolOnLeft = isSymbol ( propOp1 ) && propOp1 . symbol === symbol ;
277+ const isSymbolOnLeft = isSymbol ( propOp1 , symbol ) ;
278278 const otherSide = isSymbolOnLeft ? propOp2 : propOp1 ;
279279
280280 // Only do bounds checking for simple comparisons like "x > k" where k is numeric
@@ -486,8 +486,8 @@ function assumeElement(proposition: Expression): AssumeResult {
486486
487487 // Case 4
488488 const val = proposition . evaluate ( ) ;
489- if ( isSymbol ( val ) && val . symbol === 'True' ) return 'tautology' ;
490- if ( isSymbol ( val ) && val . symbol === 'False' ) return 'contradiction' ;
489+ if ( isSymbol ( val , 'True' ) ) return 'tautology' ;
490+ if ( isSymbol ( val , 'False' ) ) return 'contradiction' ;
491491 return 'not-a-predicate' ;
492492}
493493
@@ -550,36 +550,31 @@ export function getSignFromAssumptions(
550550 // Case 1: Direct symbol comparison
551551 // x < 0 means x is negative
552552 // x <= 0 means x is non-positive
553- if ( isSymbol ( lhs ) && lhs . symbol === symbol ) {
553+ if ( isSymbol ( lhs , symbol ) ) {
554554 if ( op === 'Less' ) return 'negative' ;
555555 if ( op === 'LessEqual' ) return 'non-positive' ;
556556 }
557557
558558 // Case 2: Negated symbol comparison
559559 // -x < 0 means x > 0 (positive)
560560 // -x <= 0 means x >= 0 (non-negative)
561- if (
562- isFunction ( lhs ) &&
563- lhs . operator === 'Negate' &&
564- isSymbol ( lhs . op1 ) &&
565- lhs . op1 . symbol === symbol
566- ) {
561+ if ( isFunction ( lhs , 'Negate' ) && isSymbol ( lhs . op1 , symbol ) ) {
567562 if ( op === 'Less' ) return 'positive' ;
568563 if ( op === 'LessEqual' ) return 'non-negative' ;
569564 }
570565
571566 // Case 3: Symbol with subtraction from constant
572567 // a - x < 0 means x > a, so if a >= 0, x is positive
573568 // x - a < 0 means x < a, so if a <= 0, x is negative
574- if ( isFunction ( lhs ) && lhs . operator === 'Subtract' ) {
569+ if ( isFunction ( lhs , 'Subtract' ) ) {
575570 const [ a , b ] = lhs . ops ;
576571 if ( a && b ) {
577572 // a - x < 0 => x > a
578- if ( isSymbol ( b ) && b . symbol === symbol && a . isNonNegative === true ) {
573+ if ( isSymbol ( b , symbol ) && a . isNonNegative === true ) {
579574 if ( op === 'Less' ) return 'positive' ;
580575 }
581576 // x - a < 0 => x < a
582- if ( isSymbol ( a ) && a . symbol === symbol && b . isNonPositive === true ) {
577+ if ( isSymbol ( a , symbol ) && b . isNonPositive === true ) {
583578 if ( op === 'Less' ) return 'negative' ;
584579 }
585580 }
@@ -588,10 +583,10 @@ export function getSignFromAssumptions(
588583 // Case 4: Addition form (canonical form of subtraction)
589584 // x + (-a) < 0 means x < a, so if a <= 0, x is negative
590585 // -x + a < 0 means -x < -a means x > a, so if a >= 0, x is positive
591- if ( isFunction ( lhs ) && lhs . operator === 'Add' ) {
586+ if ( isFunction ( lhs , 'Add' ) ) {
592587 for ( const term of lhs . ops ) {
593588 // Direct symbol in sum: check if other terms give us bounds
594- if ( isSymbol ( term ) && term . symbol === symbol ) {
589+ if ( isSymbol ( term , symbol ) ) {
595590 // x + ... < 0, check if other terms are all non-negative
596591 // That would mean x < -(sum of others), so x < non-positive = negative
597592 const otherTerms = lhs . ops . filter ( ( t ) => t !== term ) ;
@@ -604,12 +599,7 @@ export function getSignFromAssumptions(
604599 }
605600 }
606601 // Negated symbol in sum: -x + ... < 0
607- if (
608- isFunction ( term ) &&
609- term . operator === 'Negate' &&
610- isSymbol ( term . op1 ) &&
611- term . op1 . symbol === symbol
612- ) {
602+ if ( isFunction ( term , 'Negate' ) && isSymbol ( term . op1 , symbol ) ) {
613603 // -x + ... < 0 means x > ...
614604 const otherTerms = lhs . ops . filter ( ( t ) => t !== term ) ;
615605 if (
0 commit comments