Logiweb(TM)

Logiweb codex of Peano in pyk

Up Help

ref-0-id-0 Peano
ref-0-id-1 expand-all ( " )
ref-0-id-2 expand-all1 ( " , " , " )
ref-0-id-3 is-meta-term ( " , " )
ref-0-id-4 unitac-hyp
ref-0-id-5 unitac-lemma-hyp ( " )
ref-0-id-6 unitac-rule-hyp ( " )
ref-0-id-7 unitac-conclude-hyp ( " )
ref-0-id-8 tactic-hyp ( " )
ref-0-id-9 tactic-dummyhyp ( " )
ref-0-id-10 tactic-ded ( " , " )
ref-0-id-11 tactic-first-hyp ( " , " , " )
ref-0-id-12 add-first-hyp* ( " , " , " )
ref-0-id-13 add-first-hyp ( " , " , " )
ref-0-id-14 tactic-next-hyp ( " , " , " , " )
ref-0-id-15 add-next-hyp* ( " , " , " )
ref-0-id-16 add-next-hyp ( " , " , " )
ref-0-id-17 f.unitac-adapt ( " , " , " )
ref-0-id-18 f.unitac-adapt-all ( " , " , " , " , " , " , " , " , " )
ref-0-id-19 f.tacfresh ( " )
ref-0-id-20 f.unitac-ponens ( " )
ref-0-id-21 f.unitac-Ponens ( " )
ref-0-id-22 f.unitac-at ( " )
ref-0-id-23 f.unitac-At ( " )
ref-0-id-24 sub ( " , " , " , " )
ref-0-id-25 sub0 ( " , " , " , " , " )
ref-0-id-26 sub1 ( " , " , " , " , " )
ref-0-id-27 sub* ( " , " , " , " , " )
ref-0-id-28 f.subst ( " , " , " )
ref-0-id-29 f.subst* ( " , " , " )
ref-0-id-30 inst ( " , " )
ref-0-id-31 inst0 ( " , " , " )
ref-0-id-32 inst1 ( " , " , " )
ref-0-id-33 inst-strip ( " , " , " )
ref-0-id-34 inst-zip ( " , " )
ref-0-id-35 inst2 ( " , " , " , " , " )
ref-0-id-36 inst2* ( " , " , " , " , " )
ref-0-id-37 inst3 ( " , " , " )
ref-0-id-38 inst3* ( " , " , " )
ref-0-id-39 def ( " , " )
ref-0-id-40 def0 ( " , " , " )
ref-0-id-41 def0* ( " , " , " )
ref-0-id-42 def1 ( " , " , " )
ref-0-id-43 def2 ( " , " , " )
ref-0-id-44 def3 ( " , " , " , " )
ref-0-id-45 def3* ( " , " , " , " )
ref-0-id-46 defcheck
ref-0-id-47 checked-def ( " , " )
ref-0-id-48 defcheck1 ( " )
ref-0-id-49 defcheck2 ( " , " )
ref-0-id-50 valid-def ( " , " , " , " )
ref-0-id-51 valid-def* ( " , " , " , " )
ref-0-id-52 Prop
ref-0-id-53 FOL
ref-0-id-54 PA
ref-0-id-55 MP
ref-0-id-56 Gen
ref-0-id-57 Def
ref-0-id-58 A1
ref-0-id-59 A2
ref-0-id-60 A3
ref-0-id-61 A4
ref-0-id-62 AP4
ref-0-id-63 A5
ref-0-id-64 tt
ref-0-id-65 ff
ref-0-id-66 S1
ref-0-id-67 S2
ref-0-id-68 S3
ref-0-id-69 S4
ref-0-id-70 S5
ref-0-id-71 S6
ref-0-id-72 S7
ref-0-id-73 S8
ref-0-id-74 S9
ref-0-id-75 Mend1.8
ref-0-id-76 A1'
ref-0-id-77 A2'
ref-0-id-78 Mend1.47b
ref-0-id-79 Mend1.47c
ref-0-id-80 Mend1.47d
ref-0-id-81 Mend1.11b
ref-0-id-82 Mend1.48d
ref-0-id-83 Mend1.48e
ref-0-id-84 Lnexthyp
ref-0-id-85 Lcurry
ref-0-id-86 LTruth
ref-0-id-87 LElimHyp
ref-0-id-88 LA4'
ref-0-id-89 LAP4'
ref-0-id-90 MP'
ref-0-id-91 Gen1
ref-0-id-92 Gen2
ref-0-id-93 Gen3
ref-0-id-94 Induction
ref-0-id-95 hook-hyp
ref-0-id-96 tactic-Prop ( " )
ref-0-id-97 tactic-FOL ( " )
ref-0-id-98 lemma-x
ref-0-id-99 lemma-y
ref-0-id-100 lemma-z
ref-0-id-101 lemma-u
ref-0-id-102 lemma-v
ref-0-id-103 lemma-w
ref-0-id-104 hyp
ref-0-id-105 3.2a
ref-0-id-106 3.2b
ref-0-id-107 3.2c
ref-0-id-108 3.2d
ref-0-id-109 3.2e
ref-0-id-110 3.2f
ref-0-id-111 3.2g
ref-0-id-112 3.2h
ref-0-id-113 " First
ref-0-id-114 " Second
ref-0-id-115 " suc
ref-0-id-116 not "
ref-0-id-117 " and "
ref-0-id-118 " or "
ref-0-id-119 all " : "
ref-0-id-120 f.allfunc "
ref-0-id-121 exist " : "
ref-0-id-122 f.existfunc "
ref-0-id-123 " imply "
ref-0-id-124 " when "
ref-0-id-125 " iff "
ref-0-id-126 " avoid "
ref-0-id-127 " f.At
ref-0-id-128 " Mp
ref-0-id-129 " mp "
ref-0-id-130 " f.at "
ref-0-id-131 line " : Hypothesis >> " ; "
ref-0-id-132 Line " : Hypothesis >> " ; "
ref-0-id-133 line " : Deduction ; "
ref-0-id-134 Line " : Deduction ; "

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