gistfile1.txt

(3-) (datatype globals

   _______________________
   (value *proof*) : proof;)

 <1> Inputs to shen.mu_reduction 
 [[shen.mu [mode V1189 +] [[shen.mu [mode V1190 +] [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]] V1192]] V1191], +,  ==>

  <2> Inputs to shen.mu_reduction 
  [[shen.mu V1189 [[shen.mu [mode V1190 +] [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]] V1192]] V1191], +,  ==>

   <3> Inputs to shen.mu_reduction 
   [[shen.mu [mode V1190 +] [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]] V1192], +,  ==>

    <4> Inputs to shen.mu_reduction 
    [[shen.mu V1190 [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]] V1192], +,  ==>

     <5> Inputs to shen.mu_reduction 
     [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]], +,  ==>

     <5> Output from shen.mu_reduction 
     ==> [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1190 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]

    <4> Output from shen.mu_reduction 
    ==> [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1192 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]

   <3> Output from shen.mu_reduction 
   ==> [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1189 [cons V1192 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]

  <2> Output from shen.mu_reduction 
  ==> [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1191 [cons V1192 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]

 <1> Output from shen.mu_reduction 
 ==> [shen.rename shen.the shen.variables in [Context_1957] and shen.then [call shen.the shen.continuation [[unify [cons V1191 [cons V1192 []]] [cons [cons [cons value [cons *proof* []]] [cons : [cons [cons list [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons * [cons [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] [cons --> [cons [cons list [cons [cons [cons list [cons wff []]] [cons * [cons wff []]]] []]] []]]] []]]] []]] []]]] [cons Context_1957 []]]]]]]
type#globals