Adding the MP+CP+F example and a few minor tweaks.

classes/lc.js

@@ -1469,37 +1469,41 @@ class LC extends Structure {
 
     targetlist.forEach( X => {
 
-      let t0=new Date
+      // Don't validate targets that are givens
+      if (!X.isAGiven) {
 
-      // debug(`Validating target ${this.toString()} `)
-      // debug(`Computing satsnf:`)
+        let t0=new Date
 
-      let c = this.satcnf( true, X )
+        // debug(`Validating target ${this.toString()} `)
+        // debug(`Computing satsnf:`)
 
-      // debug(`resulting satsnf:`)
-      // debug(c)
+        let c = this.satcnf( true, X )
 
-      // if the target has an empty cnf, just call it true
-      if (c.length === 0) {
-        X.setAttribute('Validation',true)
-      } else {
+        // debug(`resulting satsnf:`)
+        // debug(c)
 
-        let n = LC.numvars(c)
+        // if the target has an empty cnf, just call it true
+        if (c.length === 0) {
+          X.setAttribute('Validation',true)
+        } else {
 
-        let t1=new Date
-        if (targetlist.length===1) {
-          debug(`Convert to SAT cnf (fast): ${(t1-t0)/1000} seconds`)
-        }
-        let ans=!satSolve(n,c)
+          let n = LC.numvars(c)
 
-        globalans = globalans && ans
+          let t1=new Date
+          if (targetlist.length===1) {
+            debug(`Convert to SAT cnf (fast): ${(t1-t0)/1000} seconds`)
+          }
+          let ans=!satSolve(n,c)
 
-        let t2=new Date
-        if (targetlist.length===1) {
-          debug(`Run SAT: ${(t2-t1)/1000} seconds`)
-        }
-        X.setAttribute('Validation',ans)
+          globalans = globalans && ans
 
+          let t2=new Date
+          if (targetlist.length===1) {
+            debug(`Run SAT: ${(t2-t1)/1000} seconds`)
+          }
+          X.setAttribute('Validation',ans)
+
+        }
       }
     } )
 
@@ -1820,7 +1824,7 @@ class PreppedPropForm {
     // Base case 1: If there are no targets to pursue, the result is an empty list.
     if ( targets.length == 0 )
       return [ ]
-    
+
     // If this LC is a target, just process ALL conclusions,
     // then mark all otherwise unmarked conclusions as having this LC as the target.
     if ( targets.includes( lc ) ) {

classes/statement.js

@@ -109,7 +109,7 @@ class Statement extends LC {
     let colon    = colorize(':','whiteBright','bold'),
         tilde    = colorize('~',stateColor),
         iname    = colorize(nicename(idname),stateColor),
-        boundYes = colorize('✓','yellowBright'),
+        boundYes = colorize('•','yellowBright'),
         concYes  = colorize('✔︎','yellowBright'),
         envYes   = colorize('★','yellowBright'),
         wrong    = colorize('✗','redBright'),

dependencies/lode.js

@@ -21,6 +21,7 @@ let Indent      = { Indent: true }
 let EEs         = { EEs: true }
 let Skolem      = { Skolem: true }
 let Compact     = { Compact:true }
+let Flat        = { Color:true, Conc:true, Env:true, Bound:true }
 let All         = { Conc:true, Env:true, Bound:true, Color:true,
                     Indent:true, EEs:true, Skolem: true }
 let None        = { }
@@ -63,6 +64,7 @@ X.show( options )
       Skolem  : show Skolemized constant names
       All     : show everything above
       None    : just show a flat monochromatic string.
+      Flat    : show a flat colored string with all validation icons
      `,
     Validate: `
 X.Validate( showtimes )
@@ -101,6 +103,7 @@ module.exports.Indent   = Indent
 module.exports.EEs      = EEs
 module.exports.Skolem   = Skolem
 module.exports.Compact  = Compact
+module.exports.Flat     = Flat
 module.exports.All      = All
 module.exports.None     = None
 module.exports.colorize = colorize

test/data/MPCPFexample.js

@@ -0,0 +1,9 @@
+//
+//  MPCPFexample.js - loads a giant string that contains a good example
+
+const fs = require('fs')
+
+// we keep it in a separate text file for syntax highlighting purposes
+const MPCPFstr = fs.readFileSync(__dirname+'/MPCPFexampleTxt.js', 'utf8')
+
+module.exports.MPCPFstr = MPCPFstr

test/data/MPCPFexampleTxt.js

@@ -0,0 +1,63 @@
+//
+//  MPCPFexampleTxt.js - stores a giant string that contains a good example
+//  of validation by MP+CP+F
+
+{ ////// header
+  // factoring these out to reduce clutter
+  :{ Declare{ ⊆ = ∈ ⇒ { } }
+    // EEs (misnomer, but no big deal for now)
+    { :Let{ x ∈(x,∩(A,B)) } ∈(x,∩(A,B)) }
+    { :Let{ y ∈(y,A) } ∈(y,A) }
+    // UEs from first pass of MP+CP+F validation
+    { :{ ⊆(S,S) }
+        { ⊆(A,A) }}
+    { :{ :∈(z,∩(S,T)) ∈(z,S) ∈(z,T) }
+        { :∈(x,∩(A,B)) ∈(x,A) ∈(x,B) }}
+    { :{ :⊆(S,T) :∈(z,S) ∈(z,T) }
+        { :⊆(A,B) :∈(y,A) ∈(y,B) }}
+    { :{ :∈(z,S) :∈(z,T) ∈(z,∩(S,T)) }
+        { :∈(y,A) :∈(y,B) ∈(y,∩(A,B)) }}
+    // UEs from the second pass of MP+CP+F validation
+    { :{ :{ :Let{ z ∈(z,S) } ∈(z,T) } ⊆(S,T) }
+        { :{ :Let{ x ∈(x,∩(A,B)) } ∈(x,A) } ⊆(∩(A,B),A) } }
+    { :{ :{ :Let{ z ∈(z,S) } ∈(z,T) } ⊆(S,T) }
+        { :{ :Let{ y ∈(y,A) } ∈(y,∩(A,B))  } ⊆(A,∩(A,B)) } }
+    // UEs from third pass of MP+CP+F validation
+    { :{ :⊆(S,T) :⊆(T,S) =(S,T) }
+        { :⊆(∩(A,B),A) :⊆(A,∩(A,B)) =(∩(A,B),A) }}
+    // UEs from fourth pass of MP+CP+F validation
+    { :{ :{ :P Q } ⇒(P,Q) }
+        { :{ :⊆(A,B) =(∩(A,B),A) } ⇒(⊆(A,B),=(∩(A,B),A)) }}
+  }
+
+  ////// dependencies (hidden)
+  :Declare{ ⊆ = ∈ ⇒ { } }  // constant declarations
+  :{ :{ :P Q } ⇒(P,Q) }  // implies+
+  :{ :⊆(S,T) :∈(z,S) ∈(z,T) }  // subset-
+  :{ :{ :Let{ z ∈(z,S) } ∈(z,T) } ⊆(S,T)  }  // subset+
+  :{ :⊆(S,T) :⊆(T,S) =(S,T) }  // set equality+
+  :{ :∈(z,S) :∈(z,T) ∈(z,∩(S,T)) }  // intersection+
+  :{ :∈(z,∩(S,T)) ∈(z,S) ∈(z,T) }  // intersection-
+  :{ ⊆(S,S) }  // previous theorem
+
+  ////// user's document (visible)
+  // Theorem 1
+  { =(∩(A,A),A) }
+  // Proof of Theorem 1
+  { ⊆(A,A) }
+  // Theorem 2
+  { ⇒(⊆(A,B),=(∩(A,B),A)) }
+  // Proof of Theorem 2
+  { :⊆(A,B)
+     =(∩(A,B),A)
+     ⊆(∩(A,B),A)
+     { :Let{ x ∈(x,∩(A,B)) }
+       ∈(x,A)
+     }
+     ⊆(A,∩(A,B))
+     { :Let{ y ∈(y,A) }
+       ∈(y,B)
+       ∈(y,∩(A,B))
+     }
+  }
+}