Logiweb codex of prove

Up Help

prove, << testMacro(∗), Tester1, Tester2, Tester3, Tester4, Tester5, Tester6,

∗ << test∗,

prove

[prove →^{prio} Preassociative [prove], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [a], [b], [c], [d], [e], [f ], [g], [h], [i], [j ], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [x], [y], [z], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [kvanti], [UniqueMember], [UniqueMember(Type)], [SameSeries], [A4], [SameMember], [Qclosed(Addition)], [Qclosed(Multiplication)], [FromCartProd(1)], [1rule fromCartProd(2)], [constantRationalSeries(∗)], [cartProd(∗)], [Power(∗)], [binaryUnion(∗, ∗)], [SetOfRationalSeries], [IsSubset(∗, ∗)], [(p∗, ∗)], [(s∗)], [(⋯)], [Objekt-var], [Ex-var], [Ph-var], [Værdi], [Variabel], [Op(∗)], [Op(∗, ∗)], [∗ ¨ == ∗], [ContainsEmpty(∗)], [Nat(∗)], [Dedu(∗, ∗)], [Dedu_{0}(∗, ∗)], [Dedu_{s}(∗, ∗, ∗)], [Dedu_{1}(∗, ∗, ∗)], [Dedu_{2}(∗, ∗, ∗)], [Dedu_{3}(∗, ∗, ∗, ∗)], [Dedu_{4}(∗, ∗, ∗, ∗)], [Dedu_{4}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{5}(∗, ∗, ∗)], [Dedu_{6}(∗, ∗, ∗, ∗)], [Dedu_{6}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{7}(∗)], [Dedu_{8}(∗, ∗)], [Dedu_{8}^{∗}(∗, ∗)], [Ex_{1}], [Ex_{2}], [Ex3], [Ex_{10}], [Ex_{20}], [∗_{Ex}], [∗^{Ex}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex}], [ph_{1}], [ph_{2}], [ph_{3}], [∗_{Ph}], [∗^{Ph}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡ ∗ | ∗:==∗⟩_{Me}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Me}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Me}], [bs], [OBS], [BS], [Ø], [SystemQ], [MP], [Gen], [Repetition], [Neg], [Ded], [ExistIntro], [Extensionality], [Ødef], [PairDef], [UnionDef], [PowerDef], [SeparationDef], [AddDoubleNeg], [RemoveDoubleNeg], [AndCommutativity], [AutoImply], [Contrapositive], [FirstConjunct], [SecondConjunct], [FromContradiction], [FromDisjuncts], [IffCommutativity], [IffFirst], [IffSecond], [ImplyTransitivity], [JoinConjuncts], [MP2], [MP3], [MP4], [MP5], [MT], [NegativeMT], [Technicality], [Weakening], [WeakenOr1], [WeakenOr2], [Formula2Pair], [Pair2Formula], [Formula2Union], [Union2Formula], [Formula2Sep], [Sep2Formula], [Formula2Power], [SubsetInPower], [HelperPowerIsSub], [PowerIsSub], [(Switch)HelperPowerIsSub], [(Switch)PowerIsSub], [ToSetEquality], [HelperToSetEquality(t)], [ToSetEquality(t)], [HelperFromSetEquality], [FromSetEquality], [HelperReflexivity], [Reflexivity], [HelperSymmetry], [Symmetry], [HelperTransitivity], [Transitivity], [ERisReflexive], [ERisSymmetric], [ERisTransitive], [ØisSubset], [HelperMemberNotØ], [MemberNotØ], [HelperUniqueØ], [UniqueØ], [==Reflexivity], [==Symmetry], [Helper==Transitivity], [==Transitivity], [HelperTransferNotEq], [TransferNotEq], [HelperPairSubset], [Helper(2)PairSubset], [PairSubset], [SamePair], [SameSingleton], [UnionSubset], [SameUnion], [SeparationSubset], [SameSeparation], [SameBinaryUnion], [IntersectionSubset], [SameIntersection], [AutoMember], [HelperEqSysNotØ], [EqSysNotØ], [HelperEqSubset], [EqSubset], [HelperEqNecessary], [EqNecessary], [HelperNoneEqNecessary], [Helper(2)NoneEqNecessary], [NoneEqNecessary], [EqClassIsSubset], [EqClassesAreDisjoint], [AllDisjoint], [AllDisjointImply], [BSsubset], [Union(BS/R)subset], [UnionIdentity], [EqSysIsPartition], [(x1)], [(x2)], [(y1)], [(y2)], [(v1)], [(v2)], [(v3)], [(v4)], [(v2n)], [(m1)], [(m2)], [(n1)], [(n2)], [(n3)], [(ϵ)], [(ϵ)_{1}], [(ϵ2)], [(fep)], [(fx)], [(fy)], [(fz)], [(fu)], [(fv)], [(fw)], [(rx)], [(ry)], [(rz)], [(ru)], [(sx)], [(sx1)], [(sy)], [(sy1)], [(sz)], [(sz1)], [(su)], [(su1)], [(fxs)], [(fys)], [(crs1)], [(f1)], [(f2)], [(f3)], [(f4)], [(op1)], [(op2)], [(r1)], [(s1)], [(s2)], [X_{1}], [X_{2}], [Y_{1}], [Y_{2}], [V_{1}], [V_{2}], [V_{3}], [V_{4}], [V_{2n}], [M_{1}], [M_{2}], [N_{1}], [N_{2}], [N_{3}], [ϵ], [ϵ1], [ϵ2], [FX], [FY], [FZ], [FU], [FV], [FW], [FEP], [RX], [RY], [RZ], [RU], [(SX)], [(SX1)], [(SY)], [(SY1)], [(SZ)], [(SZ1)], [(SU)], [(SU1)], [FXS], [FYS], [(F1)], [(F2)], [(F3)], [(F4)], [(OP1)], [(OP2)], [(R1)], [(S1)], [(S2)], [(EPob)], [(CRS1ob)], [(F1ob)], [(F2ob)], [(F3ob)], [(F4ob)], [(N1ob)], [(N2ob)], [(OP1ob)], [(OP2ob)], [(R1ob)], [(S1ob)], [(S2ob)], [ph_{4}], [ph_{5}], [ph_{6}], [NAT], [RATIONAL_{S}ERIES], [SERIES], [SetOfReals], [SetOfFxs], [N], [Q], [X], [xs], [xaF], [ysF], [us], [usFoelge], [0], [1], [(−1)], [2], [3], [1/2], [1/3], [2/3], [0f], [1f], [00], [01], [(− − 01)], [02], [01//02], [lemma plus0Left], [lemma times1Left], [lemma eqAdditionLeft], [lemma eqMultiplicationLeft], [PlusAssociativity(R)], [PlusAssociativity(R)XX], [Plus0(R)], [Negative(R)], [Times1(R)], [lessAddition(R)], [PlusCommutativity(R)], [LeqAntisymmetry(R)], [LeqTransitivity(R)], [leqAddition(R)], [Distribution(R)], [A4(Axiom)], [InductionAxiom], [EqualityAxiom], [EqLeqAxiom], [EqAdditionAxiom], [EqMultiplicationAxiom], [QisClosed(Reciprocal)(Imply)], [QisClosed(Reciprocal)], [QisClosed(Negative)(Imply)], [QisClosed(Negative)], [leqReflexivity], [leqAntisymmetryAxiom], [leqTransitivityAxiom], [leqTotality], [leqAdditionAxiom], [leqMultiplicationAxiom], [plusAssociativity], [plusCommutativity], [Negative], [plus0], [timesAssociativity], [timesCommutativity], [ReciprocalAxiom], [times1], [Distribution], [0not1], [lemma eqLeq(R)], [TimesAssociativity(R)], [TimesCommutativity(R)], [lemma =f to sameF], [lemma plusF(Sym)], [lemma timesF(Sym)], [Separation2formula(1)], [Separation2formula(2)], [IfThenElse(T)], [IfThenElse(F)], [Cauchy], [PlusF], [ReciprocalF], [From ==], [To ==], [From <<], [to <<], [FromInR], [PlusR], [PlusR(Sym)], [TimesR], [TimesR(Sym)], [ReciprocalR(Axiom)], [LessMinus1(N)], [Nonnegative(N)], [US0], [NextXS(UpperBound)], [NextXS(NoUpperBound)], [NextUS(UpperBound)], [NextUS(NoUpperBound)], [ExpZero], [ExpPositive], [ExpZero(R)], [ExpPositive(R)], [BSzero], [BSpositive], [UStelescope(Zero)], [UStelescope(Positive)], [EqAddition(R)], [Unminus(R)], [FromLimit], [ToUpperBound], [FromUpperBound], [USisUpperBound], [0not1(R)], [ExpUnbounded(R)], [FromLeq(Advanced)(N)], [FromLeastUpperBound], [ToLeastUpperBound], [XSisNotUpperBound], [ysFGreater], [ysFLess], [SmallInverse], [NatType], [RationalType], [SeriesType], [Max], [Numerical], [MemberOfSeries(Imply)], [JoinConjuncts(2conditions)], [prop lemma imply negation], [TND], [FromNegatedImply], [ToNegatedImply], [FromNegated(2 ∗ Imply)], [FromNegatedAnd], [FromNegatedOr], [ToNegatedOr], [FromNegations], [From3Disjuncts], [From2 ∗ 2Disjuncts], [NegateDisjunct1], [NegateDisjunct2], [ExpandDisjuncts], [SENC1], [SENC2], [LessLeq(R)], [MemberOfSeries], [memberOfSeries(Type)], [<< testMacro(∗)], [Tester1], [Tester2], [Tester3], [Tester4], [Tester5], [Tester6]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗^{hide}]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], ["∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗(exp)∗]; Preassociative [∗′], [R(∗)], [− − R(∗)], [rec∗]; Preassociative [∗/∗], [∗ ∩ ∗], [∗[∗]]; Preassociative [∪∗], [∗ ∪ ∗], [P(∗)]; Preassociative [{∗}], [StateExpand(∗, ∗, ∗)], [extractSeries(∗)], [SetOfSeries(∗)], [− − Macro(∗)], [ExpandList(∗, ∗, ∗)], [∗ ∗ Macro(∗)], [+ + Macro(∗)], [<< Macro(∗)], [UB(∗, ∗)], [LUB(∗, ∗)], [BS(∗, ∗)], [UStelescope(∗, ∗)], [(∗)], [|r ∗ |], [Limit(∗, ∗)], [Union(∗)], [IsOrderedPair(∗, ∗, ∗)], [IsRelation(∗, ∗, ∗)], [isFunction(∗, ∗, ∗)], [IsSeries(∗, ∗)], [IsNatural(∗, ∗)], [OrderedPair(∗, ∗)], [TypeNat(∗)], [TypeNat0(∗)], [TypeRational(∗)], [TypeRational0(∗)], [TypeSeries(∗, ∗)], [Typeseries0(∗, ∗)]; Preassociative [{∗, ∗}], [⟨∗, ∗⟩], [(−u∗)], [−_{f}∗], [(− − ∗)], [1f/∗], [1fny/∗], [01//temp∗]; Preassociative [∗ ∈ ∗]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [(∗ ∗ ∗)], [∗ ∗_{f} ∗], [∗ ∗ ∗∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [(∗ + ∗)], [(∗ − ∗)], [∗ +_{f} ∗], [∗ −_{f} ∗], [∗ + +∗], [R(∗) − −R(∗)]; Preassociative [| ∗ |], [if(∗, ∗, ∗)], [Max(∗, ∗)], [Max(∗, ∗)]; Preassociative [∗ = ∗], [∗ ≠ ∗], [∗ <= ∗], [∗ < ∗], [∗ <_{f} ∗], [∗ ≤_{f} ∗], [SF(∗, ∗)], [∗ == ∗], [∗!! == ∗], [∗ << ∗], [∗ <<== ∗], [∗ << test∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗==∗], [∗ ⊆ ∗]; Preassociative [¬∗], [ ˙¬ (∗)n], [∗ ∉ ∗], [∗ ≠ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ˙∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗], [∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗], [∗ ˙⇔ ∗]; Preassociative [{ph ∈ ∗ | ∗}]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗], [Π∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; ]

[prove →^{tex} “prove”]

[prove →^{pyk} “prove”]

<< testMacro(∗)

[<< testMacro(t) →^{val} Q̃(t, ⌈x⌉, ⌈x⌉ : : t^{2}^{2}^{2}^{1}^{2}^{1}^{2}^{2}^{2}^{1}^{1}^{1}^{1}^{1}^{1} : : T)]

[<< testMacro(t) →^{tex} “<<testMacro(#1.

)”] [<< testMacro(∗) →^{pyk} “<<testMacro( " )”]

Tester1

[Tester1 →^{tex} “Tester1”] [Tester1 →^{pyk} “tester1”]

Tester2

[Tester2 →^{tex} “Tester2”] [Tester2 →^{pyk} “tester2”]

Tester3

[Tester3 →^{tex} “Tester3”] [Tester3 →^{pyk} “tester3”]

Tester4

[Tester4 →^{tex} “Tester4”] [Tester4 →^{pyk} “tester4”]

Tester5

[Tester5 →^{tex} “Tester5”] [Tester5 →^{pyk} “tester5”]

Tester6

[Tester6 →^{tex} “Tester6”] [Tester6 →^{pyk} “tester6”]

∗ << test∗

[x << testy →^{macro} λt.λs.λc. << testMacro(t^{h} : : ExpandList(t^{t}, s, c))]

[x << testy →^{tex} “#1. <<test#2.”]

[∗ << test∗ →^{pyk} “" <<test "”]

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-12-07.UTC:17:24:53.972444 = MJD-54076.TAI:17:25:26.972444 = LGT-4672229126972444e-6