OAI/Computability/QuantumFactoring/ExpressionTokenProcedure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.primPackP line 15
2. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.tokenTag line 46
3. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.tokenPayload line 47
4. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.tokenTagP line 48
5. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.tokenPayloadP line 52
6. abbrev OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprEnvCode line 55
7. abbrev OAI.ExactQuantumFactoring.NetworkEmission.Emission.ExprEnv line 56
8. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.envVars line 57
9. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.tokenOpP line 58
10. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprRunP line 89
11. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprResultP line 94
12. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprPackP line 99

    Source documentation

    Compiler runs in polynomial time in the expanded source syntax, dimensions and input networks. The environment contains no circuit-generation oracle.

    noncomputable def exprPackP : Procedure
        (fun x : ExprEnv×NatExpr ℕ=>prodCode exprEnvCode (listCode (exprTokenCode Nat.bits)) (x.1,exprTokens x.2)) packCode
        (fun x=>exprPack x.1.1 x.1.2.1 (envVars x.1.2.2) x.2):=
    …

    Mentions: OAI.ExactQuantumFactoring.NetworkEmission.Emission.ExprEnv, OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprEnvCode, OAI.ExactQuantumFactoring.NetworkEmission.exprTokenCode, OAI.ExactQuantumFactoring.NetworkEmission.exprTokens, OAI.ExactQuantumFactoring.NetworkEmission.packCode, OAI.ExactQuantumFactoring.NetworkEmission.exprPack, OAI.ExactQuantumFactoring.NetworkEmission.Emission.envVars