Logiweb diagnose of pok

Up Help

Error in proof of Prop 3.2i Unknown sequent operator:

L_{?}:  Arbitrary ≫  \underline{a}, \underline{b}, \underline{c}  ;
L_{?}:  Block ≫  Begin  ;
L_{?}:  Arbitrary ≫  \underline{a}, \underline{b}, \underline{c}  ; \underline{a} =

\underline{b} ⊢ Unification failed Prop 3.2e⊳\underline{a} = \underline{b} ≫\underline{a} + \underline{c} = \underline{b} + \underline{c}; Unification failed Prop 3.2h ≫\underline{a} + \underline{c} = \underline{c} + \underline{a}; Unification failed Prop 3.2h ≫\underline{b} + \underline{c} = \underline{c} + \underline{b}; Unification failed S1⊳\underline{a} + \underline{c} = \underline{b} + \underline{c}⊳\underline{a} + \underline{c} = \underline{c} + \underline{a} ≫\underline{b} + \underline{c} = \underline{c} + \underline{a}; Unification failed Prop 3.2b⊳\underline{b} + \underline{c} = \underline{c} + \underline{a} ≫\underline{c} + \underline{a} = \underline{b} + \underline{c};

L_{?}: Prop 3.2c⊳\underline{c} + \underline{a} = \underline{b} + \underline{c}⊳\underline{b} + \underline{c} = \underline{c} + \underline{b} ≫

\underline{c} + \underline{a} = \underline{c} + \underline{b} ;

L_{g}: Block ≫ End ; Unification failed Ded ⊳ L_{g} ≫ \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-21.UTC:11:30:14.300977 = MJD-53907.TAI:11:30:47.300977 = LGT-4657606247300977e-6