Logiweb(TM)

Logiweb aspects of tactic-first-hyp ( " , " , " ) in pyk

Up Help

The "pyk" aspect

Define pyk of tactic-first-hyp ( asterisk , asterisk , asterisk ) as "tactic-first-hyp ( "! , "! , "! )" end define

The "value" aspect

define value of tactic-first-hyp ( t , s , c ) as norm { t is val : { s is val : { c is val : LET quote x conclude y end quote BE { asterisk IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime IN LET asterisk prime head BE { asterisk IN LET asterisk prime tail BE { asterisk prime IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime prime IN LET asterisk prime prime head BE { asterisk IN LET asterisk prime prime tail BE { asterisk prime prime IN LET asterisk BE { r IN LET asterisk prime prime head BE { asterisk IN LET asterisk prime prime tail BE { asterisk prime prime IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime prime prime IN LET asterisk prime prime prime head BE { asterisk IN LET asterisk prime prime prime tail BE { asterisk prime prime prime IN LET asterisk BE { i IN LET asterisk prime prime prime head BE { asterisk IN LET asterisk prime prime prime tail BE { asterisk prime prime prime IN LET asterisk prime head BE { asterisk IN LET asterisk prime tail BE { asterisk prime IN LET t BE { asterisk IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime IN LET asterisk prime head BE { asterisk IN LET asterisk prime tail BE { asterisk prime IN LET asterisk prime head BE { asterisk IN LET asterisk prime tail BE { asterisk prime IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime prime IN LET asterisk prime prime head BE { asterisk IN LET asterisk prime prime tail BE { asterisk prime prime IN LET asterisk BE { l IN LET asterisk prime prime head BE { asterisk IN LET asterisk prime prime tail BE { asterisk prime prime IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime prime prime IN LET asterisk prime prime prime head BE { asterisk IN LET asterisk prime prime prime tail BE { asterisk prime prime prime IN LET asterisk BE { x IN LET asterisk prime prime prime head BE { asterisk IN LET asterisk prime prime prime tail BE { asterisk prime prime prime IN LET { if asterisk atom then asterisk else { asterisk head } } :: { { if asterisk atom then asterisk else { asterisk tail } } :: true } BE { asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE { asterisk IN LET asterisk prime prime prime prime tail BE { asterisk prime prime prime prime IN LET asterisk BE { n IN LET asterisk prime prime prime prime head BE { asterisk IN LET asterisk prime prime prime prime tail BE { asterisk prime prime prime prime IN LET s [[ hook-hyp -> x ]] BE { asterisk IN LET asterisk BE { s IN LET s [[ hook-unitac -> unitac-hyp ]] BE { asterisk IN LET asterisk BE { s IN LET s [[ hook-pre -> add-first-hyp* ( x , s [[ hook-pre ]] , c ) ]] BE { asterisk IN LET asterisk BE { s IN LET make-root ( t , quote x unquote imply { x unquote } end quote ) :: { x :: { x :: true } } BE { asterisk IN LET asterisk BE { x prime IN LET tactic-push ( hook-pre , l :: { x prime :: { { make-root ( x prime , quote x prime unquote Init end quote ) :: { x prime :: true } } :: <<>> } } , s ) BE { asterisk IN LET asterisk BE { s IN LET taceval ( n , s , c ) BE { asterisk IN LET asterisk BE { s IN { s [[ hook-arg -> make-root ( t , quote { Mend1.8 Init Deref Ponens at { x unquote } } ;; { s [[ hook-arg ]] unquote } end quote ) :: { { make-root ( t , quote Mend1.8 Init Deref Ponens at { x unquote } end quote ) :: { { make-root ( t , quote Mend1.8 Init Deref Ponens end quote ) :: { { make-root ( t , quote Mend1.8 Init Deref end quote ) :: { { make-root ( t , quote Mend1.8 Init end quote ) :: { { make-root ( t , quote Mend1.8 end quote ) :: true } :: true } } :: true } } :: true } } :: { x :: true } } } :: { s [[ hook-arg ]] :: true } } ]] } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } end define

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:13:13.678589 = MJD-54293.TAI:20:13:46.678589 = LGT-4690988026678589e-6